[RFC] Format all java files

Reviewed By: jeremydubreil

Differential Revision: D10067033

fbshipit-source-id: 73975664e
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent d4f943e953
commit 7c89d92851

@ -10,11 +10,9 @@ package infer.inferandroidexample;
import android.app.Application;
import android.test.ApplicationTestCase;
/**
* <a href="http://d.android.com/tools/testing/testing_android.html">Testing Fundamentals</a>
*/
/** <a href="http://d.android.com/tools/testing/testing_android.html">Testing Fundamentals</a> */
public class ApplicationTest extends ApplicationTestCase<Application> {
public ApplicationTest() {
super(Application.class);
}
public ApplicationTest() {
super(Application.class);
}
}

@ -14,5 +14,4 @@ public class Generated {
static Object returnsNull() {
return null;
}
}

@ -7,73 +7,71 @@
package infer.inferandroidexample;
import android.support.v7.app.ActionBarActivity;
import android.os.Bundle;
import android.support.v7.app.ActionBarActivity;
import android.view.Menu;
import android.view.MenuItem;
import java.io.FileOutputStream;
import java.io.IOException;
import java.util.Calendar;
public class MainActivity extends ActionBarActivity {
@Override
protected void onCreate(Bundle savedInstanceState) {
super.onCreate(savedInstanceState);
setContentView(R.layout.activity_main);
String s = getDay();
int length = s.length();
writeToFile();
}
private String getDay() {
if (Calendar.getInstance().get(Calendar.DAY_OF_WEEK) == Calendar.WEDNESDAY) {
return "Wednesday";
} else {
return otherOutput();
}
}
@Override
protected void onCreate(Bundle savedInstanceState) {
super.onCreate(savedInstanceState);
setContentView(R.layout.activity_main);
String s = getDay();
int length = s.length();
writeToFile();
}
private String otherOutput() {
return null;
private String getDay() {
if (Calendar.getInstance().get(Calendar.DAY_OF_WEEK) == Calendar.WEDNESDAY) {
return "Wednesday";
} else {
return otherOutput();
}
}
private void writeToFile() {
byte[] arr = {1, 2, 3};
FileOutputStream fis;
try {
fis = new FileOutputStream("file.txt");
fis.write(arr);
fis.close();
} catch (IOException e) {
//Deal with exception
}
}
private String otherOutput() {
return null;
}
@Override
public boolean onCreateOptionsMenu(Menu menu) {
// Inflate the menu; this adds items to the action bar if it is present.
getMenuInflater().inflate(R.menu.menu_main, menu);
return true;
private void writeToFile() {
byte[] arr = {1, 2, 3};
FileOutputStream fis;
try {
fis = new FileOutputStream("file.txt");
fis.write(arr);
fis.close();
} catch (IOException e) {
// Deal with exception
}
}
@Override
public boolean onOptionsItemSelected(MenuItem item) {
// Handle action bar item clicks here. The action bar will
// automatically handle clicks on the Home/Up button, so long
// as you specify a parent activity in AndroidManifest.xml.
int id = item.getItemId();
@Override
public boolean onCreateOptionsMenu(Menu menu) {
// Inflate the menu; this adds items to the action bar if it is present.
getMenuInflater().inflate(R.menu.menu_main, menu);
return true;
}
//noinspection SimplifiableIfStatement
if (id == R.id.action_settings) {
return true;
}
@Override
public boolean onOptionsItemSelected(MenuItem item) {
// Handle action bar item clicks here. The action bar will
// automatically handle clicks on the Home/Up button, so long
// as you specify a parent activity in AndroidManifest.xml.
int id = item.getItemId();
return super.onOptionsItemSelected(item);
//noinspection SimplifiableIfStatement
if (id == R.id.action_settings) {
return true;
}
return super.onOptionsItemSelected(item);
}
private void inferShouldNotReport() {
// Generated.java is supposed to be skipped by infer, thus even though
// Generated.returnsNull() returns null, infer is not supposed to know
@ -81,5 +79,4 @@ public class MainActivity extends ActionBarActivity {
Object o = Generated.returnsNull();
o.toString();
}
}

@ -8,8 +8,8 @@
package infer.other;
import android.annotation.SuppressLint;
import android.support.v7.app.ActionBarActivity;
import android.os.Bundle;
import android.support.v7.app.ActionBarActivity;
public class MainActivity extends ActionBarActivity {
@ -26,5 +26,4 @@ public class MainActivity extends ActionBarActivity {
void shouldNotBeReported() {
source().toString();
}
}

@ -42,9 +42,8 @@ class Hello {
}
/**
* This method should be rewritten with nested try { ... } finally {
* ... } statements, or the possible exception raised by fis.close()
* should be swallowed.
* This method should be rewritten with nested try { ... } finally { ... } statements, or the
* possible exception raised by fis.close() should be swallowed.
*/
void twoResources() throws IOException {
FileInputStream fis = null;
@ -54,9 +53,12 @@ class Hello {
fos = new FileOutputStream(new File("everwhat.txt"));
fos.write(fis.read());
} finally {
if (fis != null) { fis.close(); }
if (fos != null) { fos.close(); }
if (fis != null) {
fis.close();
}
if (fos != null) {
fos.close();
}
}
}
}

@ -10,8 +10,7 @@ package hello;
public class Pointers {
public static class A {
public void method() {
}
public void method() {}
}
public static A mayReturnNull(int i) {
@ -20,5 +19,4 @@ public class Pointers {
}
return null;
}
}

@ -21,5 +21,4 @@ public class Resources {
return null;
}
}
}

@ -7,9 +7,9 @@
package com.facebook.infer.annotation;
import javax.annotation.Nullable;
import java.util.List;
import java.util.Map;
import javax.annotation.Nullable;
public class Assertions {
@ -53,11 +53,9 @@ public class Assertions {
return assertNotNull(map.get(key));
}
public static void assumeCondition(boolean condition) {
}
public static void assumeCondition(boolean condition) {}
public static void assumeCondition(boolean condition, String explanation) {
}
public static void assumeCondition(boolean condition, String explanation) {}
public static void assertCondition(boolean condition) {
if (!condition) {

@ -13,5 +13,5 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target({ ElementType.METHOD, ElementType.TYPE })
@Target({ElementType.METHOD, ElementType.TYPE})
public @interface Expensive {}

@ -12,9 +12,7 @@ import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* Annotation for a boolean function returning false when the argument is null.
*/
/** Annotation for a boolean function returning false when the argument is null. */
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.METHOD})
public @interface FalseOnNull {}

@ -12,29 +12,23 @@ import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/** Annotation for methods that always return the same value. The annotation is inherited by
* overrides of methods.
*
* This annotation is used to suppress benign race warnings on fields assigned to methods annotated
* with {@literal @Functional} in the thread-safety analysis. For example:
*
* T mField;
* {@literal @Functional} T someMethod();
* public void getField() {
* if (mField == null) {
* mField = someMethod();
* }
* return mField;
* }
*
* Normally, we'd report that the access to mField is unsafe, but we won't report here because of
* the {@literal @Functional} annotation.
*
* If the return value of the annotated function is a double or long, the annotation will be
* ignored because writes to doubles/longs are not guaranteed to be atomic. That is, if type T was
* `long` in the example above, the write-write race on mField would no longer be benign.
*/
/**
* Annotation for methods that always return the same value. The annotation is inherited by
* overrides of methods.
*
* <p>This annotation is used to suppress benign race warnings on fields assigned to methods
* annotated with {@literal @Functional} in the thread-safety analysis. For example:
*
* <p>T mField; {@literal @Functional} T someMethod(); public void getField() { if (mField == null)
* { mField = someMethod(); } return mField; }
*
* <p>Normally, we'd report that the access to mField is unsafe, but we won't report here because of
* the {@literal @Functional} annotation.
*
* <p>If the return value of the annotated function is a double or long, the annotation will be
* ignored because writes to doubles/longs are not guaranteed to be atomic. That is, if type T was
* `long` in the example above, the write-write race on mField would no longer be benign.
*/
@Target({ElementType.METHOD})
@Retention(RetentionPolicy.CLASS)
public @interface Functional {}

@ -13,11 +13,11 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* A method annotated with @Initializer should always be be called before the object is used.
* Users of the class and static checkers must enforce, and can rely on, this invariant.
* Examples include methods called indirectly by the constructor, protocols of init-then-use
* where some values are initialized after construction but before the first use,
* and builder classes where an object initialization must complete before build() is called.
* A method annotated with @Initializer should always be be called before the object is used. Users
* of the class and static checkers must enforce, and can rely on, this invariant. Examples include
* methods called indirectly by the constructor, protocols of init-then-use where some values are
* initialized after construction but before the first use, and builder classes where an object
* initialization must complete before build() is called.
*/
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.CONSTRUCTOR, ElementType.METHOD})

@ -13,9 +13,6 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target(
ElementType.PARAMETER // a user-controlled should not flow to this parameter
)
public @interface IntegritySink {
}
@Target(ElementType.PARAMETER // a user-controlled should not flow to this parameter
)
public @interface IntegritySink {}

@ -13,11 +13,10 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target(value={
ElementType.METHOD, // method returns something user-controlled
ElementType.PARAMETER, // parameter is user-controlled
ElementType.FIELD, // field is user-controlled
})
public @interface IntegritySource {
}
@Target(
value = {
ElementType.METHOD, // method returns something user-controlled
ElementType.PARAMETER, // parameter is user-controlled
ElementType.FIELD, // field is user-controlled
})
public @interface IntegritySource {}

@ -13,11 +13,7 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target({
ElementType.CONSTRUCTOR,
ElementType.METHOD,
ElementType.TYPE
})
@Target({ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE})
// Signal to the starvation checker that the method (or all the methods of the class,
// if at class level) does not perform any potentially blocking operations. Can be used to

@ -13,12 +13,10 @@ import java.lang.annotation.RetentionPolicy;
/**
* Marks a class as one that is expected to be extended.
*
* This annotation is meant to counter common misuses of subclassing. Annotate your class with this
* only if it was built with the purpose of being extended.
* <p>This annotation is meant to counter common misuses of subclassing. Annotate your class with
* this only if it was built with the purpose of being extended.
*
* Avoid adding this to classes that have existed for a long time without needing it.
* <p>Avoid adding this to classes that have existed for a long time without needing it.
*/
@Retention(RetentionPolicy.SOURCE)
public @interface OkToExtend {
}
public @interface OkToExtend {}

@ -13,5 +13,5 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target(value={ElementType.METHOD, ElementType.TYPE})
@Target(value = {ElementType.METHOD, ElementType.TYPE})
public @interface PerformanceCritical {}

@ -13,11 +13,16 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* A class field, or method return/parameter type, of Optional type is annotated @Present
* to indicate that its value cannot be absent.
* Users of the method/field and static checkers must enforce, and can rely on, this invariant.
* A class field, or method return/parameter type, of Optional type is annotated @Present to
* indicate that its value cannot be absent. Users of the method/field and static checkers must
* enforce, and can rely on, this invariant.
*/
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.CONSTRUCTOR,
ElementType.METHOD, ElementType.PARAMETER})
@Target({
ElementType.TYPE,
ElementType.FIELD,
ElementType.CONSTRUCTOR,
ElementType.METHOD,
ElementType.PARAMETER
})
public @interface Present {}

@ -13,9 +13,6 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target(
ElementType.PARAMETER // a privacy source should not flow to this parameter
)
public @interface PrivacySink {
}
@Target(ElementType.PARAMETER // a privacy source should not flow to this parameter
)
public @interface PrivacySink {}

@ -13,11 +13,10 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target(value={
ElementType.METHOD, // method returns something private
ElementType.PARAMETER, // parameter is private
ElementType.FIELD, // field is private
})
public @interface PrivacySource {
}
@Target(
value = {
ElementType.METHOD, // method returns something private
ElementType.PARAMETER, // parameter is private
ElementType.FIELD, // field is private
})
public @interface PrivacySource {}

@ -12,10 +12,7 @@ import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* Annotation to indicate that when the parameter is null, the result is also null.
*/
/** Annotation to indicate that when the parameter is null, the result is also null. */
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.PARAMETER})
public @interface PropagatesNullable {
}
public @interface PropagatesNullable {}

@ -15,10 +15,9 @@ import java.lang.annotation.Target;
/**
* Tell the thread-safety analysis that this method transfers ownership of its return value to its
* caller. Ownership means that the caller is allowed to both read and write the value outside of
* synchronization. The annotated method should not retain any references to the value.
* This annotation is trusted for now, but may be checked eventually.
* synchronization. The annotated method should not retain any references to the value. This
* annotation is trusted for now, but may be checked eventually.
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.CLASS)
public @interface ReturnsOwnership {
}
public @interface ReturnsOwnership {}

@ -14,10 +14,9 @@ import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target({
ElementType.CONSTRUCTOR,
ElementType.METHOD,
ElementType.CONSTRUCTOR,
ElementType.METHOD,
})
public @interface SuppressLint {
String[] value();
}

@ -13,8 +13,8 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* View can be annotated with @SuppressViewNullability to silence warnings when
* a view is set to null in a destructor, and created in an initializer.
* View can be annotated with @SuppressViewNullability to silence warnings when a view is set to
* null in a destructor, and created in an initializer.
*/
@Retention(RetentionPolicy.CLASS)
@Target(ElementType.FIELD)

@ -13,12 +13,10 @@ import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* Tell the analysis that a collection is thread-safe when this information is not already
* reflected in the collection's type. For example:
* private {@literal @SynchronizedCollection} Map mMap = Collections.synchronizedMap(...);
* Tell the analysis that a collection is thread-safe when this information is not already reflected
* in the collection's type. For example: private {@literal @SynchronizedCollection} Map mMap =
* Collections.synchronizedMap(...);
*/
@Target({ ElementType.FIELD })
@Target({ElementType.FIELD})
@Retention(RetentionPolicy.CLASS)
public @interface SynchronizedCollection {
}
public @interface SynchronizedCollection {}

@ -17,12 +17,13 @@ import java.lang.annotation.Target;
* class/field/method are confined to the given thread name. For the thread name, you can either use
* the default constants UI/ANY or add your own.
*/
@Target({ ElementType.TYPE, ElementType.FIELD, ElementType.METHOD })
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD})
@Retention(RetentionPolicy.CLASS)
public @interface ThreadConfined {
String value(); /** the thread that the mutations should be confined to */
public static String UI = "UI"; /** confined to the UI thread */
public static String ANY = "ANY"; /** confined to any thread (but only that thread!) */
String value();
/** the thread that the mutations should be confined to */
public static String UI = "UI";
/** confined to the UI thread */
public static String ANY = "ANY";
/** confined to any thread (but only that thread!) */
}

@ -17,8 +17,7 @@ import java.lang.annotation.Target;
* applied to methods. In addition, you can ask Infer to assume thread-safety rather than checking
* it by using {@literal @ThreadSafe(enableChecks = false)}.
*/
@Target({ ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE })
@Target({ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE})
@Retention(RetentionPolicy.CLASS)
public @interface ThreadSafe {
boolean enableChecks() default true;

@ -12,9 +12,7 @@ import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
/**
* Annotation for a boolean function returning true when the argument is null.
*/
/** Annotation for a boolean function returning true when the argument is null. */
@Retention(RetentionPolicy.CLASS)
@Target({ElementType.METHOD})
public @interface TrueOnNull {}

@ -14,11 +14,9 @@ import java.lang.annotation.Target;
@Retention(RetentionPolicy.CLASS)
@Target({
ElementType.CONSTRUCTOR,
ElementType.METHOD,
ElementType.PACKAGE,
ElementType.TYPE,
ElementType.CONSTRUCTOR,
ElementType.METHOD,
ElementType.PACKAGE,
ElementType.TYPE,
})
public @interface Verify {
}
public @interface Verify {}

@ -10,28 +10,27 @@ package com.facebook.infer.builtins;
public class InferBuiltins {
public native static void __set_file_attribute(Object o);
public static native void __set_file_attribute(Object o);
public native static void __set_mem_attribute(Object o);
public static native void __set_mem_attribute(Object o);
public native static void __set_locked_attribute(Object o);
public static native void __set_locked_attribute(Object o);
public native static void __delete_locked_attribute(Object o);
public static native void __delete_locked_attribute(Object o);
public native static void _exit();
public static native void _exit();
private native static void __infer_assume(boolean condition);
private static native void __infer_assume(boolean condition);
public static void assume(boolean condition) {
__infer_assume(condition);
}
public static void assume(boolean condition) {
__infer_assume(condition);
}
// use this instead of "assume o != null". being non-null and allocated are different to Infer
public static void assume_allocated(Object o) {
assume(o != null);
o.hashCode();
}
public native static String __split_get_nth(String s, String sep, int n);
// use this instead of "assume o != null". being non-null and allocated are different to Infer
public static void assume_allocated(Object o) {
assume(o != null);
o.hashCode();
}
public static native String __split_get_nth(String s, String sep, int n);
}

@ -12,8 +12,7 @@ import java.io.Closeable;
public final class InferCloseables {
private InferCloseables() {
}
private InferCloseables() {}
public static void close(Closeable closeable) {
if (closeable != null) {
@ -24,5 +23,4 @@ public final class InferCloseables {
public static void closeQuietly(Closeable closeable) {
close(closeable);
}
}

@ -7,10 +7,10 @@
package com.facebook.infer.builtins;
/** WARNING! These methods are for testing the taint analysis only! Don't use them in models or in
/**
* WARNING! These methods are for testing the taint analysis only! Don't use them in models or in
* real code.
*/
public class InferTaint {
// these are to test whether we can add a taint spec to methods that have an implementation
@ -20,13 +20,10 @@ public class InferTaint {
return o;
}
public static void inferSensitiveSink(Object iMightBeTainted) {
}
public static void inferSensitiveSink(Object iMightBeTainted) {}
// these are to test whether we can add a taint spec to undefined methods
public static native Object inferSecretSourceUndefined();
public static native void inferSensitiveSinkUndefined(Object iMightBeTainted);
}

@ -12,149 +12,133 @@ import java.io.IOException;
import java.net.SocketException;
import java.sql.SQLException;
public class InferUndefined {
public static native boolean boolean_undefined();
public static native int int_undefined();
public static native long long_undefined();
public static native byte byte_undefined();
public static native void void_undefined();
public static native char char_undefined();
public static native short short_undefined();
public static native double double_undefined();
public static native float float_undefined();
public static native Object object_undefined();
public static void can_throw_ioexception_void() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
} else
throw new IOException();
}
public static boolean can_throw_ioexception_boolean() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return undef;
} else
throw new IOException();
}
public static int can_throw_ioexception_int() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return int_undefined();
} else
throw new IOException();
}
public static long can_throw_ioexception_long() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return long_undefined();
} else
throw new IOException();
}
public static byte can_throw_ioexception_byte() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return byte_undefined();
} else
throw new IOException();
}
public static short can_throw_ioexception_short() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return short_undefined();
} else
throw new IOException();
}
public static float can_throw_ioexception_float() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return float_undefined();
} else
throw new IOException();
}
public static double can_throw_ioexception_double() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return double_undefined();
} else
throw new IOException();
}
public static char can_throw_ioexception_char() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return char_undefined();
} else
throw new IOException();
}
public static String can_throw_ioexception_string() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return (String)object_undefined();
} else
throw new IOException();
}
public static Object can_throw_ioexception_object() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return object_undefined();
} else
throw new IOException();
}
public static void can_throw_sqlexception_void() throws SQLException {
boolean undef = boolean_undefined();
if (undef) {
} else
throw new SQLException();
}
public static int nonneg_int() {
int res = int_undefined();
InferBuiltins.assume(res >= 0);
return res;
}
public static void can_throw_socketexception_void() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
} else
throw new SocketException();
}
public static int can_throw_socketexception_int() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
return int_undefined();
} else
throw new SocketException();
}
public static Object can_throw_socketexception_object() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
return object_undefined();
} else
throw new SocketException();
}
public static native boolean boolean_undefined();
public static native int int_undefined();
public static native long long_undefined();
public static native byte byte_undefined();
public static native void void_undefined();
public static native char char_undefined();
public static native short short_undefined();
public static native double double_undefined();
public static native float float_undefined();
public static native Object object_undefined();
public static void can_throw_ioexception_void() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
} else throw new IOException();
}
public static boolean can_throw_ioexception_boolean() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return undef;
} else throw new IOException();
}
public static int can_throw_ioexception_int() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return int_undefined();
} else throw new IOException();
}
public static long can_throw_ioexception_long() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return long_undefined();
} else throw new IOException();
}
public static byte can_throw_ioexception_byte() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return byte_undefined();
} else throw new IOException();
}
public static short can_throw_ioexception_short() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return short_undefined();
} else throw new IOException();
}
public static float can_throw_ioexception_float() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return float_undefined();
} else throw new IOException();
}
public static double can_throw_ioexception_double() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return double_undefined();
} else throw new IOException();
}
public static char can_throw_ioexception_char() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return char_undefined();
} else throw new IOException();
}
public static String can_throw_ioexception_string() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return (String) object_undefined();
} else throw new IOException();
}
public static Object can_throw_ioexception_object() throws IOException {
boolean undef = boolean_undefined();
if (undef) {
return object_undefined();
} else throw new IOException();
}
public static void can_throw_sqlexception_void() throws SQLException {
boolean undef = boolean_undefined();
if (undef) {
} else throw new SQLException();
}
public static int nonneg_int() {
int res = int_undefined();
InferBuiltins.assume(res >= 0);
return res;
}
public static void can_throw_socketexception_void() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
} else throw new SocketException();
}
public static int can_throw_socketexception_int() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
return int_undefined();
} else throw new SocketException();
}
public static Object can_throw_socketexception_object() throws SocketException {
boolean undef = boolean_undefined();
if (undef) {
return object_undefined();
} else throw new SocketException();
}
}

@ -25,5 +25,4 @@ public class InferUtils {
|| charsetName == "UTF-16"
|| charsetName == "utf-16";
}
}

@ -10,39 +10,35 @@ package android.app;
import android.content.res.TypedArray;
import android.util.AttributeSet;
import android.view.ContextThemeWrapper;
import com.facebook.infer.builtins.InferUndefined;
public abstract class Activity extends ContextThemeWrapper {
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(int resid, int[] attrs)
throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
public TypedArray obtainStyledAttributes(int resid, int[] attrs) throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(AttributeSet set,
int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(
AttributeSet set, int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {
}
public NotFoundException(String name) {
super(name);
}
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
public NotFoundException(String name) {
super(name);
}
}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
}

@ -7,7 +7,6 @@
package android.app;
import android.app.PendingIntent;
public abstract class AlarmManager {

@ -12,20 +12,17 @@ import android.database.Cursor;
public class DownloadManager {
private ContentResolver mResolver;
private String mPackageName;
private ContentResolver mResolver;
private String mPackageName;
public DownloadManager(ContentResolver resolver, String packageName) {
mResolver = resolver;
mPackageName = packageName;
}
public static class Query {
}
public Cursor query(Query query) {
return mResolver.query(null, null, null, null, null);
}
public DownloadManager(ContentResolver resolver, String packageName) {
mResolver = resolver;
mPackageName = packageName;
}
public static class Query {}
public Cursor query(Query query) {
return mResolver.query(null, null, null, null, null);
}
}

@ -7,43 +7,44 @@
package android.content;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import android.database.Cursor;
import android.database.sqlite.SQLiteCursor;
import android.net.Uri;
import android.os.CancellationSignal;
import android.os.RemoteException;
import com.facebook.infer.builtins.InferUndefined;
public class ContentProviderClient {
private ContentResolver mContentResolver;
private IContentProvider mContentProvider;
private String mPackageName;
private boolean mStable;
ContentProviderClient(
ContentResolver contentResolver, IContentProvider contentProvider, boolean stable) {
mContentResolver = contentResolver;
mContentProvider = contentProvider;
mPackageName = (String)InferUndefined.object_undefined();
mStable = stable;
}
public Cursor query(Uri url, String[] projection, String selection,
String[] selectionArgs, String sortOrder) throws RemoteException {
return query(url, projection, selection, selectionArgs, sortOrder, null);
}
public Cursor query(Uri url, String[] projection, String selection, String[] selectionArgs,
String sortOrder, CancellationSignal cancellationSignal) throws RemoteException {
return new SQLiteCursor(null, null, null);
}
private class NotRespondingRunnable {
}
private ContentResolver mContentResolver;
private IContentProvider mContentProvider;
private String mPackageName;
private boolean mStable;
ContentProviderClient(
ContentResolver contentResolver, IContentProvider contentProvider, boolean stable) {
mContentResolver = contentResolver;
mContentProvider = contentProvider;
mPackageName = (String) InferUndefined.object_undefined();
mStable = stable;
}
public Cursor query(
Uri url, String[] projection, String selection, String[] selectionArgs, String sortOrder)
throws RemoteException {
return query(url, projection, selection, selectionArgs, sortOrder, null);
}
public Cursor query(
Uri url,
String[] projection,
String selection,
String[] selectionArgs,
String sortOrder,
CancellationSignal cancellationSignal)
throws RemoteException {
return new SQLiteCursor(null, null, null);
}
private class NotRespondingRunnable {}
}

@ -11,42 +11,44 @@ import android.database.Cursor;
import android.database.sqlite.SQLiteCursor;
import android.net.Uri;
import android.os.CancellationSignal;
import com.facebook.infer.builtins.InferUndefined;
public class ContentResolver {
private final Context mContext;
private final Context mContext;
public ContentResolver(Context context) {
mContext = context;
}
public ContentResolver(Context context) {
mContext = context;
}
public final Cursor query(Uri uri, String[] projection,
String selection, String[] selectionArgs, String sortOrder) {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return query(uri, projection, selection, selectionArgs, sortOrder, null);
}
public final Cursor query(
Uri uri, String[] projection, String selection, String[] selectionArgs, String sortOrder) {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return query(uri, projection, selection, selectionArgs, sortOrder, null);
}
public final Cursor query(final Uri uri, String[] projection,
String selection, String[] selectionArgs, String sortOrder,
CancellationSignal cancellationSignal) {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return new SQLiteCursor(null, null, null);
}
}
public final Cursor query(
final Uri uri,
String[] projection,
String selection,
String[] selectionArgs,
String sortOrder,
CancellationSignal cancellationSignal) {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return new SQLiteCursor(null, null, null);
}
}
public final ContentProviderClient acquireContentProviderClient(Uri uri) {
return new ContentProviderClient(this, null, true);
}
public final ContentProviderClient acquireContentProviderClient(Uri uri) {
return new ContentProviderClient(this, null, true);
}
public final ContentProviderClient acquireContentProviderClient(String name) {
return new ContentProviderClient(this, null, true);
}
public final ContentProviderClient acquireContentProviderClient(String name) {
return new ContentProviderClient(this, null, true);
}
}

@ -13,40 +13,35 @@ import com.facebook.infer.builtins.InferUndefined;
public class Context {
public ContentResolver getContentResolver() {
return new ContentResolver(this);
}
public ContentResolver getContentResolver() {
return new ContentResolver(this);
}
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(int resid, int[] attrs)
throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
public TypedArray obtainStyledAttributes(int resid, int[] attrs) throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(AttributeSet set,
int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(
AttributeSet set, int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {}
public NotFoundException(String name) {
super(name);
}
public NotFoundException(String name) {
super(name);
}
}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
}

@ -7,5 +7,4 @@
package android.content;
public interface IContentProvider {
}
public interface IContentProvider {}

@ -7,5 +7,4 @@
package android.content;
public interface IContentService {
}
public interface IContentService {}

@ -8,44 +8,37 @@
package android.content.res;
import android.util.AttributeSet;
import com.facebook.infer.builtins.InferUndefined;
public class Resources {
public final class Theme {
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(int resid, int[] attrs)
throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
}
public TypedArray obtainStyledAttributes(AttributeSet set,
int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
public final class Theme {
public TypedArray obtainStyledAttributes(int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {
}
public TypedArray obtainStyledAttributes(int resid, int[] attrs) throws NotFoundException {
if (InferUndefined.boolean_undefined()) {
throw new NotFoundException();
}
return new TypedArray(null, attrs, attrs, 1);
}
public NotFoundException(String name) {
super(name);
}
public TypedArray obtainStyledAttributes(
AttributeSet set, int[] attrs, int defStyleAttr, int defStyleRes) {
return new TypedArray(null, attrs, attrs, 1);
}
}
public static class NotFoundException extends RuntimeException {
public NotFoundException() {}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
public NotFoundException(String name) {
super(name);
}
}
public TypedArray obtainAttributes(AttributeSet set, int[] attrs) {
return new TypedArray(null, attrs, attrs, 1);
}
}

@ -11,28 +11,27 @@ import com.facebook.infer.builtins.InferBuiltins;
public class TypedArray {
private Resources mResources;
int[] mData;
int[] mIndices;
int mLength;
public void recycle() {
// Release resource
if (mLength > 0) {
InferBuiltins.__set_mem_attribute(this);
}
private Resources mResources;
int[] mData;
int[] mIndices;
int mLength;
public void recycle() {
// Release resource
if (mLength > 0) {
InferBuiltins.__set_mem_attribute(this);
}
}
public TypedArray(Resources resources, int[] data, int[] indices, int len) {
mResources = resources;
mData = data;
mIndices = indices;
mLength = len;
public TypedArray(Resources resources, int[] data, int[] indices, int len) {
mResources = resources;
mData = data;
mIndices = indices;
mLength = len;
// Acquire resource
if (mLength > 0) {
InferBuiltins.__set_file_attribute(this);
}
// Acquire resource
if (mLength > 0) {
InferBuiltins.__set_file_attribute(this);
}
}
}

@ -7,5 +7,4 @@
package android.database;
public abstract class AbstractCursor implements CrossProcessCursor {
}
public abstract class AbstractCursor implements CrossProcessCursor {}

@ -7,5 +7,4 @@
package android.database;
public interface CrossProcessCursor extends Cursor {
}
public interface CrossProcessCursor extends Cursor {}

@ -7,5 +7,4 @@
package android.database;
public abstract class CrossProcessCursorWrapper implements CrossProcessCursor {
}
public abstract class CrossProcessCursorWrapper implements CrossProcessCursor {}

@ -7,8 +7,6 @@
package android.database;
import com.facebook.infer.builtins.InferUndefined;
import com.facebook.infer.builtins.InferBuiltins;
import java.io.IOException;
@ -22,7 +20,7 @@ public class CursorWrapper implements Cursor {
public void close() {
try {
mCursor.close();
} catch (IOException e) {}
} catch (IOException e) {
}
}
}

@ -7,6 +7,4 @@
package android.database.sqlite;
public final class SQLiteConnectionPool {
}
public final class SQLiteConnectionPool {}

@ -9,24 +9,20 @@ package android.database.sqlite;
import android.database.Cursor;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
public class SQLiteCursor implements Cursor {
@Deprecated
public SQLiteCursor(SQLiteDatabase db, SQLiteCursorDriver driver,
String editTable, SQLiteQuery query) {
this(driver, editTable, query);
}
public SQLiteCursor(SQLiteCursorDriver driver, String editTable, SQLiteQuery query) {
InferBuiltins.__set_file_attribute(this);
}
@Deprecated
public SQLiteCursor(
SQLiteDatabase db, SQLiteCursorDriver driver, String editTable, SQLiteQuery query) {
this(driver, editTable, query);
}
public void close() {
InferBuiltins.__set_mem_attribute(this);
}
public SQLiteCursor(SQLiteCursorDriver driver, String editTable, SQLiteQuery query) {
InferBuiltins.__set_file_attribute(this);
}
public void close() {
InferBuiltins.__set_mem_attribute(this);
}
}

@ -11,86 +11,159 @@ import android.database.Cursor;
import android.database.DatabaseErrorHandler;
import android.os.CancellationSignal;
public final class SQLiteDatabase {
private SQLiteDatabase(String path, int openFlags, CursorFactory cursorFactory,
DatabaseErrorHandler errorHandler) {
}
public Cursor query(boolean distinct, String table, String[] columns,
String selection, String[] selectionArgs, String groupBy,
String having, String orderBy, String limit) {
return queryWithFactory(null, distinct, table, columns, selection, selectionArgs,
groupBy, having, orderBy, limit, null);
}
public Cursor query(boolean distinct, String table, String[] columns,
String selection, String[] selectionArgs, String groupBy,
String having, String orderBy, String limit, CancellationSignal cancellationSignal) {
return queryWithFactory(null, distinct, table, columns, selection, selectionArgs,
groupBy, having, orderBy, limit, cancellationSignal);
}
public Cursor queryWithFactory(CursorFactory cursorFactory,
boolean distinct, String table, String[] columns,
String selection, String[] selectionArgs, String groupBy,
String having, String orderBy, String limit) {
return queryWithFactory(cursorFactory, distinct, table, columns, selection,
selectionArgs, groupBy, having, orderBy, limit, null);
}
public Cursor queryWithFactory(CursorFactory cursorFactory,
boolean distinct, String table, String[] columns,
String selection, String[] selectionArgs, String groupBy,
String having, String orderBy, String limit, CancellationSignal cancellationSignal) {
return rawQueryWithFactory(cursorFactory, null, selectionArgs, table, cancellationSignal);
}
public Cursor query(String table, String[] columns, String selection,
String[] selectionArgs, String groupBy, String having,
String orderBy) {
return query(false, table, columns, selection, selectionArgs, groupBy,
having, orderBy, null /* limit */);
}
public Cursor query(String table, String[] columns, String selection,
String[] selectionArgs, String groupBy, String having,
String orderBy, String limit) {
return query(false, table, columns, selection, selectionArgs, groupBy,
having, orderBy, limit);
}
public Cursor rawQuery(String sql, String[] selectionArgs) {
return rawQueryWithFactory(null, sql, selectionArgs, null, null);
}
public Cursor rawQuery(String sql, String[] selectionArgs,
CancellationSignal cancellationSignal) {
return rawQueryWithFactory(null, sql, selectionArgs, null, cancellationSignal);
}
public Cursor rawQueryWithFactory(
CursorFactory cursorFactory, String sql, String[] selectionArgs,
String editTable) {
return rawQueryWithFactory(cursorFactory, sql, selectionArgs, editTable, null);
}
public Cursor rawQueryWithFactory(
CursorFactory cursorFactory, String sql, String[] selectionArgs,
String editTable, CancellationSignal cancellationSignal) {
return new SQLiteCursor(null, editTable, null);
}
public interface CursorFactory {
public Cursor newCursor(SQLiteDatabase db,
SQLiteCursorDriver masterQuery, String editTable,
SQLiteQuery query);
}
private SQLiteDatabase(
String path, int openFlags, CursorFactory cursorFactory, DatabaseErrorHandler errorHandler) {}
public Cursor query(
boolean distinct,
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy,
String limit) {
return queryWithFactory(
null,
distinct,
table,
columns,
selection,
selectionArgs,
groupBy,
having,
orderBy,
limit,
null);
}
public Cursor query(
boolean distinct,
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy,
String limit,
CancellationSignal cancellationSignal) {
return queryWithFactory(
null,
distinct,
table,
columns,
selection,
selectionArgs,
groupBy,
having,
orderBy,
limit,
cancellationSignal);
}
public Cursor queryWithFactory(
CursorFactory cursorFactory,
boolean distinct,
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy,
String limit) {
return queryWithFactory(
cursorFactory,
distinct,
table,
columns,
selection,
selectionArgs,
groupBy,
having,
orderBy,
limit,
null);
}
public Cursor queryWithFactory(
CursorFactory cursorFactory,
boolean distinct,
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy,
String limit,
CancellationSignal cancellationSignal) {
return rawQueryWithFactory(cursorFactory, null, selectionArgs, table, cancellationSignal);
}
public Cursor query(
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy) {
return query(
false,
table,
columns,
selection,
selectionArgs,
groupBy,
having,
orderBy,
null /* limit */);
}
public Cursor query(
String table,
String[] columns,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String orderBy,
String limit) {
return query(false, table, columns, selection, selectionArgs, groupBy, having, orderBy, limit);
}
public Cursor rawQuery(String sql, String[] selectionArgs) {
return rawQueryWithFactory(null, sql, selectionArgs, null, null);
}
public Cursor rawQuery(
String sql, String[] selectionArgs, CancellationSignal cancellationSignal) {
return rawQueryWithFactory(null, sql, selectionArgs, null, cancellationSignal);
}
public Cursor rawQueryWithFactory(
CursorFactory cursorFactory, String sql, String[] selectionArgs, String editTable) {
return rawQueryWithFactory(cursorFactory, sql, selectionArgs, editTable, null);
}
public Cursor rawQueryWithFactory(
CursorFactory cursorFactory,
String sql,
String[] selectionArgs,
String editTable,
CancellationSignal cancellationSignal) {
return new SQLiteCursor(null, editTable, null);
}
public interface CursorFactory {
public Cursor newCursor(
SQLiteDatabase db, SQLiteCursorDriver masterQuery, String editTable, SQLiteQuery query);
}
}

@ -7,5 +7,4 @@
package android.database.sqlite;
public final class SQLiteDatabaseConfiguration {
}
public final class SQLiteDatabaseConfiguration {}

@ -12,26 +12,49 @@ import android.os.CancellationSignal;
public class SQLiteQueryBuilder {
public Cursor query(SQLiteDatabase db, String[] projectionIn,
String selection, String[] selectionArgs, String groupBy,
String having, String sortOrder) {
return query(db, projectionIn, selection, selectionArgs, groupBy, having, sortOrder,
null /* limit */, null /* cancellationSignal */);
}
public Cursor query(SQLiteDatabase db, String[] projectionIn,
String selection, String[] selectionArgs, String groupBy,
String having, String sortOrder, String limit) {
return query(db, projectionIn, selection, selectionArgs,
groupBy, having, sortOrder, limit, null);
}
public Cursor query(SQLiteDatabase db, String[] projectionIn,
String selection, String[] selectionArgs, String groupBy,
String having, String sortOrder, String limit,
CancellationSignal cancellationSignal) {
return new SQLiteCursor(null, null, null);
}
public Cursor query(
SQLiteDatabase db,
String[] projectionIn,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String sortOrder) {
return query(
db,
projectionIn,
selection,
selectionArgs,
groupBy,
having,
sortOrder,
null /* limit */,
null /* cancellationSignal */);
}
public Cursor query(
SQLiteDatabase db,
String[] projectionIn,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String sortOrder,
String limit) {
return query(
db, projectionIn, selection, selectionArgs, groupBy, having, sortOrder, limit, null);
}
public Cursor query(
SQLiteDatabase db,
String[] projectionIn,
String selection,
String[] selectionArgs,
String groupBy,
String having,
String sortOrder,
String limit,
CancellationSignal cancellationSignal) {
return new SQLiteCursor(null, null, null);
}
}

@ -13,23 +13,27 @@ import android.net.Uri;
public final class MediaStore {
public static final class Images {
public static final class Media {
public static final Cursor query(ContentResolver cr, Uri uri, String[] projection) {
return cr.query(uri, projection, null, null, null);
}
public static final Cursor query(ContentResolver cr, Uri uri, String[] projection,
String where, String orderBy) {
return cr.query(uri, projection, where, null, orderBy);
}
public static final Cursor query(ContentResolver cr, Uri uri, String[] projection,
String selection, String[] selectionArgs, String orderBy) {
return cr.query(uri, projection, selection, selectionArgs, orderBy);
}
}
public static final class Images {
public static final class Media {
public static final Cursor query(ContentResolver cr, Uri uri, String[] projection) {
return cr.query(uri, projection, null, null, null);
}
public static final Cursor query(
ContentResolver cr, Uri uri, String[] projection, String where, String orderBy) {
return cr.query(uri, projection, where, null, orderBy);
}
public static final Cursor query(
ContentResolver cr,
Uri uri,
String[] projection,
String selection,
String[] selectionArgs,
String orderBy) {
return cr.query(uri, projection, selection, selectionArgs, orderBy);
}
}
}
}

@ -18,11 +18,11 @@
package android.text;
public class TextUtils {
public static boolean isEmpty(CharSequence str) {
if (str == null || str.length() == 0) {
return true;
} else {
return false;
}
public static boolean isEmpty(CharSequence str) {
if (str == null || str.length() == 0) {
return true;
} else {
return false;
}
}
}

@ -8,7 +8,6 @@
package com.facebook.infer.annotation;
import com.facebook.infer.builtins.InferBuiltins;
import javax.annotation.Nullable;
public class Assertions {

@ -9,7 +9,6 @@ package com.fasterxml.jackson.core;
import com.fasterxml.jackson.core.json.PackageVersion;
import com.fasterxml.jackson.core.json.UTF8StreamJsonParser;
import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;
@ -17,47 +16,35 @@ import java.io.InputStream;
import java.io.Reader;
import java.net.URL;
public class JsonFactory
implements Versioned, java.io.Serializable {
@Override
public Version version() {
return PackageVersion.VERSION;
}
public JsonParser createParser(File f)
throws IOException, JsonParseException {
return createOwningParser();
}
public JsonParser createParser(URL url)
throws IOException, JsonParseException {
return createOwningParser();
}
public JsonParser createParser(InputStream in)
throws IOException, JsonParseException {
return createNonOwningParser();
}
public JsonParser createParser(Reader r)
throws IOException, JsonParseException {
return createNonOwningParser();
}
private JsonParser createOwningParser()
throws IOException, JsonParseException {
InputStream in = new FileInputStream("");
return new UTF8StreamJsonParser(null, 0, in, null, null,
new byte[]{}, 0, 0,
false);
}
private JsonParser createNonOwningParser()
throws IOException, JsonParseException {
return new UTF8StreamJsonParser(null, 0, null, null, null,
new byte[]{}, 0, 0,
false);
}
public class JsonFactory implements Versioned, java.io.Serializable {
@Override
public Version version() {
return PackageVersion.VERSION;
}
public JsonParser createParser(File f) throws IOException, JsonParseException {
return createOwningParser();
}
public JsonParser createParser(URL url) throws IOException, JsonParseException {
return createOwningParser();
}
public JsonParser createParser(InputStream in) throws IOException, JsonParseException {
return createNonOwningParser();
}
public JsonParser createParser(Reader r) throws IOException, JsonParseException {
return createNonOwningParser();
}
private JsonParser createOwningParser() throws IOException, JsonParseException {
InputStream in = new FileInputStream("");
return new UTF8StreamJsonParser(null, 0, in, null, null, new byte[] {}, 0, 0, false);
}
private JsonParser createNonOwningParser() throws IOException, JsonParseException {
return new UTF8StreamJsonParser(null, 0, null, null, null, new byte[] {}, 0, 0, false);
}
}

@ -9,32 +9,27 @@ package com.fasterxml.jackson.core;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.io.Closeable;
import java.io.IOException;
public abstract class JsonParser
implements Closeable, Versioned {
public abstract class JsonParser implements Closeable, Versioned {
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
private void throwExceptions()
throws JsonParseException, IOException {
if (InferUndefined.boolean_undefined()) {
throw new JsonParseException(null, null, null);
}
if (InferUndefined.boolean_undefined()) {
throw new IOException();
}
private void throwExceptions() throws JsonParseException, IOException {
if (InferUndefined.boolean_undefined()) {
throw new JsonParseException(null, null, null);
}
public Object readValueAs(Class valueType)
throws IOException, JsonProcessingException {
throwExceptions();
return InferUndefined.object_undefined();
if (InferUndefined.boolean_undefined()) {
throw new IOException();
}
}
public Object readValueAs(Class valueType) throws IOException, JsonProcessingException {
throwExceptions();
return InferUndefined.object_undefined();
}
}

@ -15,7 +15,6 @@ import com.fasterxml.jackson.core.ObjectCodec;
import com.fasterxml.jackson.core.base.ParserBase;
import com.fasterxml.jackson.core.io.IOContext;
import com.fasterxml.jackson.core.sym.BytesToNameCanonicalizer;
import java.io.IOException;
import java.io.InputStream;
@ -24,120 +23,114 @@ import java.io.InputStream;
* This class contains a minimum set of methods in order to compile it for the
* models
*/
public final class UTF8StreamJsonParser
extends ParserBase {
protected ObjectCodec _objectCodec;
protected BytesToNameCanonicalizer _symbols;
protected int[] _quadBuffer;
protected boolean _tokenIncomplete;
protected InputStream _inputStream;
protected byte[] _inputBuffer;
protected boolean _bufferRecyclable;
public UTF8StreamJsonParser(IOContext ctxt, int features, InputStream in,
ObjectCodec codec, BytesToNameCanonicalizer sym,
byte[] inputBuffer, int start, int end,
boolean bufferRecyclable) {
super(ctxt, features);
_inputStream = in;
_objectCodec = codec;
_symbols = sym;
_inputBuffer = inputBuffer;
_inputPtr = start;
_inputEnd = end;
_bufferRecyclable = bufferRecyclable;
}
@Override
public void close() throws IOException {
if (_inputStream != null) {
_inputStream.close();
}
}
private void throwExceptions()
throws JsonParseException, IOException {
if (InferUndefined.boolean_undefined()) {
throw new JsonParseException(null, null, null);
}
if (InferUndefined.boolean_undefined()) {
throw new IOException();
}
}
/*
* Methods from ParserBase
*/
@Override
protected boolean loadMore()
throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
@Override
protected void _finishString()
throws IOException, JsonParseException {
throwExceptions();
}
@Override
protected void _closeInput() throws IOException {
close();
}
/*
* Methods from ParserMinimalBase
*/
@Override
public byte[] getBinaryValue(Base64Variant b64variant)
throws IOException, JsonParseException {
throwExceptions();
return new byte[]{InferUndefined.byte_undefined()};
public final class UTF8StreamJsonParser extends ParserBase {
protected ObjectCodec _objectCodec;
protected BytesToNameCanonicalizer _symbols;
protected int[] _quadBuffer;
protected boolean _tokenIncomplete;
protected InputStream _inputStream;
protected byte[] _inputBuffer;
protected boolean _bufferRecyclable;
public UTF8StreamJsonParser(
IOContext ctxt,
int features,
InputStream in,
ObjectCodec codec,
BytesToNameCanonicalizer sym,
byte[] inputBuffer,
int start,
int end,
boolean bufferRecyclable) {
super(ctxt, features);
_inputStream = in;
_objectCodec = codec;
_symbols = sym;
_inputBuffer = inputBuffer;
_inputPtr = start;
_inputEnd = end;
_bufferRecyclable = bufferRecyclable;
}
@Override
public void close() throws IOException {
if (_inputStream != null) {
_inputStream.close();
}
}
@Override
public int getTextOffset()
throws IOException, JsonParseException {
throwExceptions();
return InferUndefined.int_undefined();
private void throwExceptions() throws JsonParseException, IOException {
if (InferUndefined.boolean_undefined()) {
throw new JsonParseException(null, null, null);
}
@Override
public int getTextLength()
throws IOException, JsonParseException {
throwExceptions();
return InferUndefined.int_undefined();
}
@Override
public char[] getTextCharacters()
throws IOException, JsonParseException {
throwExceptions();
return new char[]{InferUndefined.char_undefined()};
}
@Override
public String getText()
throws IOException, JsonParseException {
throwExceptions();
return (String)InferUndefined.object_undefined();
}
@Override
public JsonToken nextToken()
throws IOException, JsonParseException {
throwExceptions();
throw new IOException();
if (InferUndefined.boolean_undefined()) {
throw new IOException();
}
}
/*
* Methods from ParserBase
*/
@Override
protected boolean loadMore() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
@Override
protected void _finishString() throws IOException, JsonParseException {
throwExceptions();
}
@Override
protected void _closeInput() throws IOException {
close();
}
/*
* Methods from ParserMinimalBase
*/
@Override
public byte[] getBinaryValue(Base64Variant b64variant) throws IOException, JsonParseException {
throwExceptions();
return new byte[] {InferUndefined.byte_undefined()};
}
@Override
public int getTextOffset() throws IOException, JsonParseException {
throwExceptions();
return InferUndefined.int_undefined();
}
@Override
public int getTextLength() throws IOException, JsonParseException {
throwExceptions();
return InferUndefined.int_undefined();
}
@Override
public char[] getTextCharacters() throws IOException, JsonParseException {
throwExceptions();
return new char[] {InferUndefined.char_undefined()};
}
@Override
public String getText() throws IOException, JsonParseException {
throwExceptions();
return (String) InferUndefined.object_undefined();
}
@Override
public JsonToken nextToken() throws IOException, JsonParseException {
throwExceptions();
throw new IOException();
}
}

@ -9,9 +9,8 @@ package com.google.common.base;
import javax.annotation.Nullable;
public abstract class Optional<T> {
public abstract class Optional<T> {
@Nullable
public abstract T orNull();
}

@ -7,9 +7,9 @@
package com.google.common.base;
import javax.annotation.Nullable;
import static com.facebook.infer.builtins.InferBuiltins.assume;
import javax.annotation.Nullable;
public final class Preconditions {
@ -22,9 +22,8 @@ public final class Preconditions {
return checkNotNull(reference);
}
public static <T> T checkNotNull(T reference,
@Nullable String errorMessageTemplate,
@Nullable Object... errorMessageArgs) {
public static <T> T checkNotNull(
T reference, @Nullable String errorMessageTemplate, @Nullable Object... errorMessageArgs) {
return checkNotNull(reference);
}
@ -32,14 +31,14 @@ public final class Preconditions {
assume(expression);
}
public static void checkState(boolean expression,
@Nullable Object errorMessage) {
public static void checkState(boolean expression, @Nullable Object errorMessage) {
assume(expression);
}
public static void checkState(boolean expression,
@Nullable String errorMessageTemplate,
@Nullable Object... errorMessageArgs) {
public static void checkState(
boolean expression,
@Nullable String errorMessageTemplate,
@Nullable Object... errorMessageArgs) {
assume(expression);
}
@ -57,5 +56,4 @@ public final class Preconditions {
@Nullable Object... errorMessageArgs) {
assume(expression);
}
}

@ -7,10 +7,8 @@
package com.google.common.collect;
import java.util.NoSuchElementException;
import com.facebook.infer.builtins.InferBuiltins;
import java.util.NoSuchElementException;
import javax.annotation.Nullable;
public class Iterators {
@ -35,5 +33,4 @@ public class Iterators {
}
};
}
}

@ -9,20 +9,17 @@ package com.google.common.io;
import com.facebook.infer.builtins.InferCloseables;
import com.facebook.infer.builtins.InferUndefined;
import java.io.Closeable;
import java.io.IOException;
public final class Closeables {
public static void close(Closeable closeable, boolean swallowIOException) throws IOException {
InferCloseables.close(closeable);
if (!swallowIOException)
InferUndefined.can_throw_ioexception_void();
}
public static void closeQuietly(Closeable closeable) {
InferCloseables.closeQuietly(closeable);
}
public static void close(Closeable closeable, boolean swallowIOException) throws IOException {
InferCloseables.close(closeable);
if (!swallowIOException) InferUndefined.can_throw_ioexception_void();
}
public static void closeQuietly(Closeable closeable) {
InferCloseables.closeQuietly(closeable);
}
}

@ -7,10 +7,9 @@
package dalvik.system;
public class CloseGuard {
public static interface Reporter {
public void report(String message, Throwable allocationSite);
}
public static interface Reporter {
public void report(String message, Throwable allocationSite);
}
}

@ -34,5 +34,4 @@ public class BufferedInputStream {
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
}

@ -11,34 +11,33 @@ import com.facebook.infer.builtins.InferUndefined;
public class BufferedOutputStream extends FilterOutputStream {
public BufferedOutputStream(OutputStream out) {
super(out);
}
public BufferedOutputStream(OutputStream out) {
super(out);
}
public BufferedOutputStream(OutputStream out, int size) {
super(out);
}
public BufferedOutputStream(OutputStream out, int size) {
super(out);
}
public void close() throws IOException {
if (out != null) {
out.close();
}
public void close() throws IOException {
if (out != null) {
out.close();
}
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -9,35 +9,33 @@ package java.io;
import com.facebook.infer.builtins.InferUndefined;
public abstract class BufferedWriter extends Writer {
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void newLine() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void newLine() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -9,75 +9,73 @@ package java.io;
import com.facebook.infer.builtins.InferUndefined;
public class DataInputStream {
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[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final boolean readBoolean() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public int read(byte b[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final byte readByte() throws IOException {
return InferUndefined.can_throw_ioexception_byte();
}
public final boolean readBoolean() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public final char readChar() throws IOException {
return InferUndefined.can_throw_ioexception_char();
}
public final byte readByte() throws IOException {
return InferUndefined.can_throw_ioexception_byte();
}
public final double readDouble() throws IOException {
return InferUndefined.can_throw_ioexception_double();
}
public final char readChar() throws IOException {
return InferUndefined.can_throw_ioexception_char();
}
public final float readFloat() throws IOException {
return InferUndefined.can_throw_ioexception_float();
}
public final double readDouble() throws IOException {
return InferUndefined.can_throw_ioexception_double();
}
public final void readFully(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final float readFloat() throws IOException {
return InferUndefined.can_throw_ioexception_float();
}
public final void readFully(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void readFully(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final int readInt() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final void readFully(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final long readLong() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public final int readInt() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final short readShort() throws IOException {
return InferUndefined.can_throw_ioexception_short();
}
public final long readLong() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public final int readUnsignedByte() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final short readShort() throws IOException {
return InferUndefined.can_throw_ioexception_short();
}
public final int readUnsignedShort() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final int readUnsignedByte() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final String readUTF() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final int readUnsignedShort() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public static final String readUTF(DataInput in) throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final String readUTF() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final int skipBytes(int n) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public static final String readUTF(DataInput in) throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final int skipBytes(int n) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
}

@ -9,71 +9,69 @@ package java.io;
import com.facebook.infer.builtins.InferUndefined;
public class DataOutputStream extends FilterOutputStream {
public DataOutputStream(OutputStream out) {
super(out);
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public DataOutputStream(OutputStream out) {
super(out);
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBoolean(boolean v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeByte(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBoolean(boolean v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBytes(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeByte(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChar(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBytes(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChars(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChar(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeDouble(double v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChars(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeFloat(float v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeDouble(double v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeInt(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeFloat(float v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeLong(long v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeInt(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeShort(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeLong(long v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeShort(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -12,12 +12,11 @@ import javax.annotation.Nullable;
public class File {
public @Nullable File[] listFiles() {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return (File[])InferUndefined.object_undefined();
}
public @Nullable File[] listFiles() {
if (InferUndefined.boolean_undefined()) {
return null;
} else {
return (File[]) InferUndefined.object_undefined();
}
}
}

@ -9,70 +9,67 @@ package java.io;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.nio.FileChannelImpl;
import java.nio.channels.FileChannel;
public class FileInputStream extends InputStream {
private FileDescriptor fd;
private FileChannel channel;
private void init() {
InferBuiltins.__set_file_attribute(this);
}
public FileInputStream(String name) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileInputStream(File file) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileInputStream(FileDescriptor fdObj) {
init();
}
public void close() throws IOException {
super.close();
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public int available() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
private FileDescriptor fd;
private FileChannel channel;
@Override
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
private void init() {
InferBuiltins.__set_file_attribute(this);
}
@Override
public int read(byte b[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
public FileInputStream(String name) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
@Override
public int read(byte b[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
public FileInputStream(File file) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
public long skip(int n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
}
public FileInputStream(FileDescriptor fdObj) {
init();
}
public void close() throws IOException {
super.close();
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public int available() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
@Override
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
@Override
public int read(byte b[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
@Override
public int read(byte b[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public long skip(int n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
}

@ -9,77 +9,73 @@ package java.io;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.nio.FileChannelImpl;
import java.nio.channels.FileChannel;
public class FileOutputStream extends OutputStream {
private FileDescriptor fd;
private FileChannel channel;
private FileDescriptor fd;
private FileChannel channel;
private void init() {
InferBuiltins.__set_file_attribute(this);
}
public FileOutputStream(String name) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
private void init() {
InferBuiltins.__set_file_attribute(this);
}
public FileOutputStream(String name, boolean append) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
public FileOutputStream(String name) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileOutputStream(File file) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
public FileOutputStream(String name, boolean append) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileOutputStream(File file, boolean append)
throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
public FileOutputStream(File file) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileOutputStream(FileDescriptor fdObj) {
init();
public FileOutputStream(File file, boolean append) throws FileNotFoundException {
if (InferUndefined.boolean_undefined()) {
init();
} else {
throw new FileNotFoundException();
}
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public FileOutputStream(FileDescriptor fdObj) {
init();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
}

@ -11,29 +11,27 @@ import com.facebook.infer.builtins.InferUndefined;
public class FilterInputStream {
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 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 void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
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();
}
}

@ -11,36 +11,33 @@ import com.facebook.infer.builtins.InferUndefined;
public class FilterOutputStream {
protected OutputStream out;
protected OutputStream out;
public FilterOutputStream() {
}
public FilterOutputStream(OutputStream out) {
this.out = out;
}
public void close() throws IOException {
if (out != null) {
out.close();
}
}
public FilterOutputStream() {}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public FilterOutputStream(OutputStream out) {
this.out = out;
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
public void close() throws IOException {
if (out != null) {
out.close();
}
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -11,28 +11,27 @@ import com.facebook.infer.builtins.InferUndefined;
public abstract class FilterReader {
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(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
}

@ -12,21 +12,20 @@ import com.facebook.infer.builtins.InferUndefined;
public class InputStream {
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
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 void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
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();
}
}

@ -11,37 +11,29 @@ import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import com.facebook.infer.builtins.InferUtils;
import java.nio.charset.Charset;
import java.nio.charset.CharsetDecoder;
public abstract class InputStreamReader {
public InputStreamReader(InputStream in, String charsetName)
throws UnsupportedEncodingException {
if (charsetName == null)
throw new NullPointerException("charsetName");
else if (InferUtils.isValidCharset(charsetName)) {
InferBuiltins.__set_mem_attribute(in);
InferBuiltins.__set_file_attribute(this);
} else
throw new UnsupportedEncodingException();
}
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char[] cbuf, int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public InputStreamReader(InputStream in, String charsetName) throws UnsupportedEncodingException {
if (charsetName == null) throw new NullPointerException("charsetName");
else if (InferUtils.isValidCharset(charsetName)) {
InferBuiltins.__set_mem_attribute(in);
InferBuiltins.__set_file_attribute(this);
} else throw new UnsupportedEncodingException();
}
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char[] cbuf, int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
}

@ -7,10 +7,8 @@
package java.io;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
public class ObjectInputStream {
InputStream in;
@ -26,8 +24,7 @@ public class ObjectInputStream {
}
}
protected ObjectInputStream() throws IOException, SecurityException {
}
protected ObjectInputStream() throws IOException, SecurityException {}
public int available() throws IOException {
return InferUndefined.can_throw_ioexception_int();
@ -117,7 +114,5 @@ public class ObjectInputStream {
return InferUndefined.can_throw_ioexception_int();
}
public static abstract class GetField {
}
public abstract static class GetField {}
}

@ -11,94 +11,94 @@ import com.facebook.infer.builtins.InferUndefined;
public class ObjectOutputStream extends OutputStream {
private DataOutputStream output;
private DataOutputStream output;
public ObjectOutputStream(OutputStream out) throws IOException {
this.output = new DataOutputStream(out);
InferUndefined.can_throw_ioexception_void();
}
public ObjectOutputStream(OutputStream out) throws IOException {
this.output = new DataOutputStream(out);
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
output.close();
}
public void close() throws IOException {
output.close();
}
public void defaultWriteObject() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void defaultWriteObject() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeBoolean(boolean val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeBoolean(boolean val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeByte(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeByte(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeBytes(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeBytes(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeChar(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeChar(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeChars(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeChars(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeDouble(double val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeDouble(double val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeFields() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeFields() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeFloat(float val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeFloat(float val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeInt(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeInt(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeLong(long val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeLong(long val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeObject(Object obj) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeObject(Object obj) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeShort(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeShort(int val) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeUnshared(Object obj) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeUnshared(Object obj) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -31,5 +31,4 @@ public class OutputStream {
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
}
}

@ -11,43 +11,37 @@ import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import com.facebook.infer.builtins.InferUtils;
import java.nio.charset.Charset;
import java.nio.charset.CharsetEncoder;
public class OutputStreamWriter extends Writer {
public OutputStreamWriter(OutputStream out, String charsetName)
throws UnsupportedEncodingException {
if (charsetName == null)
throw new NullPointerException("charsetName");
else if (InferUtils.isValidCharset(charsetName)) {
InferBuiltins.__set_file_attribute(this);
} else
throw new UnsupportedEncodingException();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public OutputStreamWriter(OutputStream out, String charsetName)
throws UnsupportedEncodingException {
if (charsetName == null) throw new NullPointerException("charsetName");
else if (InferUtils.isValidCharset(charsetName)) {
InferBuiltins.__set_file_attribute(this);
} else throw new UnsupportedEncodingException();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -12,46 +12,44 @@ import com.facebook.infer.builtins.InferUndefined;
public class PipedInputStream extends InputStream {
public PipedInputStream(PipedOutputStream src) throws IOException {
this();
}
public PipedInputStream(PipedOutputStream src, int pipeSize)
throws IOException {
this();
}
public PipedInputStream() {
InferBuiltins.__set_file_attribute(this);
}
public PipedInputStream(int pipeSize) {
this();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void connect(PipedOutputStream src) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public int available() 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[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public PipedInputStream(PipedOutputStream src) throws IOException {
this();
}
public PipedInputStream(PipedOutputStream src, int pipeSize) throws IOException {
this();
}
public PipedInputStream() {
InferBuiltins.__set_file_attribute(this);
}
public PipedInputStream(int pipeSize) {
this();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void connect(PipedOutputStream src) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public int available() 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[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
}

@ -12,37 +12,36 @@ import com.facebook.infer.builtins.InferUndefined;
public class PipedOutputStream extends OutputStream {
public PipedOutputStream(PipedInputStream snk) throws IOException {
InferBuiltins.__set_file_attribute(this);
}
public PipedOutputStream() {
InferBuiltins.__set_file_attribute(this);
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void connect(PipedInputStream snk) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public PipedOutputStream(PipedInputStream snk) throws IOException {
InferBuiltins.__set_file_attribute(this);
}
public PipedOutputStream() {
InferBuiltins.__set_file_attribute(this);
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void connect(PipedInputStream snk) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -12,56 +12,53 @@ import com.facebook.infer.builtins.InferUndefined;
public class PipedReader extends Reader {
private void init() throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
private void init() throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
public PipedReader() {
}
public PipedReader() {}
public PipedReader(int pipeSize) {
}
public PipedReader(int pipeSize) {}
public PipedReader(PipedWriter src) throws IOException {
init();
}
public PipedReader(PipedWriter src) throws IOException {
init();
}
public PipedReader(PipedWriter src, int pipeSize) throws IOException {
init();
}
public PipedReader(PipedWriter src, int pipeSize) throws IOException {
init();
}
public void connect(PipedWriter src) throws IOException {
init();
}
public void connect(PipedWriter src) throws IOException {
init();
}
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(char[] cbuf, int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char[] cbuf, int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public void mark(int readAheadLimit) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void mark(int readAheadLimit) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
}

@ -12,65 +12,62 @@ import com.facebook.infer.builtins.InferUndefined;
public abstract class PipedWriter extends Writer {
private void init() throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
public PipedWriter() {
}
public PipedWriter(PipedReader snk) throws IOException {
init();
}
public void connect(PipedReader snk) throws IOException {
init();
}
public Writer append(char c) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq, int start, int end)
throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
private void init() throws IOException {
InferUndefined.can_throw_ioexception_void();
InferBuiltins.__set_file_attribute(this);
}
public PipedWriter() {}
public PipedWriter(PipedReader snk) throws IOException {
init();
}
public void connect(PipedReader snk) throws IOException {
init();
}
public Writer append(char c) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq, int start, int end) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
}

@ -32,8 +32,7 @@ public abstract class PrintWriter {
return this;
}
public PrintWriter append(CharSequence csq, int start, int end)
throws IOException {
public PrintWriter append(CharSequence csq, int start, int end) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
@ -68,5 +67,4 @@ public abstract class PrintWriter {
mOutputStream.close();
}
}
}

@ -9,7 +9,6 @@ package java.io;
import com.facebook.infer.builtins.InferUndefined;
public class PushbackInputStream {
public int available() throws IOException {
@ -47,5 +46,4 @@ public class PushbackInputStream {
public void unread(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -11,40 +11,39 @@ import com.facebook.infer.builtins.InferUndefined;
public abstract class PushbackReader {
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(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
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();
}
public void unread(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void unread(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void unread(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void unread(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void unread(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void unread(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -9,165 +9,161 @@ package java.io;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.nio.FileChannelImpl;
import java.nio.channels.FileChannel;
public class RandomAccessFile implements Closeable {
private FileDescriptor fd;
private FileChannel channel;
private FileDescriptor fd;
private FileChannel channel;
public RandomAccessFile(String name, String mode)
throws FileNotFoundException {
InferBuiltins.__set_file_attribute(this);
}
public RandomAccessFile(String name, String mode) throws FileNotFoundException {
InferBuiltins.__set_file_attribute(this);
}
public RandomAccessFile(File file, String mode)
throws FileNotFoundException {
InferBuiltins.__set_file_attribute(this);
}
public RandomAccessFile(File file, String mode) throws FileNotFoundException {
InferBuiltins.__set_file_attribute(this);
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public FileChannel getChannel() {
channel = new FileChannelImpl(this, fd, InferUndefined.int_undefined());
return channel;
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
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[], 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 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 final void readFully(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void readFully(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void readFully(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void readFully(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int b) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(byte b[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void seek(long pos) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void seek(long pos) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long length() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public long length() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public final boolean readBoolean() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public final boolean readBoolean() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public final byte readByte() throws IOException {
return InferUndefined.can_throw_ioexception_byte();
}
public final byte readByte() throws IOException {
return InferUndefined.can_throw_ioexception_byte();
}
public final int readUnsignedByte() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final int readUnsignedByte() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final short readShort() throws IOException {
return InferUndefined.can_throw_ioexception_short();
}
public final short readShort() throws IOException {
return InferUndefined.can_throw_ioexception_short();
}
public final int readUnsignedShort() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final int readUnsignedShort() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final char readChar() throws IOException {
return InferUndefined.can_throw_ioexception_char();
}
public final char readChar() throws IOException {
return InferUndefined.can_throw_ioexception_char();
}
public final int readInt() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final int readInt() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public final long readLong() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public final long readLong() throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public final float readFloat() throws IOException {
return InferUndefined.can_throw_ioexception_float();
}
public final float readFloat() throws IOException {
return InferUndefined.can_throw_ioexception_float();
}
public final double readDouble() throws IOException {
return InferUndefined.can_throw_ioexception_double();
}
public final String readLine() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final String readUTF() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final void writeBoolean(boolean v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeByte(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeShort(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final double readDouble() throws IOException {
return InferUndefined.can_throw_ioexception_double();
}
public final String readLine() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final String readUTF() throws IOException {
return InferUndefined.can_throw_ioexception_string();
}
public final void writeBoolean(boolean v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeByte(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeShort(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChar(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChar(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeInt(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeInt(int v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeLong(long v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeLong(long v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeFloat(float v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeFloat(float v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeDouble(double v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeDouble(double v) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBytes(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeBytes(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChars(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeChars(String s) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public final void writeUTF(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -12,37 +12,36 @@ import com.facebook.infer.builtins.InferUndefined;
public abstract class Reader {
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(java.nio.CharBuffer target) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
public void close() throws IOException {
InferBuiltins.__set_mem_attribute(this);
InferUndefined.can_throw_ioexception_void();
}
public int read() throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[]) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(char cbuf[], int off, int len) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public int read(java.nio.CharBuffer target) throws IOException {
return InferUndefined.can_throw_ioexception_int();
}
public boolean ready() throws IOException {
return InferUndefined.can_throw_ioexception_boolean();
}
public void reset() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public long skip(long n) throws IOException {
return InferUndefined.can_throw_ioexception_long();
}
}

@ -11,44 +11,42 @@ import com.facebook.infer.builtins.InferUndefined;
public abstract class Writer {
public Writer append(char c) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq, int start, int end)
throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public Writer append(char c) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public Writer append(CharSequence csq, int start, int end) throws IOException {
InferUndefined.can_throw_ioexception_void();
return this;
}
public void flush() throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[]) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(char cbuf[], int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(int c) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
public void write(String str, int off, int len) throws IOException {
InferUndefined.can_throw_ioexception_void();
}
}

@ -9,25 +9,23 @@ package java.lang;
public final class Class<T> {
transient String name;
transient String name;
public String getName() {
return this.name;
}
public String getName() {
return this.name;
}
public static Class<?> forName(String className)
throws ClassNotFoundException {
return new Class();
}
public static Class<?> forName(String className) throws ClassNotFoundException {
return new Class();
}
public boolean isAssignableFrom(Class<?> cls) {
return false;
}
public static Class getPrimitiveClass(String name) {
Class c = new Class();
c.name = name;
return c;
}
public boolean isAssignableFrom(Class<?> cls) {
return false;
}
public static Class getPrimitiveClass(String name) {
Class c = new Class();
c.name = name;
return c;
}
}

@ -24,12 +24,11 @@ public final class Integer {
public boolean equals(Object anObject) {
return anObject != null
&& anObject instanceof Integer
&& this.value == ((Integer) anObject).value;
&& anObject instanceof Integer
&& this.value == ((Integer) anObject).value;
}
public int intValue() {
return this.value;
}
}

@ -9,10 +9,7 @@ package java.lang;
public class NullPointerException extends RuntimeException {
public NullPointerException() {
}
public NullPointerException(String s) {
}
public NullPointerException() {}
public NullPointerException(String s) {}
}

@ -11,13 +11,13 @@ import com.facebook.infer.builtins.InferUndefined;
public class Object {
public Class getClass() {
Class c = new Class();
c.name = (String)InferUndefined.object_undefined();
return c;
}
public Class getClass() {
Class c = new Class();
c.name = (String) InferUndefined.object_undefined();
return c;
}
public int hashCode() {
return InferUndefined.int_undefined();
}
public int hashCode() {
return InferUndefined.int_undefined();
}
}

@ -8,8 +8,6 @@
package java.lang;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.io.FileDescriptor;
public class Process {
@ -26,5 +24,4 @@ public class Process {
destroy();
return this;
}
}

@ -8,19 +8,18 @@
package java.lang;
import com.facebook.infer.builtins.InferUndefined;
import java.io.File;
import java.io.FileDescriptor;
import java.io.IOException;
import java.lang.ref.ReferenceQueue;
import java.lang.ref.WeakReference;
abstract class ProcessManager {
public Process exec(String[] taintedCommand, String[] taintedEnvironment, File workingDirectory,
boolean redirectErrorStream) throws IOException {
public Process exec(
String[] taintedCommand,
String[] taintedEnvironment,
File workingDirectory,
boolean redirectErrorStream)
throws IOException {
FileDescriptor in = new FileDescriptor();
FileDescriptor out = new FileDescriptor();
@ -30,5 +29,4 @@ abstract class ProcessManager {
}
public static native ProcessManager getInstance();
}

@ -10,11 +10,9 @@ package java.lang;
import java.io.File;
import java.io.IOException;
public class Runtime {
private Runtime() {
}
private Runtime() {}
public Process exec(String command) throws IOException {
return exec(command, null, null);
@ -24,8 +22,7 @@ public class Runtime {
return exec(command, envp, null);
}
public Process exec(String command, String[] envp, File dir)
throws IOException {
public Process exec(String command, String[] envp, File dir) throws IOException {
return ProcessManager.getInstance().exec(null, envp, null, false);
}
@ -37,9 +34,7 @@ public class Runtime {
return exec(cmdarray, envp, null);
}
public Process exec(String[] cmdarray, String[] envp, File dir)
throws IOException {
public Process exec(String[] cmdarray, String[] envp, File dir) throws IOException {
return ProcessManager.getInstance().exec(cmdarray, envp, dir, false);
}
}

@ -8,56 +8,50 @@
package java.lang;
import com.facebook.infer.builtins.InferUndefined;
import com.facebook.infer.builtins.InferBuiltins;
public final class String {
private final char[] value;
private final int offset;
private final int count;
private final char[] value;
private final int offset;
private final int count;
public int length() {
if (this == "")
return 0;
else {
return InferUndefined.nonneg_int();
}
public int length() {
if (this == "") return 0;
else {
return InferUndefined.nonneg_int();
}
public String() {
this.offset = 0;
this.count = 0;
this.value = new char[0];
}
public String(byte bytes[]) {
this(bytes, 0, bytes.length);
}
public String(byte bytes[], int offset, int length) {
checkBounds(bytes, offset, length);
char[] v = new char[bytes[0]]; /** yes, this could be improved **/
this.offset = 0;
this.count = v.length;
this.value = v;
}
public String() {
this.offset = 0;
this.count = 0;
this.value = new char[0];
}
public String(byte bytes[]) {
this(bytes, 0, bytes.length);
}
public String(byte bytes[], int offset, int length) {
checkBounds(bytes, offset, length);
char[] v = new char[bytes[0]];
/** yes, this could be improved * */
this.offset = 0;
this.count = v.length;
this.value = v;
}
private static void checkBounds(byte[] bytes, int offset, int length) {
if (length < 0) throw new StringIndexOutOfBoundsException(length);
if (offset < 0) throw new StringIndexOutOfBoundsException(offset);
if (offset > bytes.length - length) throw new StringIndexOutOfBoundsException(offset + length);
}
public boolean equals(Object anObject) {
if (this == anObject) {
return true;
} else {
return InferUndefined.boolean_undefined();
}
private static void checkBounds(byte[] bytes, int offset, int length) {
if (length < 0)
throw new StringIndexOutOfBoundsException(length);
if (offset < 0)
throw new StringIndexOutOfBoundsException(offset);
if (offset > bytes.length - length)
throw new StringIndexOutOfBoundsException(offset + length);
}
public boolean equals(Object anObject) {
if (this == anObject) {
return true;
} else {
return InferUndefined.boolean_undefined();
}
}
}
}

@ -9,41 +9,35 @@ package java.lang;
import com.facebook.infer.builtins.InferBuiltins;
import com.facebook.infer.builtins.InferUndefined;
import java.io.ByteArrayInputStream;
import java.io.ByteArrayOutputStream;
import java.io.InputStream;
import java.io.PrintStream;
public final class System {
private System() {
}
private System() {}
public final static InputStream in;
public static final InputStream in;
static {
byte[] arr = {0};
in = new ByteArrayInputStream(arr);
}
static {
byte[] arr = {0};
in = new ByteArrayInputStream(arr);
}
public final static PrintStream out = new PrintStream(
new ByteArrayOutputStream());
public static final PrintStream out = new PrintStream(new ByteArrayOutputStream());
public final static PrintStream err = new PrintStream(
new ByteArrayOutputStream());
public static final PrintStream err = new PrintStream(new ByteArrayOutputStream());
public static void exit(int status) {
InferBuiltins._exit();
}
public static void exit(int status) {
InferBuiltins._exit();
}
public static String getProperty(String key) {
int n = key.length(); // key must not be null
if (InferUndefined.boolean_undefined()) {
return null;
}
return (String)InferUndefined.object_undefined();
public static String getProperty(String key) {
int n = key.length(); // key must not be null
if (InferUndefined.boolean_undefined()) {
return null;
}
return (String) InferUndefined.object_undefined();
}
}

Some files were not shown because too many files have changed in this diff Show More

Loading…
Cancel
Save