nagai/fune
3
0
Fork 0
forked from mirrors/gecko-dev
Code Pull requests Activity

Bug 1576659 - Update infer to 0.17.0. r=bastien

Browse source 
Differential Revision: https://phabricator.services.mozilla.com/D43471

--HG--
extra : moz-landing-system : lando
This commit is contained in:
Andi-Bogdan Postelnicu 2019-09-13 14:25:32 +00:00
parent ab637aa92b
commit 1b886ecee7
9 changed files with 32 additions and 453 deletions
repo.diff.show_diff_stats Download patch file Download diff file Expand all files Collapse all files

19
build/build-infer/build-infer.py
View file

@ -107,11 +107,26 @@ if __name__ == '__main__':
run_in(source_dir, ['git']+command)
for p in config.get('patches', []):
run_in(source_dir, ['git', 'apply', os.path.join(dir_path, p)])
# configure opam
run_in(source_dir, ['opam', 'init', '--no-setup', '--disable-sandboxing'])
# build infer
run_in(source_dir, ['./build-infer.sh', 'java'],
extra_env={'NO_CMAKE_STRIP': '1'})
package_name = 'infer'
infer_package = os.path.join(os.getcwd(), package_name)
# We need to create a package with all of the depended libraries injected in it
run_in(source_dir, ['make', 'install-with-libs', 'BUILD_MODE=opt',
'PATCHELF=patchelf', 'DESTDIR={}'.format(infer_package),
'libdir_relative_to_bindir=../lib'])
infer_package_with_pref = os.path.join(infer_package, 'usr')
if not args.skip_tar:
os.rename(os.path.join(infer_package_with_pref, 'local'),
os.path.join(infer_package_with_pref, 'infer'))
build_tar_package('tar', '%s.tar.xz' % (package_name),
source_dir, [os.path.join('infer', 'bin'),
os.path.join('infer', 'lib')])
infer_package_with_pref,
[os.path.join('infer', 'bin'),
os.path.join('infer', 'lib'),
os.path.join('infer', 'share')])

2
build/build-infer/infer-linux64.json
View file

@ -1,5 +1,5 @@
{
"infer_repo": "https://github.com/facebook/infer",
"infer_revision": "14aa1edbf532675f48ba0a35a2e55d07b79b1f3c",
"infer_revision": "99464c01da5809e7159ed1a75ef10f60d34506a4",
"patches": []
}

2
python/mozbuild/mozbuild/code-analysis/mach_commands.py
View file

@ -1261,7 +1261,7 @@ class StaticAnalysis(MachCommandBase):
)
return self.TOOLS_CHECKER_RETURNED_NO_ISSUES
if self._dump_results:
self._build_autotest_result(test_file_path_json, issues)
self._build_autotest_result(test_file_path_json, json.dumps(issues))
else:
if not os.path.exists(test_file_path_json):
# Result file for test not found maybe regenerate it?

2
taskcluster/ci/docker-image/kind.yml
View file

@ -202,7 +202,7 @@ jobs:
- deb10-python-zstandard
static-analysis-build:
symbol: I(static-analysis-build)
parent: android-build
parent: debian9-base
mingw32-build:
symbol: I(mingw)
parent: debian9-base

10
taskcluster/docker/static-analysis-build/Dockerfile
View file

@ -21,7 +21,6 @@ RUN apt-get update && \
cmake \
flex \
curl \
opam \
libsqlite3-dev \
file \
gawk \
@ -29,6 +28,7 @@ RUN apt-get update && \
gnupg \
jq \
libc6-dev \
libmpfr-dev \
nasm \
openjdk-8-jdk-headless \
pkg-config \
@ -55,10 +55,16 @@ RUN apt-get update && \
libfontconfig1-dev \
libfreetype6-dev \
libgconf2-dev \
libgmp-dev \
libgtk-3-dev \
libgtk2.0-dev \
libpango1.0-dev \
libpulse-dev \
libx11-xcb-dev \
libxt-dev \
lib32z1
lib32z1 \
patchelf
# Install opam 2
RUN curl -sL https://github.com/ocaml/opam/releases/download/2.0.3/opam-2.0.3-x86_64-linux > /usr/bin/opam && \
chmod +x /usr/bin/opam

115
tools/infer/test/autotest/src/main/java/Biabduction.json
View file

@ -1,114 +1 @@
[
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "start of procedure f1()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 11
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 12
},
{
"column_number": -1,
"description": "start of procedure get()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 1,
"line_number": 9
},
{
"column_number": -1,
"description": "return from a call to String Biabduction.get()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 1,
"line_number": 9
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 12
}
],
"bug_type": "NULL_DEREFERENCE",
"bug_type_hum": "Null Dereference",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Biabduction.java",
"hash": "918d7eaedf45f651f04c55554c72478c",
"key": "Biabduction.java|f1|NULL_DEREFERENCE",
"kind": "ERROR",
"line": 12,
"node_key": "9afcdcc9d4253c36267a0d34b98c337d",
"procedure": "void Biabduction.f1()",
"procedure_id": "Biabduction.f1():void.4b49520e7621606a0d5661886ff0b098",
"procedure_start_line": 11,
"qualifier": "object returned by `get(this)` could be null and is dereferenced at line 12.",
"severity": "HIGH",
"visibility": "user"
},
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "start of procedure f2()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 15
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 17
},
{
"column_number": -1,
"description": "start of procedure get()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 1,
"line_number": 9
},
{
"column_number": -1,
"description": "return from a call to String Biabduction.get()",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 1,
"line_number": 9
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Biabduction.java",
"level": 0,
"line_number": 17
}
],
"bug_type": "NULL_DEREFERENCE",
"bug_type_hum": "Null Dereference",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Biabduction.java",
"hash": "bc952ce8bad58dac5cb6672dc3150524",
"key": "Biabduction.java|f2|NULL_DEREFERENCE",
"kind": "ERROR",
"line": 17,
"node_key": "9afcdcc9d4253c36267a0d34b98c337d",
"procedure": "void Biabduction.f2()",
"procedure_id": "Biabduction.f2():void.41c05a632eb912a458482c1e2e4dcbb4",
"procedure_start_line": 15,
"qualifier": "object returned by `get(this)` could be null and is dereferenced at line 17.",
"severity": "HIGH",
"visibility": "user"
}
]
[{"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."}]

122
tools/infer/test/autotest/src/main/java/Checkers.json
View file

@ -1,121 +1 @@
[
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "start of procedure leak()",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 10
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 12
}
],
"bug_type": "RESOURCE_LEAK",
"bug_type_hum": "Resource Leak",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Checkers.java",
"hash": "56806153823413731f2e2166ed8d30a0",
"key": "Checkers.java|leak|RESOURCE_LEAK",
"kind": "ERROR",
"line": 12,
"node_key": "3a2af627d5d1f10e1994f6259cf18e4c",
"procedure": "void Checkers.leak()",
"procedure_id": "Checkers.leak():void.e21648e10d3037f4559cdb7c08642c84",
"procedure_start_line": 10,
"qualifier": "resource of type `java.io.FileReader` acquired by call to `new()` at line 12 is not released after line 12.",
"severity": "HIGH",
"visibility": "user"
},
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "start of procedure error1()",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 20
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 21
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 23
}
],
"bug_type": "NULL_DEREFERENCE",
"bug_type_hum": "Null Dereference",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Checkers.java",
"hash": "6de26e7c66c71b1114ad233679d55640",
"key": "Checkers.java|error1|NULL_DEREFERENCE",
"kind": "ERROR",
"line": 23,
"node_key": "c281f77c6dae544ee5fb7d5e2bb35118",
"procedure": "void Checkers.error1()",
"procedure_id": "Checkers.error1():void.59417424d80960700a32012973e98db5",
"procedure_start_line": 20,
"qualifier": "object `str` last assigned on line 21 could be null and is dereferenced at line 23.",
"severity": "HIGH",
"visibility": "user"
},
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "start of procedure error2()",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 29
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 30
},
{
"column_number": -1,
"description": "",
"filename": "autotest/src/main/java/Checkers.java",
"level": 0,
"line_number": 31
}
],
"bug_type": "NULL_DEREFERENCE",
"bug_type_hum": "Null Dereference",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Checkers.java",
"hash": "39e021b634ab428af7be2034688491a7",
"key": "Checkers.java|error2|NULL_DEREFERENCE",
"kind": "ERROR",
"line": 31,
"node_key": "c281f77c6dae544ee5fb7d5e2bb35118",
"procedure": "void Checkers.error2()",
"procedure_id": "Checkers.error2():void.e9146d80ba20c908c11d08947cd89d06",
"procedure_start_line": 29,
"qualifier": "object `str` last assigned on line 30 could be null and is dereferenced at line 31.",
"severity": "HIGH",
"visibility": "user"
}
]
[{"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."}]

147
tools/infer/test/autotest/src/main/java/Racerd.json
View file

@ -1,146 +1 @@
[
{
"access": "hJWmvgAAAJMAAAApAAAAfgAAAHSwkNAnZGVwb3NpdKCgQCNpbnRAk6AnQWNjb3VudECQoEAkdm9pZECgoJKgIECwXAD/kgkiYXV0b3Rlc3Qvc3JjL21haW4vamF2YS9SYWNlcmQuamF2YZGgoJGwAjafTBegJHRoaXNAkAQcoKOglJOgBBpAsEBAQEAEAaCRkTBBY2NvdW50Lm1CYWxhbmNlQKAEF0A=",
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "access to `this.Account.mBalance`",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 28
}
],
"bug_type": "THREAD_SAFETY_VIOLATION",
"bug_type_hum": "Thread Safety Violation",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Racerd.java",
"hash": "6b62cb17008a3135d218108fa3123402",
"key": "Racerd.java|deposit|THREAD_SAFETY_VIOLATION",
"kind": "ERROR",
"line": 28,
"node_key": "9c5d6d9028928346cc4fb44cced5dea1",
"procedure": "void Account.deposit(int)",
"procedure_id": "Account.deposit(int):void.a9cc1805c1e3652887a5ee12b55803af",
"procedure_start_line": 0,
"qualifier": "Unprotected write. Non-private method `void Account.deposit(int)` writes to field `this.Account.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).",
"severity": "HIGH",
"visibility": "user"
},
{
"access": "hJWmvgAAAKYAAAApAAAAhQAAAHqwkNAqbWFrZURpbm5lckCToCZSYWNlcmRAkKBAJHZvaWRAoKCQ0Clib2lsV2F0ZXJAk6AEC0AECkCwTQD/kgkiYXV0b3Rlc3Qvc3JjL21haW4vamF2YS9SYWNlcmQuamF2YZGgoJGwAjafTBegJHRoaXNAkAQboKOglJOgBBxAsEBAQEAEAaCRkTNSYWNlcmQubVRlbXBlcmF0dXJlQKCwUQD/BBdA",
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "call to void Racerd.boilWater()",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 13
},
{
"column_number": -1,
"description": "access to `this.Racerd.mTemperature`",
"filename": "autotest/src/main/java/Racerd.java",
"level": 1,
"line_number": 17
}
],
"bug_type": "THREAD_SAFETY_VIOLATION",
"bug_type_hum": "Thread Safety Violation",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Racerd.java",
"hash": "2882383086ab102a88144ae3c2cc4701",
"key": "Racerd.java|makeDinner|THREAD_SAFETY_VIOLATION",
"kind": "ERROR",
"line": 13,
"node_key": "9c5d6d9028928346cc4fb44cced5dea1",
"procedure": "void Racerd.makeDinner()",
"procedure_id": "Racerd.makeDinner():void.2796f75396b30d2d49b24ddfab722306",
"procedure_start_line": 0,
"qualifier": "Unprotected write. Non-private method `void Racerd.makeDinner()` indirectly writes to field `this.Racerd.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).",
"severity": "HIGH",
"visibility": "user"
},
{
"access": "hJWmvgAAAJgAAAAqAAAAgwAAAHqwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsGMA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmGQoKCRsAI2n0wXoCR0aGlzQJAEG6CjoJSToAQZQLBAQEBABAGgkZEwQWNjb3VudC5tQmFsYW5jZUCgBBegsGIA/wQYQA==",
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "<Read trace>",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 35
},
{
"column_number": -1,
"description": "access to `this.Account.mBalance`",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 35
},
{
"column_number": -1,
"description": "<Write trace>",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 34
},
{
"column_number": -1,
"description": "access to `this.Account.mBalance`",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 34
}
],
"bug_type": "THREAD_SAFETY_VIOLATION",
"bug_type_hum": "Thread Safety Violation",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Racerd.java",
"hash": "5665f12d2392f93f11f556cd1b1e238a",
"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION",
"kind": "ERROR",
"line": 35,
"node_key": "9c5d6d9028928346cc4fb44cced5dea1",
"procedure": "int Account.withdraw(int)",
"procedure_id": "Account.withdraw(int):int.038de5054c5c25e60d169e42e0177a16",
"procedure_start_line": 0,
"qualifier": "Read/Write race. Non-private method `int Account.withdraw(int)` reads without synchronization from `this.Account.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).",
"severity": "HIGH",
"visibility": "user"
},
{
"access": "hJWmvgAAAJEAAAAoAAAAfAAAAHOwkNAod2l0aGRyYXegoEAjaW50QJOgJ0FjY291bnRAkKBABAZAoKCSoCBAsGIA/5IJImF1dG90ZXN0L3NyYy9tYWluL2phdmEvUmFjZXJkLmphdmGRoKCRsAI2n0wXoCR0aGlzQJAEG6CjoJSToAQZQLBAQEBABAGgkZEwQWNjb3VudC5tQmFsYW5jZUCgBBdA",
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "access to `this.Account.mBalance`",
"filename": "autotest/src/main/java/Racerd.java",
"level": 0,
"line_number": 34
}
],
"bug_type": "THREAD_SAFETY_VIOLATION",
"bug_type_hum": "Thread Safety Violation",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Racerd.java",
"hash": "a7c30fd1b251d9e16750fc7e5913b885",
"key": "Racerd.java|withdraw|THREAD_SAFETY_VIOLATION",
"kind": "ERROR",
"line": 34,
"node_key": "9c5d6d9028928346cc4fb44cced5dea1",
"procedure": "int Account.withdraw(int)",
"procedure_id": "Account.withdraw(int):int.038de5054c5c25e60d169e42e0177a16",
"procedure_start_line": 0,
"qualifier": "Unprotected write. Non-private method `int Account.withdraw(int)` writes to field `this.Account.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).",
"severity": "HIGH",
"visibility": "user"
}
]
[{"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)."}]

66
tools/infer/test/autotest/src/main/java/Starvation.json
View file

@ -1,65 +1 @@
[
{
"bug_class": "PROVER",
"bug_trace": [
{
"column_number": -1,
"description": "[Trace 1] `void Starvation.lockAThenB()`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 0,
"line_number": 11
},
{
"column_number": -1,
"description": "locks `this.Starvation.lockA` in class `Starvation*`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 0,
"line_number": 11
},
{
"column_number": -1,
"description": "locks `this.Starvation.lockB` in class `Starvation*`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 1,
"line_number": 12
},
{
"column_number": -1,
"description": "[Trace 2] `void Starvation.lockBThenA()`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 0,
"line_number": 19
},
{
"column_number": -1,
"description": "locks `this.Starvation.lockB` in class `Starvation*`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 0,
"line_number": 19
},
{
"column_number": -1,
"description": "locks `this.Starvation.lockA` in class `Starvation*`",
"filename": "autotest/src/main/java/Starvation.java",
"level": 1,
"line_number": 20
}
],
"bug_type": "DEADLOCK",
"bug_type_hum": "Deadlock",
"censored_reason": "",
"column": -1,
"file": "autotest/src/main/java/Starvation.java",
"hash": "043d28a94431b4c573b949b8570fb318",
"key": "Starvation.java|lockAThenB|DEADLOCK",
"kind": "ERROR",
"line": 11,
"node_key": "9c5d6d9028928346cc4fb44cced5dea1",
"procedure": "void Starvation.lockAThenB()",
"procedure_id": "Starvation.lockAThenB():void.b7eb3955306c498af42d6336f52a796f",
"procedure_start_line": 0,
"qualifier": "Potential deadlock.\nTrace 1 (starts at `void Starvation.lockAThenB()`) first locks `this.Starvation.lockA` in class `Starvation*` (line 11 in `void Starvation.lockAThenB()`) and then locks `this.Starvation.lockB` in class `Starvation*` (line 12 in `void Starvation.lockAThenB()`).\nTrace 2 (starts at `void Starvation.lockBThenA()`), first locks `this.Starvation.lockB` in class `Starvation*` (line 19 in `void Starvation.lockBThenA()`) and then locks `this.Starvation.lockA` in class `Starvation*` (line 20 in `void Starvation.lockBThenA()`).",
"severity": "HIGH",
"visibility": "user"
}
]
[{"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."}]