From 2ded1d7a0c887021b17e0410383e043a22113861 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Fri, 10 Feb 2017 13:36:38 -0800 Subject: [PATCH] [infer][java] Simplify some of the models of Java resources [3/n] Summary: Even more simplifications of the models Reviewed By: sblackshear Differential Revision: D4542406 fbshipit-source-id: fd3aa82 --- .../java/src/java/io/BufferedInputStream.java | 51 ++---- .../java/src/java/io/DataInputStream.java | 6 +- .../java/src/java/io/FilterInputStream.java | 20 +-- .../java/src/java/io/ObjectInputStream.java | 163 +++++++++--------- .../models/java/src/java/io/PrintStream.java | 70 -------- .../java/src/java/io/PushbackInputStream.java | 66 +++---- .../src/java/security/DigestInputStream.java | 23 ++- .../src/java/util/jar/JarInputStream.java | 20 +-- .../src/java/util/zip/CheckedInputStream.java | 29 ++-- .../java/util/zip/DeflaterInputStream.java | 52 ++---- .../src/java/util/zip/GZIPInputStream.java | 26 ++- .../java/util/zip/InflaterInputStream.java | 17 -- .../src/java/util/zip/ZipInputStream.java | 41 ++--- .../src/javax/crypto/CipherInputStream.java | 45 ++--- .../tests/codetoanalyze/java/infer/issues.exp | 9 - 15 files changed, 221 insertions(+), 417 deletions(-) delete mode 100644 infer/models/java/src/java/io/PrintStream.java diff --git a/infer/models/java/src/java/io/BufferedInputStream.java b/infer/models/java/src/java/io/BufferedInputStream.java index c0762a48c..c4e45a3bc 100644 --- a/infer/models/java/src/java/io/BufferedInputStream.java +++ b/infer/models/java/src/java/io/BufferedInputStream.java @@ -11,43 +11,30 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class BufferedInputStream extends FilterInputStream { +public class BufferedInputStream { - public BufferedInputStream(InputStream in) { - super(in); - } + public int available() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public BufferedInputStream(InputStream in, int size) { - super(in); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int available() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public void close() throws IOException { - if (in != null) { - in.close(); - } - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public void reset() throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public long skip(long n) throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } - - public void reset() throws IOException { - InferUndefined.can_throw_ioexception_void(); - } - - public long skip(long n) throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } } diff --git a/infer/models/java/src/java/io/DataInputStream.java b/infer/models/java/src/java/io/DataInputStream.java index 33554e091..d71751f61 100644 --- a/infer/models/java/src/java/io/DataInputStream.java +++ b/infer/models/java/src/java/io/DataInputStream.java @@ -12,11 +12,7 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class DataInputStream extends FilterInputStream { - - public DataInputStream(InputStream in) { - super(in); - } +public class DataInputStream { public int read(byte b[]) throws IOException { return InferUndefined.can_throw_ioexception_int(); diff --git a/infer/models/java/src/java/io/FilterInputStream.java b/infer/models/java/src/java/io/FilterInputStream.java index 5344f746f..3271b6e82 100644 --- a/infer/models/java/src/java/io/FilterInputStream.java +++ b/infer/models/java/src/java/io/FilterInputStream.java @@ -11,30 +11,12 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class FilterInputStream extends InputStream { - - protected volatile InputStream in; - - protected FilterInputStream(InputStream in) { - this.in = in; - } +public class FilterInputStream { public int available() throws IOException { return InferUndefined.can_throw_ioexception_int(); } - public void close() throws IOException { - if (in != null) { - if (in instanceof FileInputStream) { - ((FileInputStream) in).close(); - } else if (in instanceof BufferedInputStream) { - ((FilterInputStream) in).close(); - } else { - in.close(); - } - } - } - public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); } diff --git a/infer/models/java/src/java/io/ObjectInputStream.java b/infer/models/java/src/java/io/ObjectInputStream.java index 6a2f84a5e..829bed0a7 100644 --- a/infer/models/java/src/java/io/ObjectInputStream.java +++ b/infer/models/java/src/java/io/ObjectInputStream.java @@ -9,118 +9,117 @@ package java.io; +import com.facebook.infer.builtins.InferBuiltins; import com.facebook.infer.builtins.InferUndefined; -public class ObjectInputStream extends InputStream { +public class ObjectInputStream { - private DataInputStream input; + InputStream in; - static class InputValidationDesc { - ObjectInputValidation validator; - int priority; - } + public ObjectInputStream(InputStream in) throws IOException { + InferUndefined.can_throw_ioexception_void(); + this.in = in; + } - public ObjectInputStream(InputStream in) throws IOException { - this.input = new DataInputStream(in); - InferUndefined.can_throw_ioexception_void(); + public void close() throws IOException { + if (in != null) { + in.close(); } + } - protected ObjectInputStream() throws IOException, SecurityException { - } + protected ObjectInputStream() throws IOException, SecurityException { + } - public int available() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int available() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public void close() throws IOException { - input.close(); - } + public void defaultReadObject() throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public void defaultReadObject() throws IOException { - InferUndefined.can_throw_ioexception_void(); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public boolean readBoolean() throws IOException { + return InferUndefined.can_throw_ioexception_boolean(); + } - public boolean readBoolean() throws IOException { - return InferUndefined.can_throw_ioexception_boolean(); - } + public byte readByte() throws IOException { + return InferUndefined.can_throw_ioexception_byte(); + } - public byte readByte() throws IOException { - return InferUndefined.can_throw_ioexception_byte(); - } + public char readChar() throws IOException { + return InferUndefined.can_throw_ioexception_char(); + } - public char readChar() throws IOException { - return InferUndefined.can_throw_ioexception_char(); - } + public double readDouble() throws IOException { + return InferUndefined.can_throw_ioexception_double(); + } - public double readDouble() throws IOException { - return InferUndefined.can_throw_ioexception_double(); - } + public ObjectInputStream.GetField readFields() throws IOException { + throw new IOException(); + } - public ObjectInputStream.GetField readFields() throws IOException { - throw new IOException(); - } + public float readFloat() throws IOException { + return InferUndefined.can_throw_ioexception_float(); + } - public float readFloat() throws IOException { - return InferUndefined.can_throw_ioexception_float(); - } + public void readFully(byte[] buf) throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public void readFully(byte[] buf) throws IOException { - InferUndefined.can_throw_ioexception_void(); - } + public void readFully(byte[] buf, int off, int len) throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public void readFully(byte[] buf, int off, int len) throws IOException { - InferUndefined.can_throw_ioexception_void(); - } + public int readInt() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int readInt() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public long readLong() throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } - public long readLong() throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } + public final Object readObject() throws IOException { + return InferUndefined.can_throw_ioexception_object(); + } - public final Object readObject() throws IOException { - return InferUndefined.can_throw_ioexception_object(); - } + public short readShort() throws IOException { + return InferUndefined.can_throw_ioexception_short(); + } - public short readShort() throws IOException { - return InferUndefined.can_throw_ioexception_short(); - } + public Object readUnshared() throws IOException, ClassNotFoundException { + return InferUndefined.can_throw_ioexception_object(); + } - public Object readUnshared() throws IOException, ClassNotFoundException { - return InferUndefined.can_throw_ioexception_object(); - } + public int readUnsignedByte() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int readUnsignedByte() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int readUnsignedShort() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int readUnsignedShort() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public String readUTF() throws IOException { + return InferUndefined.can_throw_ioexception_string(); + } - public String readUTF() throws IOException { - return InferUndefined.can_throw_ioexception_string(); - } + public int skipBytes(int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int skipBytes(int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public static abstract class GetField { + } - public static abstract class GetField { - } } diff --git a/infer/models/java/src/java/io/PrintStream.java b/infer/models/java/src/java/io/PrintStream.java deleted file mode 100644 index d73cc4790..000000000 --- a/infer/models/java/src/java/io/PrintStream.java +++ /dev/null @@ -1,70 +0,0 @@ -/* - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - */ - -package java.io; - -public class PrintStream extends FilterOutputStream implements Closeable { - - public PrintStream(OutputStream out) { - super(out); - } - - public PrintStream(OutputStream out, boolean autoFlush) { - super(out); - } - - public PrintStream(OutputStream out, boolean autoFlush, String encoding) - throws UnsupportedEncodingException { - super(out); - } - - public PrintStream(String fileName) throws FileNotFoundException { - super(new FileOutputStream(fileName)); - } - - public PrintStream(String fileName, String csn) - throws FileNotFoundException, UnsupportedEncodingException { - super(new FileOutputStream(fileName)); - } - - public PrintStream(File file) throws FileNotFoundException { - super(new FileOutputStream(file)); - } - - public PrintStream(File file, String csn) throws FileNotFoundException, - UnsupportedEncodingException { - super(new FileOutputStream(file)); - } - - public void close() { - if (out != null) { - try { - if (out instanceof FileOutputStream) - ((FileOutputStream) out).close(); - } catch (IOException e) { - } - } - } - - //the methods write and flush in this class do not throw IOExceptions, thus they are - //modelled as a void method that does nothing. - - public void write(byte b[], int off, int len) { - } - - public void write(byte b[]) throws IOException { - } - - public void write(int b) { - } - - public void flush() { - } - -} diff --git a/infer/models/java/src/java/io/PushbackInputStream.java b/infer/models/java/src/java/io/PushbackInputStream.java index d513802c7..ce5f65007 100644 --- a/infer/models/java/src/java/io/PushbackInputStream.java +++ b/infer/models/java/src/java/io/PushbackInputStream.java @@ -11,53 +11,43 @@ package java.io; import com.facebook.infer.builtins.InferUndefined; -public class PushbackInputStream extends FilterInputStream { - public PushbackInputStream(InputStream in, int size) { - super(in); - } +public class PushbackInputStream { - public PushbackInputStream(InputStream in) { - super(in); - } + public int available() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int available() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public void close() throws IOException { - super.close(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public void reset() throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public long skip(long n) throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } - public void reset() throws IOException { - InferUndefined.can_throw_ioexception_void(); - } + public void unread(byte[] b) throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public long skip(long n) throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } + public void unread(byte[] b, int off, int len) throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public void unread(byte[] b) throws IOException { - InferUndefined.can_throw_ioexception_void(); - } + public void unread(int b) throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public void unread(byte[] b, int off, int len) throws IOException { - InferUndefined.can_throw_ioexception_void(); - } - - public void unread(int b) throws IOException { - InferUndefined.can_throw_ioexception_void(); - } } diff --git a/infer/models/java/src/java/security/DigestInputStream.java b/infer/models/java/src/java/security/DigestInputStream.java index 8eb6824dc..c131be30d 100644 --- a/infer/models/java/src/java/security/DigestInputStream.java +++ b/infer/models/java/src/java/security/DigestInputStream.java @@ -16,21 +16,18 @@ import java.io.IOException; import java.io.InputStream; -public class DigestInputStream extends FilterInputStream { +public class DigestInputStream { - public DigestInputStream(InputStream stream, MessageDigest digest) { - super(stream); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } } diff --git a/infer/models/java/src/java/util/jar/JarInputStream.java b/infer/models/java/src/java/util/jar/JarInputStream.java index 61d3a0a0d..3cfeaecf5 100644 --- a/infer/models/java/src/java/util/jar/JarInputStream.java +++ b/infer/models/java/src/java/util/jar/JarInputStream.java @@ -9,23 +9,23 @@ package java.util.jar; +import com.facebook.infer.builtins.InferBuiltins; import com.facebook.infer.builtins.InferUndefined; import java.io.IOException; import java.io.InputStream; import java.util.zip.ZipInputStream; +public class JarInputStream { -public class JarInputStream extends ZipInputStream { + public JarInputStream(InputStream in) throws IOException { + InferUndefined.can_throw_ioexception_void(); + InferBuiltins.__set_mem_attribute(in); + InferBuiltins.__set_file_attribute(this); + } - public JarInputStream(InputStream in) throws IOException { - super(in); - InferUndefined.can_throw_ioexception_void(); - } - - public JarInputStream(InputStream in, boolean verify) throws IOException { - super(in); - InferUndefined.can_throw_ioexception_void(); - } + public JarInputStream(InputStream in, boolean verify) throws IOException { + this(in); + } } diff --git a/infer/models/java/src/java/util/zip/CheckedInputStream.java b/infer/models/java/src/java/util/zip/CheckedInputStream.java index cbee94934..da84bad6d 100644 --- a/infer/models/java/src/java/util/zip/CheckedInputStream.java +++ b/infer/models/java/src/java/util/zip/CheckedInputStream.java @@ -15,25 +15,22 @@ import java.io.FilterInputStream; import java.io.IOException; import java.io.InputStream; -public class CheckedInputStream extends FilterInputStream { +public class CheckedInputStream { - public CheckedInputStream(InputStream in, Checksum cksum) { - super(in); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public long skip(long n) throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } - public long skip(long n) throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } } diff --git a/infer/models/java/src/java/util/zip/DeflaterInputStream.java b/infer/models/java/src/java/util/zip/DeflaterInputStream.java index 7a93e2ad3..bfc3f1dc2 100644 --- a/infer/models/java/src/java/util/zip/DeflaterInputStream.java +++ b/infer/models/java/src/java/util/zip/DeflaterInputStream.java @@ -15,46 +15,32 @@ import java.io.FilterInputStream; import java.io.IOException; import java.io.InputStream; -public class DeflaterInputStream extends FilterInputStream { +public class DeflaterInputStream { - public DeflaterInputStream(InputStream in) { - super(in); - } - public DeflaterInputStream(InputStream in, Deflater defl) { - super(in); - } + public int available() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public DeflaterInputStream(InputStream in, Deflater defl, int bufLen) { - super(in); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int available() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public void close() throws IOException { - super.close(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public void reset() throws IOException { + InferUndefined.can_throw_ioexception_void(); + } - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public long skip(long n) throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } - - public void reset() throws IOException { - InferUndefined.can_throw_ioexception_void(); - } - - public long skip(long n) throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } } diff --git a/infer/models/java/src/java/util/zip/GZIPInputStream.java b/infer/models/java/src/java/util/zip/GZIPInputStream.java index a5a8520fb..b5704eb15 100644 --- a/infer/models/java/src/java/util/zip/GZIPInputStream.java +++ b/infer/models/java/src/java/util/zip/GZIPInputStream.java @@ -9,29 +9,23 @@ package java.util.zip; +import com.facebook.infer.builtins.InferBuiltins; import com.facebook.infer.builtins.InferUndefined; import java.io.IOException; import java.io.InputStream; -public class GZIPInputStream extends InflaterInputStream { +public class GZIPInputStream { - public GZIPInputStream(InputStream in, int size) throws IOException { - super(in); - if (!InferUndefined.boolean_undefined()) { - throw new IOException(); - } - } + public GZIPInputStream(InputStream in) throws IOException { + InferUndefined.can_throw_ioexception_void(); + InferBuiltins.__set_mem_attribute(in); + InferBuiltins.__set_file_attribute(this); + } - public GZIPInputStream(InputStream in) throws IOException { - super(in); - if (!InferUndefined.boolean_undefined()) { - throw new IOException(); - } - } + public GZIPInputStream(InputStream in, int size) throws IOException { + this(in); + } - public void close() throws IOException { - super.close(); - } } diff --git a/infer/models/java/src/java/util/zip/InflaterInputStream.java b/infer/models/java/src/java/util/zip/InflaterInputStream.java index b3de9f6aa..6e7fba777 100644 --- a/infer/models/java/src/java/util/zip/InflaterInputStream.java +++ b/infer/models/java/src/java/util/zip/InflaterInputStream.java @@ -17,26 +17,10 @@ import java.io.InputStream; public class InflaterInputStream extends FilterInputStream { - public InflaterInputStream(InputStream in, Inflater inf, int size) { - super(in); - } - - public InflaterInputStream(InputStream in, Inflater inf) { - super(in); - } - - public InflaterInputStream(InputStream in) { - super(in); - } - public int available() throws IOException { return InferUndefined.can_throw_ioexception_int(); } - public void close() throws IOException { - super.close(); - } - public int read() throws IOException { return InferUndefined.can_throw_ioexception_int(); } @@ -53,7 +37,6 @@ public class InflaterInputStream extends FilterInputStream { InferUndefined.can_throw_ioexception_void(); } - public long skip(long n) throws IOException { return InferUndefined.can_throw_ioexception_long(); } diff --git a/infer/models/java/src/java/util/zip/ZipInputStream.java b/infer/models/java/src/java/util/zip/ZipInputStream.java index 8a7ca32ee..54d93f643 100644 --- a/infer/models/java/src/java/util/zip/ZipInputStream.java +++ b/infer/models/java/src/java/util/zip/ZipInputStream.java @@ -16,33 +16,18 @@ import java.io.FileInputStream; import java.io.IOException; import java.io.InputStream; -public class ZipInputStream extends InflaterInputStream { - - private ZipEntry currentEntry; - - public ZipInputStream(InputStream in) { - super(in); - } - - public ZipEntry getNextEntry() throws IOException { - boolean undef = InferUndefined.boolean_undefined(); - if (undef) { - return currentEntry; - } else - throw new IOException(); - } - - public void closeEntry() throws IOException { - InferUndefined.can_throw_ioexception_void(); - } - - public void close() throws IOException { - if (in != null) - if (in instanceof FileInputStream) { - ((FileInputStream) in).close(); - } else if (in instanceof BufferedInputStream) { - ((BufferedInputStream) in).close(); - } - } +public class ZipInputStream { + + public ZipEntry getNextEntry() throws IOException { + boolean undef = InferUndefined.boolean_undefined(); + if (undef) { + return new ZipEntry(""); + } else + throw new IOException(); + } + + public void closeEntry() throws IOException { + InferUndefined.can_throw_ioexception_void(); + } } diff --git a/infer/models/java/src/javax/crypto/CipherInputStream.java b/infer/models/java/src/javax/crypto/CipherInputStream.java index ec9bab083..6d7a16678 100644 --- a/infer/models/java/src/javax/crypto/CipherInputStream.java +++ b/infer/models/java/src/javax/crypto/CipherInputStream.java @@ -15,39 +15,26 @@ import java.io.FilterInputStream; import java.io.IOException; import java.io.InputStream; -public class CipherInputStream extends FilterInputStream { +public class CipherInputStream { + public int available() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public CipherInputStream(InputStream is, Cipher c) { - super(is); - } + public int read() throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - protected CipherInputStream(InputStream is) { - super(is); - } + public int read(byte b[]) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public int available() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } + public int read(byte b[], int off, int len) throws IOException { + return InferUndefined.can_throw_ioexception_int(); + } - public void close() throws IOException { - super.close(); - } - - public int read() throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } - - public int read(byte b[]) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } - - public int read(byte b[], int off, int len) throws IOException { - return InferUndefined.can_throw_ioexception_int(); - } - - public long skip(long n) throws IOException { - return InferUndefined.can_throw_ioexception_long(); - } + public long skip(long n) throws IOException { + return InferUndefined.can_throw_ioexception_long(); + } } diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 67ab7c688..4e5ae7ab7 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -61,38 +61,29 @@ codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.dynamicDispa codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.dynamicDispatchShouldNotReportWhenCallingSupertype(DynamicDispatch$Subtype), 3, NULL_DEREFERENCE, [start of procedure dynamicDispatchShouldNotReportWhenCallingSupertype(...),start of procedure foo(),return from a call to Object DynamicDispatch$Subtype.foo()] codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasy(), 3, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeEasy(),start of procedure DynamicDispatch$Impl(),return from a call to DynamicDispatch$Impl.(),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()] codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Impl), 1, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeHard(...),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.bufferedInputStreamClosedAfterReset(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure bufferedInputStreamClosedAfterReset(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.bufferedInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure bufferedInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.bufferedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure bufferedInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamClosedAfterSkip(), 6, RETURN_VALUE_IGNORED, [start of procedure checkedInputStreamClosedAfterSkip()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamClosedAfterSkip(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure checkedInputStreamClosedAfterSkip(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure checkedInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure checkedInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamClosedAfterRead(), 6, RETURN_VALUE_IGNORED, [start of procedure cipherInputStreamClosedAfterRead()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamClosedAfterRead(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure cipherInputStreamClosedAfterRead(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamNotClosedAfterSkip(), 5, RETURN_VALUE_IGNORED, [start of procedure cipherInputStreamNotClosedAfterSkip()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamNotClosedAfterSkip(), 7, RESOURCE_LEAK, [start of procedure cipherInputStreamNotClosedAfterSkip(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.dataInputStreamClosedAfterReadBoolean(), 6, RETURN_VALUE_IGNORED, [start of procedure dataInputStreamClosedAfterReadBoolean()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.dataInputStreamClosedAfterReadBoolean(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure dataInputStreamClosedAfterReadBoolean(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.dataInputStreamNotClosedAfterRead(), 6, RETURN_VALUE_IGNORED, [start of procedure dataInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.dataInputStreamNotClosedAfterRead(), 8, RESOURCE_LEAK, [start of procedure dataInputStreamNotClosedAfterRead(),exception java.io.IOException] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.deflaterInputStreamClosedAfterReset(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure deflaterInputStreamClosedAfterReset(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.deflaterInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure deflaterInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.deflaterInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure deflaterInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.digestInputStreamClosedAfterRead(), 6, RETURN_VALUE_IGNORED, [start of procedure digestInputStreamClosedAfterRead()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.digestInputStreamClosedAfterRead(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure digestInputStreamClosedAfterRead(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.digestInputStreamNotClosedAfterRead(), 6, RETURN_VALUE_IGNORED, [start of procedure digestInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.digestInputStreamNotClosedAfterRead(), 8, RESOURCE_LEAK, [start of procedure digestInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamClosedAfterRead(), 6, RETURN_VALUE_IGNORED, [start of procedure gzipInputStreamClosedAfterRead()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamClosedAfterRead(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure gzipInputStreamClosedAfterRead(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamNotClosedAfterRead(), 4, RESOURCE_LEAK, [start of procedure gzipInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure gzipInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.gzipInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure gzipInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.inflaterInputStreamClosedAfterAvailable(), 6, RETURN_VALUE_IGNORED, [start of procedure inflaterInputStreamClosedAfterAvailable()] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.inflaterInputStreamClosedAfterAvailable(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure inflaterInputStreamClosedAfterAvailable(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.inflaterInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure inflaterInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.inflaterInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure inflaterInputStreamNotClosedAfterRead(),exception java.io.IOException] -codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.pushbackInputStreamClosedAfterReset(), 9, NULL_TEST_AFTER_DEREFERENCE, [start of procedure pushbackInputStreamClosedAfterReset(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.pushbackInputStreamNotClosedAfterRead(), 5, RETURN_VALUE_IGNORED, [start of procedure pushbackInputStreamNotClosedAfterRead()] codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.pushbackInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure pushbackInputStreamNotClosedAfterRead(),exception java.io.IOException] codetoanalyze/java/infer/FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.bufferedOutputStreamClosedAfterWrite(), 10, NULL_TEST_AFTER_DEREFERENCE, [start of procedure bufferedOutputStreamClosedAfterWrite(),exception java.io.IOException,Switch condition is true. Entering switch case,Taking false branch]