[infer][java] modeling that the resource created by ZipFile.getInputStream(ZipEntry entry) is closed by ZipFile.close()

Summary:
This fix fixes a case of false positive when a resource created by ZipFile.getInputStream() is expected to closed when closing the file
master
jrm 9 years ago
parent 3e199467f4
commit 9b63476805

@ -11,8 +11,6 @@ package java.util.jar;
import java.io.File;
import java.io.IOException;
import java.io.InputStream;
import java.util.zip.ZipEntry;
import java.util.zip.ZipFile;
@ -43,11 +41,6 @@ public class JarFile extends ZipFile {
throw new IOException();
}
public synchronized InputStream getInputStream(ZipEntry ze)
throws IOException {
return super.getInputStream(ze);
}
public void close() throws IOException {
super.close();
}

@ -11,76 +11,56 @@ package java.util.zip;
import com.facebook.infer.models.InferBuiltins;
import com.facebook.infer.models.InferUndefined;
import dalvik.system.CloseGuard;
import java.io.*;
import java.io.File;
import java.io.IOException;
import java.util.Enumeration;
import java.util.LinkedHashMap;
import java.util.NoSuchElementException;
public class ZipFile {
private void init() throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
public ZipFile(String name) throws IOException {
InferUndefined.can_throw_ioexception_void();
//Had to throw before setting attribute else
// whenInferRunsOnJarFileClosedThenResourceLeakIsNotFound fails
InferBuiltins.__set_file_attribute(this);
}
public ZipFile(String name) throws IOException {
init();
}
public ZipFile(File file, int mode) throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
public ZipFile(File file, int mode) throws IOException {
init();
}
public ZipFile(File file) throws ZipException, IOException {
this(file, 0);
}
public ZipFile(File file) throws ZipException, IOException {
init();
}
public InputStream getInputStream(ZipEntry entry) throws IOException {
FileInputStream in = new FileInputStream("");
return new InflaterInputStream(in, null, 0) {
private boolean isClosed = false;
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
super.close();
}
protected void finalize() throws IOException {
close();
}
protected void fill() throws IOException {
}
public Enumeration<? extends ZipEntry> entries() {
private boolean eof;
return new Enumeration<ZipEntry>() {
private boolean hasEls;
public int available() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
};
}
public boolean hasMoreElements() {
return hasEls;
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public ZipEntry nextElement() throws NoSuchElementException {
if (hasEls)
return new ZipEntry("");
else
throw new NoSuchElementException();
}
};
}
protected void finalize() throws IOException {
close();
}
public Enumeration<? extends ZipEntry> entries() {
return new Enumeration<ZipEntry>() {
private boolean hasEls;
public boolean hasMoreElements() {
return hasEls;
}
public ZipEntry nextElement() throws NoSuchElementException {
if (hasEls)
return new ZipEntry("");
else
throw new NoSuchElementException();
}
};
}
}

@ -16,7 +16,6 @@ import com.google.common.base.Preconditions;
import com.google.common.io.Closeables;
import java.io.BufferedInputStream;
import java.io.BufferedReader;
import java.io.Closeable;
import java.io.DataOutputStream;
import java.io.File;
@ -906,4 +905,11 @@ public class ResourceLeaks {
return reader;
}
public void withZipFile() throws IOException {
ZipFile f = new ZipFile("hi");
InputStream s = f.getInputStream(f.getEntry("there"));
if (s != null) s.toString();
f.close();
}
}

Loading…
Cancel
Save