diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index df3cf545c5..c151ed1f75 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -56,7 +56,8 @@ struct Priv.read_global ask getg st g x else ( let rel = st.rel in - let g_var = RV.global g in + (* If it has escaped and we have never been multi-threaded, we can still refer to the local *) + let g_var = if g.vglob then RV.global g else RV.local g in let x_var = RV.local x in let rel' = RD.add_vars rel [g_var] in let rel' = RD.assign_var rel' x_var g_var in @@ -602,6 +603,10 @@ struct | Some (Local v) -> if VH.mem v_ins_inv v then keep_global + else if ThreadEscape.has_escaped ask v then + (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *) + (* and is not a sound description of the C variable. *) + false else keep_local | _ -> false diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c new file mode 100644 index 0000000000..c63ef754a0 --- /dev/null +++ b/tests/regression/46-apron2/95-witness-mm-escape.c @@ -0,0 +1,19 @@ +// CRAM SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml +#include +#include + +int *b; +pthread_mutex_t e; + +void main() { + + int g = 8; + int a; + if(a) { + g = 10; + } + + b = &g; + + pthread_mutex_lock(&e); +} diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t new file mode 100644 index 0000000000..11cd3691c5 --- /dev/null +++ b/tests/regression/46-apron2/95-witness-mm-escape.t @@ -0,0 +1,29 @@ + $ goblint --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml 95-witness-mm-escape.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Success][Witness] invariant confirmed: 0 <= g (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: -8LL + (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: 2147483648LL + (long long )a >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: 10LL - (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: 2147483647LL - (long long )a >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1) + [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1) + [Info][Witness] witness validation summary: + confirmed: 15 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 15 diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml new file mode 100644 index 0000000000..0f0614892c --- /dev/null +++ b/tests/regression/46-apron2/95-witness-mm-escape.yml @@ -0,0 +1,450 @@ +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: f88caf27-fbfe-4ce8-a15d-463646cca899 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: 0 <= g + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 7949534c-6edd-4412-9778-fc58745e7cc5 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: 0 <= *b + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: ffe5f8b3-569c-4d42-8e9b-21c48312e6ce + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: g <= 127 + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: cad5c137-4373-4431-b8c8-c5d1e537a716 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: '*b <= 127' + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: aa21493b-1338-4004-90b7-046b9e826169 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: -8LL + (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: b640fdf6-abc8-45b9-ad4f-2695e0d66a3d + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: 2147483648LL + (long long )a >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: ecc017f2-d045-45c7-a795-d3d16088368d + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: (2147483638LL + (long long )a) + (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 52ace953-715d-4d44-9c44-5b40c1124593 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: (2147483637LL - (long long )a) + (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 661e7eee-b5c0-4de3-89ed-369f6978ba28 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: 10LL - (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 7878f84e-a951-4247-a196-97f9195cf2fb + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: 2147483647LL - (long long )a >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: e80582ed-4527-4773-97fd-08631c673c21 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: (2147483658LL + (long long )a) - (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 49f62de7-3bfc-45ee-8709-0ff295f23b7a + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: (2147483657LL - (long long )a) - (long long )g >= 0LL + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: cb86dd3a-2ff5-420b-8d49-42240a324a26 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: b == & g + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 2573f907-0386-4098-9b0c-7f1ec86d3f90 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: g != 0 + type: assertion + format: C +- entry_type: location_invariant + metadata: + format_version: "0.1" + uuid: 15693293-61f1-431b-867e-86add36e4d80 + creation_time: 2024-07-16T16:36:39Z + producer: + name: Goblint + version: heads/check_overflow_convert-0-gc35fd8620-dirty + command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]'' + ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization'' + ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable'' + ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var'' + ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + task: + input_files: + - 95-witness-mm-escape.c + input_file_hashes: + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + data_model: LP64 + language: C + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + location_invariant: + string: '*b != 0' + type: assertion + format: C diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c new file mode 100644 index 0000000000..fbbd1a44eb --- /dev/null +++ b/tests/regression/46-apron2/96-witness-mm-escape2.c @@ -0,0 +1,22 @@ +// CRAM SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable warn.deterministic --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml +#include +int *b; +pthread_mutex_t e; + +void* other(void* arg) { + pthread_mutex_lock(&e); + *b = -100; + pthread_mutex_unlock(&e); + + return NULL; +} + +void main() { + pthread_t t; + pthread_create(&t, NULL, other, NULL); + int g = 8; + + b = &g; + + pthread_mutex_lock(&e); +} diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t new file mode 100644 index 0000000000..1f73026a5b --- /dev/null +++ b/tests/regression/46-apron2/96-witness-mm-escape2.t @@ -0,0 +1,21 @@ + $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.entry-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml + [Info][Witness] witness generation summary: + location invariants: 4 + loop invariants: 0 + flow-insensitive invariants: 0 + total generation entries: 4 + + $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set witness.yaml.entry-types '["location_invariant"]' --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c + [Info][Witness] witness validation summary: + confirmed: 4 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 4 + [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5) + [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1) + [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1) + [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1) diff --git a/tests/regression/46-apron2/dune b/tests/regression/46-apron2/dune index 89efde3083..8395e69ea3 100644 --- a/tests/regression/46-apron2/dune +++ b/tests/regression/46-apron2/dune @@ -12,4 +12,4 @@ (cram (alias runaprontest) (enabled_if %{lib-available:apron}) - (deps (glob_files *.c))) + (deps (glob_files *.c) (glob_files *.yml)))