diff options
Diffstat (limited to 'tools/infer/test/autotest/src/main')
9 files changed, 182 insertions, 0 deletions
diff --git a/tools/infer/test/autotest/src/main/java/Biabduction.java b/tools/infer/test/autotest/src/main/java/Biabduction.java new file mode 100644 index 0000000000..22fd0a896b --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Biabduction.java @@ -0,0 +1,22 @@ +/* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ + +import javax.annotation.Nullable; +import java.util.List; + +public class Biabduction { + private String get() { return null; } + + public void f1() { + get().length(); // error + } + + public void f2() { + try { + get().length(); // error + } catch (NullPointerException e) { + + } + } +} diff --git a/tools/infer/test/autotest/src/main/java/Biabduction.json b/tools/infer/test/autotest/src/main/java/Biabduction.json new file mode 100644 index 0000000000..953119d0c1 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Biabduction.json @@ -0,0 +1 @@ +[{"key": "Biabduction.java|f1|NULL_DEREFERENCE", "hash": "18467ae22b3a0dde943dc9dfc84d193a", "severity": "ERROR", "column": -1, "bug_type_hum": "Null Dereference", "node_key": "9afcdcc9d4253c36267a0d34b98c337d", "bug_type": "NULL_DEREFERENCE", "file": "autotest/src/main/java/Biabduction.java", "procedure_start_line": 11, "line": 12, "bug_trace": [{"line_number": 11, "filename": "autotest/src/main/java/Biabduction.java", "description": "start of procedure f1()", "column_number": -1, "level": 0}, {"line_number": 12, "filename": "autotest/src/main/java/Biabduction.java", "description": "", "column_number": -1, "level": 0}, {"line_number": 9, "filename": "autotest/src/main/java/Biabduction.java", "description": "start of procedure get()", "column_number": -1, "level": 1}, {"line_number": 9, "filename": "autotest/src/main/java/Biabduction.java", "description": "return from a call to String Biabduction.get()", "column_number": -1, "level": 1}, {"line_number": 12, "filename": "autotest/src/main/java/Biabduction.java", "description": "", "column_number": -1, "level": 0}], "procedure": "Biabduction.f1():void", "qualifier": "object returned by `get(this)` could be null and is dereferenced at line 12."}, {"key": "Biabduction.java|f2|NULL_DEREFERENCE", "hash": "d2f31f10d3c48ee63c61f52f4f83de4c", "severity": "ERROR", "column": -1, "bug_type_hum": "Null Dereference", "node_key": "9afcdcc9d4253c36267a0d34b98c337d", "bug_type": "NULL_DEREFERENCE", "file": "autotest/src/main/java/Biabduction.java", "procedure_start_line": 15, "line": 17, "bug_trace": [{"line_number": 15, "filename": "autotest/src/main/java/Biabduction.java", "description": "start of procedure f2()", "column_number": -1, "level": 0}, {"line_number": 17, "filename": "autotest/src/main/java/Biabduction.java", "description": "", "column_number": -1, "level": 0}, {"line_number": 9, "filename": "autotest/src/main/java/Biabduction.java", "description": "start of procedure get()", "column_number": -1, "level": 1}, {"line_number": 9, "filename": "autotest/src/main/java/Biabduction.java", "description": "return from a call to String Biabduction.get()", "column_number": -1, "level": 1}, {"line_number": 17, "filename": "autotest/src/main/java/Biabduction.java", "description": "", "column_number": -1, "level": 0}], "procedure": "Biabduction.f2():void", "qualifier": "object returned by `get(this)` could be null and is dereferenced at line 17."}]
\ No newline at end of file diff --git a/tools/infer/test/autotest/src/main/java/Checkers.java b/tools/infer/test/autotest/src/main/java/Checkers.java new file mode 100644 index 0000000000..f26170a471 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Checkers.java @@ -0,0 +1,34 @@ +/* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ + +import java.io.BufferedReader; +import java.io.File; +import java.io.FileReader; + +public class Checkers { + public static void leak() { + try { + BufferedReader br = new BufferedReader( + new FileReader(new File("some.txt")) + ); + } catch (Exception e) { + + } + } + + public static void error1() { + String str = null; + try { + int x = str.length(); // Error: even if exception is caught + } catch (NullPointerException e) { + + } + } + + public static void error2() { + String str = null; + int x = str.length(); // Error: not checking for null + } + +} diff --git a/tools/infer/test/autotest/src/main/java/Checkers.json b/tools/infer/test/autotest/src/main/java/Checkers.json new file mode 100644 index 0000000000..a971d3f771 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Checkers.json @@ -0,0 +1 @@ +[{"key": "Checkers.java|leak|RESOURCE_LEAK", "hash": "9c8b2bb1dbffb7893fc2ae9f60f83653", "severity": "ERROR", "column": -1, "bug_type_hum": "Resource Leak", "node_key": "3a2af627d5d1f10e1994f6259cf18e4c", "bug_type": "RESOURCE_LEAK", "file": "autotest/src/main/java/Checkers.java", "procedure_start_line": 10, "line": 12, "bug_trace": [{"line_number": 10, "filename": "autotest/src/main/java/Checkers.java", "description": "start of procedure leak()", "column_number": -1, "level": 0}, {"line_number": 12, "filename": "autotest/src/main/java/Checkers.java", "description": "", "column_number": -1, "level": 0}], "procedure": "Checkers.leak():void", "qualifier": "resource of type `java.io.FileReader` acquired by call to `new()` at line 12 is not released after line 12."}, {"key": "Checkers.java|error1|NULL_DEREFERENCE", "hash": "04ff79bfff8a231ff4cdb045a76641f0", "severity": "ERROR", "column": -1, "bug_type_hum": "Null Dereference", "node_key": "c281f77c6dae544ee5fb7d5e2bb35118", "bug_type": "NULL_DEREFERENCE", "file": "autotest/src/main/java/Checkers.java", "procedure_start_line": 20, "line": 23, "bug_trace": [{"line_number": 20, "filename": "autotest/src/main/java/Checkers.java", "description": "start of procedure error1()", "column_number": -1, "level": 0}, {"line_number": 21, "filename": "autotest/src/main/java/Checkers.java", "description": "", "column_number": -1, "level": 0}, {"line_number": 23, "filename": "autotest/src/main/java/Checkers.java", "description": "", "column_number": -1, "level": 0}], "procedure": "Checkers.error1():void", "qualifier": "object `str` last assigned on line 21 could be null and is dereferenced at line 23."}, {"key": "Checkers.java|error2|NULL_DEREFERENCE", "hash": "c4fe7d68fbb6b3ea84f233de6fd3add8", "severity": "ERROR", "column": -1, "bug_type_hum": "Null Dereference", "node_key": "c281f77c6dae544ee5fb7d5e2bb35118", "bug_type": "NULL_DEREFERENCE", "file": "autotest/src/main/java/Checkers.java", "procedure_start_line": 29, "line": 31, "bug_trace": [{"line_number": 29, "filename": "autotest/src/main/java/Checkers.java", "description": "start of procedure error2()", "column_number": -1, "level": 0}, {"line_number": 30, "filename": "autotest/src/main/java/Checkers.java", "description": "", "column_number": -1, "level": 0}, {"line_number": 31, "filename": "autotest/src/main/java/Checkers.java", "description": "", "column_number": -1, "level": 0}], "procedure": "Checkers.error2():void", "qualifier": "object `str` last assigned on line 30 could be null and is dereferenced at line 31."}]
\ No newline at end of file diff --git a/tools/infer/test/autotest/src/main/java/Eradicate.java b/tools/infer/test/autotest/src/main/java/Eradicate.java new file mode 100644 index 0000000000..41e02d0562 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Eradicate.java @@ -0,0 +1,57 @@ +/* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ + +import javax.annotation.Nullable; + +// Examples taken from the infer website. +public class Eradicate { + + public String f; // Because it is not annoted with nullable -> can never be null! + + public void field(@Nullable Eradicate x) { + x.f = "3"; // Error: Eradicate null field access + } + + public void method(@Nullable Object x) { + String s = x.toString(); // Error: Eradicate null method call + } + + public void filedNotNull(@Nullable String s) { + f = s; // Error: Eradicate field not nullable + } + + public Eradicate() {} // Error: Eradicate field not initialized + + public void str(Eradicate x) { + String s = x.toString(); + } + + public void callStr(@Nullable Eradicate x) { + str(x); // Error: Eradicate parameter not nullable + } + + public String shouldNotReturnNullBecauseNotAnnotated() { + return null; // Error: Eradicate return not nullable + } + + public void redundant() { + String s = new String("abc"); + if (s != null) { // Error: Eradicate condition redundant + int n = s.length(); + } + } + + @Nullable + public static String someMethod() { + return ""; // Error: Eradicate return overannotated + } +} + +class B extends Eradicate { + @Nullable public String shouldNotReturnNullBecauseNotAnnotated() { + return null; // Error: Eradicate inconsistent subclass return annotation + } + + public void field(Eradicate x) {} // Error: Inconsistent subclass parameter annotation +} diff --git a/tools/infer/test/autotest/src/main/java/Racerd.java b/tools/infer/test/autotest/src/main/java/Racerd.java new file mode 100644 index 0000000000..176847f5f5 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Racerd.java @@ -0,0 +1,40 @@ +/* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ + +import javax.annotation.concurrent.ThreadSafe; + +// Examples taken from the infer website. +@ThreadSafe +public class Racerd { + private int mTemperature; + + public void makeDinner() { + boilWater(); + } + + private void boilWater() { + mTemperature = 100; //Error: unprotected write. + } +} + +@ThreadSafe +class Account { + + int mBalance = 0; + + public void deposit(int amount) { + if (amount > 0) { + mBalance += amount; // Error: unsynchronized write + } + } + + public int withdraw(int amount){ + if (amount >= 0 && mBalance - amount >= 0) { + mBalance -= amount; // Error: unsynchronized write + return mBalance; // Error: unsynchronized read + } else { + return 0; + } + } +} diff --git a/tools/infer/test/autotest/src/main/java/Racerd.json b/tools/infer/test/autotest/src/main/java/Racerd.json new file mode 100644 index 0000000000..ec55362496 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Racerd.json @@ -0,0 +1 @@ +[{"key": "Racerd.java|deposit|THREAD_SAFETY_VIOLATION", "hash": "1ec753a9022eedd27443e3ed3da93e44", "severity": "WARNING", "column": -1, "bug_type_hum": "Thread Safety Violation", "access": "hJWmvgAAACsAAAAEAAAAEwAAAA+gsFwA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmFA", "bug_type": "THREAD_SAFETY_VIOLATION", "file": "autotest/src/main/java/Racerd.java", "procedure_start_line": 0, "line": 28, "bug_trace": [{"line_number": 28, "filename": "autotest/src/main/java/Racerd.java", "description": "access to `this.mBalance`", "column_number": -1, "level": 0}], "procedure": "Account.deposit(int):void", "qualifier": "Unprotected write. Non-private method `void Account.deposit(int)` writes to field `this.mBalance` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself)."}, {"key": "Racerd.java|makeDinner|THREAD_SAFETY_VIOLATION", "hash": "b4c48330cdd4742e24fdfc5c809ff604", "severity": "WARNING", "column": -1, "bug_type_hum": "Thread Safety Violation", "access": "hJWmvgAAACsAAAAEAAAAEwAAAA+gsFEA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmFA", "bug_type": "THREAD_SAFETY_VIOLATION", "file": "autotest/src/main/java/Racerd.java", "procedure_start_line": 0, "line": 13, "bug_trace": [{"line_number": 13, "filename": "autotest/src/main/java/Racerd.java", "description": "call to void Racerd.boilWater()", "column_number": -1, "level": 0}, {"line_number": 17, "filename": "autotest/src/main/java/Racerd.java", "description": "access to `this.mTemperature`", "column_number": -1, "level": 1}], "procedure": "Racerd.makeDinner():void", "qualifier": "Unprotected write. Non-private method `void Racerd.makeDinner()` indirectly writes to field `this.mTemperature` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself)."}, {"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION", "hash": "4cb9f0b0b4649ec0f84dea3541a6c70d", "severity": "WARNING", "column": -1, "bug_type_hum": "Thread Safety Violation", "access": "hJWmvgAAADIAAAAGAAAAGgAAABagsGEA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmGgsGIA/wQEQA==", "bug_type": "THREAD_SAFETY_VIOLATION", "file": "autotest/src/main/java/Racerd.java", "procedure_start_line": 0, "line": 33, "bug_trace": [{"line_number": 33, "filename": "autotest/src/main/java/Racerd.java", "description": "<Read trace>", "column_number": -1, "level": 0}, {"line_number": 33, "filename": "autotest/src/main/java/Racerd.java", "description": "access to `this.mBalance`", "column_number": -1, "level": 0}, {"line_number": 34, "filename": "autotest/src/main/java/Racerd.java", "description": "<Write trace>", "column_number": -1, "level": 0}, {"line_number": 34, "filename": "autotest/src/main/java/Racerd.java", "description": "access to `this.mBalance`", "column_number": -1, "level": 0}], "procedure": "Account.withdraw(int):int", "qualifier": "Read/Write race. Non-private method `int Account.withdraw(int)` reads without synchronization from `this.mBalance`. Potentially races with write in method `Account.withdraw(...)`.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself)."}, {"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION", "hash": "83037b7ad2aa337deba2dbe26e892440", "severity": "WARNING", "column": -1, "bug_type_hum": "Thread Safety Violation", "access": "hJWmvgAAACsAAAAEAAAAEwAAAA+gsGIA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmFA", "bug_type": "THREAD_SAFETY_VIOLATION", "file": "autotest/src/main/java/Racerd.java", "procedure_start_line": 0, "line": 34, "bug_trace": [{"line_number": 34, "filename": "autotest/src/main/java/Racerd.java", "description": "access to `this.mBalance`", "column_number": -1, "level": 0}], "procedure": "Account.withdraw(int):int", "qualifier": "Unprotected write. Non-private method `int Account.withdraw(int)` writes to field `this.mBalance` outside of synchronization.\n Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (including itself)."}]
\ No newline at end of file diff --git a/tools/infer/test/autotest/src/main/java/Starvation.java b/tools/infer/test/autotest/src/main/java/Starvation.java new file mode 100644 index 0000000000..29748877d6 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Starvation.java @@ -0,0 +1,25 @@ +/* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at http://mozilla.org/MPL/2.0/. */ + +// Examples taken from the infer website. +public class Starvation { + + String lockA, lockB; + + public void lockAThenB() { + synchronized(lockA) { + synchronized(lockB) { + // do something with both resources + } + } + } + + public void lockBThenA() { + synchronized(lockB) { + synchronized(lockA) { + // do something with both resources + } + } + } +} diff --git a/tools/infer/test/autotest/src/main/java/Starvation.json b/tools/infer/test/autotest/src/main/java/Starvation.json new file mode 100644 index 0000000000..0d0384a724 --- /dev/null +++ b/tools/infer/test/autotest/src/main/java/Starvation.json @@ -0,0 +1 @@ +[{"key": "Starvation.java|lockAThenB|DEADLOCK", "hash": "9197aca80b5207ae80f4b51c218dcf49", "severity": "ERROR", "column": -1, "bug_type_hum": "Deadlock", "bug_type": "DEADLOCK", "file": "autotest/src/main/java/Starvation.java", "procedure_start_line": 0, "line": 11, "bug_trace": [{"line_number": 11, "filename": "autotest/src/main/java/Starvation.java", "description": "[Trace 1] `void Starvation.lockAThenB()`", "column_number": -1, "level": 0}, {"line_number": 11, "filename": "autotest/src/main/java/Starvation.java", "description": " locks `this.lockA` in `class Starvation`", "column_number": -1, "level": 0}, {"line_number": 12, "filename": "autotest/src/main/java/Starvation.java", "description": " locks `this.lockB` in `class Starvation`", "column_number": -1, "level": 1}, {"line_number": 19, "filename": "autotest/src/main/java/Starvation.java", "description": "[Trace 2] `void Starvation.lockBThenA()`", "column_number": -1, "level": 0}, {"line_number": 19, "filename": "autotest/src/main/java/Starvation.java", "description": " locks `this.lockB` in `class Starvation`", "column_number": -1, "level": 0}, {"line_number": 20, "filename": "autotest/src/main/java/Starvation.java", "description": " locks `this.lockA` in `class Starvation`", "column_number": -1, "level": 1}], "procedure": "Starvation.lockAThenB():void", "qualifier": "Potential deadlock. `void Starvation.lockAThenB()` (Trace 1) and `void Starvation.lockBThenA()` (Trace 2) acquire locks `this.lockB` in `class Starvation` and `this.lockA` in `class Starvation` in reverse orders."}]
\ No newline at end of file |