diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t index c5cee8cfdb..047cb15718 100644 --- a/tests/regression/46-apron2/95-witness-mm-escape.t +++ b/tests/regression/46-apron2/95-witness-mm-escape.t @@ -7,19 +7,23 @@ [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: 22 + confirmed: 30 unconfirmed: 0 refuted: 0 error: 0 unchecked: 0 unsupported: 0 disabled: 0 - total validation entries: 22 + total validation entries: 30 diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml index bf99e03f97..66715bd382 100644 --- a/tests/regression/46-apron2/95-witness-mm-escape.yml +++ b/tests/regression/46-apron2/95-witness-mm-escape.yml @@ -1,25 +1,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: bd605de4-9e24-4df2-a8b6-7a20973f08c3 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -30,25 +31,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: d52450ae-a439-4c7e-9cd7-88a4d7b2729d - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -59,25 +61,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: 934e24ac-ff4e-4ce8-b10e-28c96d1d9a85 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -88,25 +91,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: b67ec3d2-1506-4a5a-a019-b959fa02c710 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -117,25 +121,86 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: 799dbde2-5854-4786-b784-22941410dd4c - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 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 @@ -146,25 +211,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: fbf9961a-853f-4bc0-be9b-a12f6d49ab20 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -175,25 +241,86 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: c7d1d801-2b2a-4f34-a0ed-29e496ae2bbf - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 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 @@ -204,25 +331,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: f626d0f0-9ab2-4e7e-8568-194a3ba0f671 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -233,25 +361,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: 70ebfa4c-8b42-439e-bb6f-f8b87b8bebe9 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -262,25 +391,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: 1b25d102-ebc5-4dde-854d-ac5525aa4fed - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -291,25 +421,26 @@ - entry_type: location_invariant metadata: format_version: "0.1" - uuid: bc5e8286-3029-4002-b87b-1288f32e44c4 - creation_time: 2024-07-16T16:10:49Z + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -320,20 +451,21 @@ - entry_type: invariant_set metadata: format_version: "0.1" - uuid: 8cad3de5-98bb-4400-833c-bae232e13530 - creation_time: 2024-07-16T16:10:49Z + uuid: 5f4a70a3-8b30-4b5a-a260-56bb341a6283 + 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'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml''' + ''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: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + 95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 data_model: LP64 language: C content: @@ -341,7 +473,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -351,7 +483,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -361,7 +493,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -371,7 +503,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -381,7 +513,27 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + value: -8LL + (long long )g >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + value: 2147483648LL + (long long )a >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -391,7 +543,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -401,7 +553,27 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + value: 10LL - (long long )g >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 + line: 19 + column: 1 + function: main + value: 2147483647LL - (long long )a >= 0LL + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 95-witness-mm-escape.c + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -411,7 +583,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -421,7 +593,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -431,7 +603,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main @@ -441,7 +613,7 @@ type: location_invariant location: file_name: 95-witness-mm-escape.c - file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe + file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8 line: 19 column: 1 function: main