From a2d47fc541cc4cd18c97fc1b90956ac684832207 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 5 Oct 2022 14:50:46 +0300 Subject: [PATCH 01/15] Add yamlWitnessStrip testing utility --- src/witness/yamlWitnessType.ml | 14 ++++++++++ tests/util/dune | 11 ++++++++ tests/util/yamlWitnessStrip.ml | 48 ++++++++++++++++++++++++++++++++++ 3 files changed, 73 insertions(+) create mode 100644 tests/util/dune create mode 100644 tests/util/yamlWitnessStrip.ml diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index de9fa151d8..1630e05b69 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -111,6 +111,7 @@ struct column: int; function_: string; } + [@@deriving ord] let to_yaml {file_name; file_hash; line; column; function_} = `O [ @@ -138,6 +139,7 @@ struct type_: string; format: string; } + [@@deriving ord] let to_yaml {string; type_; format} = `O [ @@ -160,6 +162,7 @@ struct location: Location.t; loop_invariant: Invariant.t; } + [@@deriving ord] let entry_type = "loop_invariant" @@ -182,6 +185,7 @@ struct location: Location.t; location_invariant: Invariant.t; } + [@@deriving ord] let entry_type = "location_invariant" @@ -203,6 +207,7 @@ struct type t = { flow_insensitive_invariant: Invariant.t; } + [@@deriving ord] let entry_type = "flow_insensitive_invariant" @@ -224,6 +229,7 @@ struct loop_invariant: Invariant.t; precondition: Invariant.t; } + [@@deriving ord] let entry_type = "precondition_loop_invariant" @@ -251,6 +257,7 @@ struct value: string; format: string; } + [@@deriving ord] let invariant_type = "loop_invariant" @@ -282,6 +289,7 @@ struct type t = | LocationInvariant of LocationInvariant.t | LoopInvariant of LoopInvariant.t + [@@deriving ord] let invariant_type = function | LocationInvariant _ -> LocationInvariant.invariant_type @@ -309,6 +317,7 @@ struct type t = { invariant_type: InvariantType.t; } + [@@deriving ord] let to_yaml {invariant_type} = `O [ @@ -327,6 +336,7 @@ struct type t = { content: Invariant.t list; } + [@@deriving ord] let entry_type = "invariant_set" @@ -346,6 +356,7 @@ struct type_: string; file_hash: string; } + [@@deriving ord] let to_yaml {uuid; type_; file_hash} = `O [ @@ -369,6 +380,7 @@ struct type_: string; format: string; } + [@@deriving ord] let to_yaml {string; type_; format} = `O [ @@ -391,6 +403,7 @@ struct target: Target.t; certification: Certification.t; } + [@@deriving ord] let entry_type = "loop_invariant_certificate" @@ -424,6 +437,7 @@ struct | LoopInvariantCertificate of LoopInvariantCertificate.t | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t | InvariantSet of InvariantSet.t + [@@deriving ord] let entry_type = function | LocationInvariant _ -> LocationInvariant.entry_type diff --git a/tests/util/dune b/tests/util/dune new file mode 100644 index 0000000000..6637217651 --- /dev/null +++ b/tests/util/dune @@ -0,0 +1,11 @@ +(executable + (name yamlWitnessStrip) + (libraries + batteries.unthreaded + goblint_std + goblint_lib + yaml + goblint.sites.dune + goblint.build-info.dune) + (flags :standard -open Goblint_std) + (preprocess (pps ppx_deriving.std))) diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml new file mode 100644 index 0000000000..02cd3c57b9 --- /dev/null +++ b/tests/util/yamlWitnessStrip.ml @@ -0,0 +1,48 @@ +open Goblint_lib +open YamlWitnessType + +module StrippedEntry = +struct + type t = { + entry_type: EntryType.t; + } + [@@deriving ord] + + let to_yaml {entry_type} = + `O ([ + ("entry_type", `String (EntryType.entry_type entry_type)); + ] @ EntryType.to_yaml' entry_type) +end + +(* Use set for output, so order is deterministic regardless of Goblint. *) +module StrippedEntrySet = Set.Make (StrippedEntry) + +let main () = + let yaml_str = Batteries.input_all stdin in + let yaml = Yaml.of_string_exn yaml_str in + let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in + + let stripped_entries = List.fold_left (fun stripped_entries yaml_entry -> + match YamlWitnessType.Entry.of_yaml yaml_entry with + | Ok {entry_type; _} -> + let stripped_entry: StrippedEntry.t = {entry_type} in + StrippedEntrySet.add stripped_entry stripped_entries + | Error (`Msg e) -> + Format.eprintf "couldn't parse entry: %s" e; + stripped_entries + ) StrippedEntrySet.empty yaml_entries + in + let stripped_yaml_entries = + StrippedEntrySet.elements stripped_entries + |> List.rev_map StrippedEntry.to_yaml + in + + let stripped_yaml = `A stripped_yaml_entries in + (* to_file/to_string uses a fixed-size buffer... *) + let stripped_yaml_str = match GobYaml.to_string' stripped_yaml with + | Ok text -> text + | Error (`Msg m) -> failwith ("Yaml.to_string: " ^ m) + in + Batteries.output_string Batteries.stdout stripped_yaml_str + +let () = main () From 11c16bc960de657c7e8c5e9a7ef5a1a1f44a11da Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 5 Oct 2022 15:10:49 +0300 Subject: [PATCH 02/15] Strip file hashes from YAML witness cram tests --- tests/util/yamlWitnessStrip.ml | 38 ++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml index 02cd3c57b9..8a5046d6ff 100644 --- a/tests/util/yamlWitnessStrip.ml +++ b/tests/util/yamlWitnessStrip.ml @@ -8,6 +8,43 @@ struct } [@@deriving ord] + let strip_file_hashes {entry_type} = + let stripped_file_hash = "$FILE_HASH" in + let location_strip_file_hash location: Location.t = + {location with file_hash = stripped_file_hash} + in + let target_strip_file_hash target: Target.t = + {target with file_hash = stripped_file_hash} + in + let invariant_strip_file_hash ({invariant_type}: InvariantSet.Invariant.t): InvariantSet.Invariant.t = + let invariant_type: InvariantSet.InvariantType.t = + match invariant_type with + | LocationInvariant x -> + LocationInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariant x -> + LoopInvariant {x with location = location_strip_file_hash x.location} + in + {invariant_type} + in + let entry_type: EntryType.t = + match entry_type with + | LocationInvariant x -> + LocationInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariant x -> + LoopInvariant {x with location = location_strip_file_hash x.location} + | FlowInsensitiveInvariant x -> + FlowInsensitiveInvariant x (* no location to strip *) + | PreconditionLoopInvariant x -> + PreconditionLoopInvariant {x with location = location_strip_file_hash x.location} + | LoopInvariantCertificate x -> + LoopInvariantCertificate {x with target = target_strip_file_hash x.target} + | PreconditionLoopInvariantCertificate x -> + PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target} + | InvariantSet x -> + InvariantSet {content = List.map invariant_strip_file_hash x.content} + in + {entry_type} + let to_yaml {entry_type} = `O ([ ("entry_type", `String (EntryType.entry_type entry_type)); @@ -34,6 +71,7 @@ let main () = in let stripped_yaml_entries = StrippedEntrySet.elements stripped_entries + |> List.map StrippedEntry.strip_file_hashes |> List.rev_map StrippedEntry.to_yaml in From 6c9d719475797fc3bb8bec2f9c86a1d3bec19cc9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 5 Oct 2022 14:51:14 +0300 Subject: [PATCH 03/15] Add cram witness test to 56-witness/05-prec-problem --- tests/regression/56-witness/05-prec-problem.c | 4 +- tests/regression/56-witness/05-prec-problem.t | 89 +++++++++++++++++++ tests/regression/56-witness/dune | 6 ++ 3 files changed, 97 insertions(+), 2 deletions(-) create mode 100644 tests/regression/56-witness/05-prec-problem.t create mode 100644 tests/regression/56-witness/dune diff --git a/tests/regression/56-witness/05-prec-problem.c b/tests/regression/56-witness/05-prec-problem.c index 132ba6b466..276adec093 100644 --- a/tests/regression/56-witness/05-prec-problem.c +++ b/tests/regression/56-witness/05-prec-problem.c @@ -1,4 +1,4 @@ -//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types[+] precondition_loop_invariant +//PARAM: --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' #include #include @@ -9,7 +9,7 @@ int foo(int* ptr1, int* ptr2){ } else { result = 1; } - // Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s] + // cram test checks for precondition invariant soundness return result; } diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t new file mode 100644 index 0000000000..829ddd1ab8 --- /dev/null +++ b/tests/regression/56-witness/05-prec-problem.t @@ -0,0 +1,89 @@ + $ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c + [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:21:5-21:28) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 12 + dead: 0 + total lines: 12 + [Info][Witness] witness generation summary: + total generation entries: 10 + +Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`, +and separately invariants `result == 0` and `result == 1`. +The sound invariant is `result == 1 || result == 0`. + + $ yamlWitnessStrip < witness.yml + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: result == 1 || result == 0 + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: '*ptr2 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 13 + column: 4 + function: foo + loop_invariant: + string: '*ptr1 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 7 + column: 7 + function: foo + loop_invariant: + string: '*ptr2 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C + - entry_type: precondition_loop_invariant + location: + file_name: 05-prec-problem.c + file_hash: $FILE_HASH + line: 7 + column: 7 + function: foo + loop_invariant: + string: '*ptr1 == 5' + type: assertion + format: C + precondition: + string: '*ptr1 == 5 && *ptr2 == 5' + type: assertion + format: C diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune new file mode 100644 index 0000000000..05fce8ddec --- /dev/null +++ b/tests/regression/56-witness/dune @@ -0,0 +1,6 @@ +(env + (_ + (binaries ../../util/yamlWitnessStrip.exe))) + +(cram + (deps (glob_files *.c) %{bin:yamlWitnessStrip})) From 990cf0c892ea54da5fd8d559033444f0d77fab11 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 8 Feb 2024 16:03:19 +0200 Subject: [PATCH 04/15] Add test for synthetic YAML witness invariant locations (PR #758) --- tests/regression/56-witness/dune | 6 +- tests/regression/dune | 9 ++- tests/regression/pr-758.t/pr-758.c | 22 ++++++ tests/regression/pr-758.t/run.t | 119 +++++++++++++++++++++++++++++ 4 files changed, 150 insertions(+), 6 deletions(-) create mode 100644 tests/regression/pr-758.t/pr-758.c create mode 100644 tests/regression/pr-758.t/run.t diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune index 05fce8ddec..23c0dd3290 100644 --- a/tests/regression/56-witness/dune +++ b/tests/regression/56-witness/dune @@ -1,6 +1,2 @@ -(env - (_ - (binaries ../../util/yamlWitnessStrip.exe))) - (cram - (deps (glob_files *.c) %{bin:yamlWitnessStrip})) + (deps (glob_files *.c))) diff --git a/tests/regression/dune b/tests/regression/dune index fdb1d941c2..f68053ef63 100644 --- a/tests/regression/dune +++ b/tests/regression/dune @@ -1,3 +1,10 @@ +(env + (_ + (binaries ../util/yamlWitnessStrip.exe))) + (cram (applies_to :whole_subtree) - (deps %{bin:goblint} (package goblint))) ; need entire package for includes/ + (deps + %{bin:goblint} + (package goblint) ; need entire package for includes/ + %{bin:yamlWitnessStrip})) diff --git a/tests/regression/pr-758.t/pr-758.c b/tests/regression/pr-758.t/pr-758.c new file mode 100644 index 0000000000..87aa41889d --- /dev/null +++ b/tests/regression/pr-758.t/pr-758.c @@ -0,0 +1,22 @@ +// Code from https://github.com/goblint/cil/pull/98 + +int main() { + // for loop + int x = 42; + for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line + // ... + } + + // expression with side effect + int i, k; + i = k = 0; // there shouldn't be invariant k == 0 before this line + + // compound initializers + struct kala { + int kaal; + int hind; + }; + + struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line + return 0; +} diff --git a/tests/regression/pr-758.t/run.t b/tests/regression/pr-758.t/run.t new file mode 100644 index 0000000000..23c327aeb2 --- /dev/null +++ b/tests/regression/pr-758.t/run.t @@ -0,0 +1,119 @@ + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Info][Witness] witness generation summary: + total generation entries: 10 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 6 + column: 2 + function: main + loop_invariant: + string: (0 <= x && (x <= 9 || x <= 10)) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.kaal == 2 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.hind == 3 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C From 066e11a2bd3aecb7bc968ffebb7483e165e6c9fe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 8 Feb 2024 16:16:27 +0200 Subject: [PATCH 05/15] Add test for incorrect YAML witness invariant locations from CIL transformations (issue #1356) --- tests/regression/issue-1356.t/issue-1356.c | 20 ++++++++++++++++++++ tests/regression/issue-1356.t/run.t | 12 ++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/regression/issue-1356.t/issue-1356.c create mode 100644 tests/regression/issue-1356.t/run.t diff --git a/tests/regression/issue-1356.t/issue-1356.c b/tests/regression/issue-1356.t/issue-1356.c new file mode 100644 index 0000000000..b773f6cf66 --- /dev/null +++ b/tests/regression/issue-1356.t/issue-1356.c @@ -0,0 +1,20 @@ +extern int __VERIFIER_nondet_int(void); + +extern void abort(void); +void assume_abort_if_not(int cond) { + if(!cond) {abort();} +} + +int minus(int a, int b) { + assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line + assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line + return a - b; +} + +int main() { + int x, y; + x = __VERIFIER_nondet_int(); + y = __VERIFIER_nondet_int(); + minus(x, y); + return 0; +} diff --git a/tests/regression/issue-1356.t/run.t b/tests/regression/issue-1356.t/run.t new file mode 100644 index 0000000000..7765c02b8d --- /dev/null +++ b/tests/regression/issue-1356.t/run.t @@ -0,0 +1,12 @@ + $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53) + [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:3-11:15) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 13 + dead: 0 + total lines: 13 + [Info][Witness] witness generation summary: + total generation entries: 0 + + $ yamlWitnessStrip < witness.yml + [] From da6987d474fe402ace4bc244b0e68ea89c9984a2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 16:53:02 +0200 Subject: [PATCH 06/15] Deduplicate YAML witness tests from CFG tests --- tests/regression/cfg/issue-1356.t/run.t | 14 +++ tests/regression/cfg/pr-758.t/run.t | 121 +++++++++++++++++++++ tests/regression/issue-1356.t/issue-1356.c | 20 ---- tests/regression/issue-1356.t/run.t | 12 -- tests/regression/pr-758.t/pr-758.c | 22 ---- tests/regression/pr-758.t/run.t | 119 -------------------- 6 files changed, 135 insertions(+), 173 deletions(-) delete mode 100644 tests/regression/issue-1356.t/issue-1356.c delete mode 100644 tests/regression/issue-1356.t/run.t delete mode 100644 tests/regression/pr-758.t/pr-758.c delete mode 100644 tests/regression/pr-758.t/run.t diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t index 78a81aff68..416eadea95 100644 --- a/tests/regression/cfg/issue-1356.t/run.t +++ b/tests/regression/cfg/issue-1356.t/run.t @@ -76,3 +76,17 @@ ┌─────────────────────────────────────────┐ │ return of minus() │ └─────────────────────────────────────────┘ + + + $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53) + [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:3-11:15) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 13 + dead: 0 + total lines: 13 + [Info][Witness] witness generation summary: + total generation entries: 0 + + $ yamlWitnessStrip < witness.yml + [] diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t index d87d9128c7..23eaa2ae39 100644 --- a/tests/regression/cfg/pr-758.t/run.t +++ b/tests/regression/cfg/pr-758.t/run.t @@ -69,3 +69,124 @@ ┌────────────────────────────────────┐ │ return of main() │ └────────────────────────────────────┘ + + + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Info][Witness] witness generation summary: + total generation entries: 10 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 6 + column: 2 + function: main + loop_invariant: + string: (0 <= x && (x <= 9 || x <= 10)) + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.kaal == 2 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 21 + column: 2 + function: main + location_invariant: + string: a.hind == 3 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 20 + column: 2 + function: main + location_invariant: + string: i == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: pr-758.c + file_hash: $FILE_HASH + line: 12 + column: 2 + function: main + location_invariant: + string: x == 10 + type: assertion + format: C diff --git a/tests/regression/issue-1356.t/issue-1356.c b/tests/regression/issue-1356.t/issue-1356.c deleted file mode 100644 index b773f6cf66..0000000000 --- a/tests/regression/issue-1356.t/issue-1356.c +++ /dev/null @@ -1,20 +0,0 @@ -extern int __VERIFIER_nondet_int(void); - -extern void abort(void); -void assume_abort_if_not(int cond) { - if(!cond) {abort();} -} - -int minus(int a, int b) { - assume_abort_if_not(b <= 0 || a >= b - 2147483648); // there shouldn't be invariants 1 <= b and b != 0 before this line - assume_abort_if_not(b >= 0 || a <= b + 2147483647); // there shouldn't be invariants b <= -1 and b != 0 before this line - return a - b; -} - -int main() { - int x, y; - x = __VERIFIER_nondet_int(); - y = __VERIFIER_nondet_int(); - minus(x, y); - return 0; -} diff --git a/tests/regression/issue-1356.t/run.t b/tests/regression/issue-1356.t/run.t deleted file mode 100644 index 7765c02b8d..0000000000 --- a/tests/regression/issue-1356.t/run.t +++ /dev/null @@ -1,12 +0,0 @@ - $ goblint --enable ana.sv-comp.functions --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' issue-1356.c - [Warning][Integer > Overflow][CWE-190] Signed integer overflow (issue-1356.c:10:3-10:53) - [Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (issue-1356.c:11:3-11:15) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 13 - dead: 0 - total lines: 13 - [Info][Witness] witness generation summary: - total generation entries: 0 - - $ yamlWitnessStrip < witness.yml - [] diff --git a/tests/regression/pr-758.t/pr-758.c b/tests/regression/pr-758.t/pr-758.c deleted file mode 100644 index 87aa41889d..0000000000 --- a/tests/regression/pr-758.t/pr-758.c +++ /dev/null @@ -1,22 +0,0 @@ -// Code from https://github.com/goblint/cil/pull/98 - -int main() { - // for loop - int x = 42; - for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line - // ... - } - - // expression with side effect - int i, k; - i = k = 0; // there shouldn't be invariant k == 0 before this line - - // compound initializers - struct kala { - int kaal; - int hind; - }; - - struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line - return 0; -} diff --git a/tests/regression/pr-758.t/run.t b/tests/regression/pr-758.t/run.t deleted file mode 100644 index 23c327aeb2..0000000000 --- a/tests/regression/pr-758.t/run.t +++ /dev/null @@ -1,119 +0,0 @@ - $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 6 - dead: 0 - total lines: 6 - [Info][Witness] witness generation summary: - total generation entries: 10 - - $ yamlWitnessStrip < witness.yml - - entry_type: loop_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 6 - column: 2 - function: main - loop_invariant: - string: (0 <= x && (x <= 9 || x <= 10)) - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 21 - column: 2 - function: main - location_invariant: - string: x == 10 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 21 - column: 2 - function: main - location_invariant: - string: k == 0 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 21 - column: 2 - function: main - location_invariant: - string: i == 0 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 21 - column: 2 - function: main - location_invariant: - string: a.kaal == 2 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 21 - column: 2 - function: main - location_invariant: - string: a.hind == 3 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 20 - column: 2 - function: main - location_invariant: - string: x == 10 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 20 - column: 2 - function: main - location_invariant: - string: k == 0 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 20 - column: 2 - function: main - location_invariant: - string: i == 0 - type: assertion - format: C - - entry_type: location_invariant - location: - file_name: pr-758.c - file_hash: $FILE_HASH - line: 12 - column: 2 - function: main - location_invariant: - string: x == 10 - type: assertion - format: C From 78b8037e97eeaab3c1bc7512ae107199c87c8542 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:21:15 +0200 Subject: [PATCH 07/15] Adapt 56-witness/05-prec-problem to correct precondition_loop_invariant handling --- tests/regression/56-witness/05-prec-problem.c | 3 +- tests/regression/56-witness/05-prec-problem.t | 39 +++---------------- 2 files changed, 7 insertions(+), 35 deletions(-) diff --git a/tests/regression/56-witness/05-prec-problem.c b/tests/regression/56-witness/05-prec-problem.c index 276adec093..08c665ce12 100644 --- a/tests/regression/56-witness/05-prec-problem.c +++ b/tests/regression/56-witness/05-prec-problem.c @@ -9,7 +9,8 @@ int foo(int* ptr1, int* ptr2){ } else { result = 1; } - // cram test checks for precondition invariant soundness + + while (0); // cram test checks for precondition invariant soundness return result; } diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t index 829ddd1ab8..25a3fc619f 100644 --- a/tests/regression/56-witness/05-prec-problem.t +++ b/tests/regression/56-witness/05-prec-problem.t @@ -1,11 +1,12 @@ $ goblint --enable witness.yaml.enabled --enable ana.int.interval --set witness.yaml.entry-types '["precondition_loop_invariant"]' 05-prec-problem.c - [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:21:5-21:28) + [Success][Assert] Assertion "y != z" will succeed (05-prec-problem.c:22:5-22:28) [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 12 + live: 13 dead: 0 - total lines: 12 + total lines: 13 + [Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13) [Info][Witness] witness generation summary: - total generation entries: 10 + total generation entries: 6 Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`, and separately invariants `result == 0` and `result == 1`. @@ -57,33 +58,3 @@ The sound invariant is `result == 1 || result == 0`. string: '*ptr1 == 5 && *ptr2 == 5' type: assertion format: C - - entry_type: precondition_loop_invariant - location: - file_name: 05-prec-problem.c - file_hash: $FILE_HASH - line: 7 - column: 7 - function: foo - loop_invariant: - string: '*ptr2 == 5' - type: assertion - format: C - precondition: - string: '*ptr1 == 5 && *ptr2 == 5' - type: assertion - format: C - - entry_type: precondition_loop_invariant - location: - file_name: 05-prec-problem.c - file_hash: $FILE_HASH - line: 7 - column: 7 - function: foo - loop_invariant: - string: '*ptr1 == 5' - type: assertion - format: C - precondition: - string: '*ptr1 == 5 && *ptr2 == 5' - type: assertion - format: C From 61f94d099dbf9dc448f2451c64a6ba74144482bb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:22:40 +0200 Subject: [PATCH 08/15] Fix invalid locations for precondition_loop_invariant Accidentally shadowed the right loc variable for the loop head. --- src/witness/yamlWitness.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 3eefe5c547..c7694f67be 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -387,7 +387,6 @@ struct let query = Queries.Invariant Invariant.default_context in begin match R.ask_local pre_lvar query with | `Lifted c_inv -> - let loc = Node.location n in (* Find unknowns for which the preceding start state satisfies the precondtion *) let xs = find_matching_states lvar in From 786affd4a0135df7a3221b31ceafed1f3fc8f12b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:24:37 +0200 Subject: [PATCH 09/15] Add TODO about duplicate precondition_loop_invariant entries --- tests/regression/56-witness/05-prec-problem.t | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t index 25a3fc619f..4c7dd02fa9 100644 --- a/tests/regression/56-witness/05-prec-problem.t +++ b/tests/regression/56-witness/05-prec-problem.t @@ -8,6 +8,8 @@ [Info][Witness] witness generation summary: total generation entries: 6 +TODO: Don't generate duplicate entries from each context: should have generated just 3. + Witness shouldn't contain two unsound precondition_loop_invariant-s with precondition `*ptr1 == 5 && *ptr2 == 5`, and separately invariants `result == 0` and `result == 1`. The sound invariant is `result == 1 || result == 0`. From 07430d2c0f225449d5b40426c87e6747481981a9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:27:29 +0200 Subject: [PATCH 10/15] Use yamlWitnessStrip for 56-witness/08-witness-all-locals --- .../56-witness/08-witness-all-locals.t | 59 ++++++++++++++++++- 1 file changed, 57 insertions(+), 2 deletions(-) diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t index 64ab054549..bd7012ec25 100644 --- a/tests/regression/56-witness/08-witness-all-locals.t +++ b/tests/regression/56-witness/08-witness-all-locals.t @@ -6,7 +6,40 @@ [Info][Witness] witness generation summary: total generation entries: 3 -TODO: check witness.yml content with yamlWitnessStrip + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: y == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 7 + column: 4 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C Fewer entries are emitted if locals from nested block scopes are excluded: @@ -19,4 +52,26 @@ Fewer entries are emitted if locals from nested block scopes are excluded: [Info][Witness] witness generation summary: total generation entries: 2 -TODO: check witness.yml content with yamlWitnessStrip + $ yamlWitnessStrip < witness.yml + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 9 + column: 2 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: 08-witness-all-locals.c + file_hash: $FILE_HASH + line: 7 + column: 4 + function: main + location_invariant: + string: x == 5 + type: assertion + format: C From 5d98e2e2b1cba4bd12384c33903387f0e1b210cb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:33:49 +0200 Subject: [PATCH 11/15] Add cram test for YAML witness unrolled loop invariant (issue #1225) --- .../55-loop-unrolling/11-unrolled-loop-invariant.c | 6 ++++++ .../55-loop-unrolling/11-unrolled-loop-invariant.t | 6 ++++++ 2 files changed, 12 insertions(+) create mode 100644 tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c create mode 100644 tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c new file mode 100644 index 0000000000..39e3cbce49 --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c @@ -0,0 +1,6 @@ +int main() { + int i = 0; + while (i < 10) + i++; + return 0; +} diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t new file mode 100644 index 0000000000..c46c468642 --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -0,0 +1,6 @@ + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c + [Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370). + Fatal error: exception Failure("Option error") + [2] + +TODO: Fix loop unrolling with YAML witnesses: https://github.com/goblint/analyzer/pull/1370 From 71015ee5c5f0809fbd5449b2cfec6715d803b91f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 29 Feb 2024 17:58:28 +0200 Subject: [PATCH 12/15] Add YAML witness location tests for loops --- tests/regression/cfg/foo.t/run.t | 156 ++++++++++ tests/regression/cfg/loops.t/run.t | 440 +++++++++++++++++++++++++++++ 2 files changed, 596 insertions(+) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index ba7720d81f..6dcb21863e 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -57,3 +57,159 @@ │ YAML loc: foo.c:5:5-5:8 │ │ │ GraphML: true; server: true │ ─┘ └───────────────────────────────┘ + + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' --set sem.int.signed_overflow assume_none foo.c + [Warning][Integer > Overflow][CWE-190] Signed integer overflow (foo.c:4:5-4:8) + [Warning][Integer > Overflow][CWE-191] Signed integer underflow (foo.c:5:5-5:8) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 6 + dead: 0 + total lines: 6 + [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20) + [Info][Witness] witness generation summary: + total generation entries: 13 + + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 3 + column: 2 + function: main + loop_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 3 + column: 2 + function: main + loop_invariant: + string: 1 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: b == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: a != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: 1 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: b != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: a != 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 5 + column: 4 + function: main + location_invariant: + string: 2 <= a + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: b <= 1 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: b != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: a != 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: 1 <= a + type: assertion + format: C diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index bd9ec42307..febb255865 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -187,4 +187,444 @@ │ │ └──────────────────────────────────────────────────────────────────────────────┘ + $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' loops.c + [Success][Assert] Assertion "1" will succeed (loops.c:14:5-14:23) + [Success][Assert] Assertion "1" will succeed (loops.c:30:5-30:23) + [Success][Assert] Assertion "1" will succeed (loops.c:35:5-35:23) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 18 + dead: 0 + total lines: 18 + [Info][Witness] witness generation summary: + total generation entries: 39 + $ yamlWitnessStrip < witness.yml + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 2 + function: main + loop_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 2 + function: main + loop_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 29 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 29 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 8 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 8 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 41 + column: 4 + function: main + location_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 41 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 41 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + location_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: j == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 35 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 34 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 30 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 30 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 28 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 24 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 24 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 23 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 18 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 14 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 14 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 13 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 9 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 9 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C From 3527e35c0dd49fba0078f6df44c9c18e4569674a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 12:44:56 +0200 Subject: [PATCH 13/15] Add for loop location test with single delcaration initializer --- tests/regression/cfg/loops.t/loops.c | 7 +- tests/regression/cfg/loops.t/run.t | 357 ++++++++++++++++++++------- 2 files changed, 273 insertions(+), 91 deletions(-) diff --git a/tests/regression/cfg/loops.t/loops.c b/tests/regression/cfg/loops.t/loops.c index 0e038e1898..cac7837bcc 100644 --- a/tests/regression/cfg/loops.t/loops.c +++ b/tests/regression/cfg/loops.t/loops.c @@ -30,8 +30,13 @@ int main() { __goblint_check(1); } + // for loop with declaration initializer + for (int j = 0; j < 10; j++) { + __goblint_check(1); + } + // for loop with two initializers - for (int j = (i = 0); i < 10; i++) { + for (int k = (i = 0); i < 10; i++) { __goblint_check(1); } diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index febb255865..bcbe66d126 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -115,106 +115,140 @@ │ __goblint_check(1) │ Neg(i < 10) │ ▼ ▼ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ - │ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:8-34:23 │ │ - │ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:23 (synthetic)) │ │ - │ GraphML: true; server: false │ │ YAML loc: loops.c:34:8-34:23 │ │ - │ │ │ GraphML: true; server: false │ │ - └───────────────────────────────────┘ └───────────────────────────────────┘ │ - │ │ │ - │ │ i = 0 │ - │ ▼ │ - │ ┌───────────────────────────────────┐ │ - │ │ loops.c:34:8-34:23 (synthetic) │ │ - │ │ (loops.c:34:12-34:23 (synthetic)) │ │ - │ │ GraphML: true; server: false │ │ - │ └───────────────────────────────────┘ │ - │ │ │ - ┌────┘ │ j = i │ - │ ▼ │ - │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ - │ │ loops.c:35:5-35:23 │ │ loops.c:34:3-36:3 (synthetic) │ │ - │ │ (loops.c:35:5-35:23) │ │ (loops.c:34:7-34:36 (synthetic)) │ │ - │ │ YAML loc: loops.c:35:5-35:23 │ │ YAML loop: loops.c:34:3-36:3 │ │ - │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ - │ │ │ ◀───────────── │ loop: loops.c:34:3-36:3 │ ◀─────────────────────┼────┐ - │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ - │ │ │ │ │ - │ │ __goblint_check(1) │ Neg(i < 10) │ │ - │ ▼ ▼ │ │ - │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ - │ │ loops.c:34:8-34:23 (synthetic) │ │ loops.c:39:3-39:8 │ │ │ - │ │ (loops.c:34:12-34:23 (synthetic)) │ │ (loops.c:39:3-39:8) │ │ │ - │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:3-39:8 │ │ │ - │ │ │ ─┐ │ GraphML: true; server: true │ │ │ - │ └───────────────────────────────────┘ │ └───────────────────────────────────┘ │ │ - │ │ │ │ │ - │ │ │ i = 0 │ │ - │ │ ▼ │ │ - │ │ ┌───────────────────────────────────┐ │ │ - │ │ │ loops.c:41:5-41:8 │ │ │ - │ │ │ (loops.c:41:5-41:8) │ │ │ - │ │ │ YAML loc: loops.c:41:5-41:8 │ │ │ - │ │ │ YAML loop: loops.c:40:3-42:19 │ │ │ - │ │ │ GraphML: true; server: true │ │ │ - │ │ │ loop: loops.c:40:3-42:19 │ ◀┐ │ │ - │ │ └───────────────────────────────────┘ │ │ │ - │ │ │ │ │ │ - │ │ │ i = i + 1 │ Pos(i < 10) │ │ - │ │ ▼ │ │ │ - │ │ ┌───────────────────────────────────┐ │ │ │ - │ │ │ loops.c:40:3-42:19 (synthetic) │ │ │ │ - │ │ │ (loops.c:42:12-42:19 (synthetic)) │ │ │ │ - │ │ │ GraphML: true; server: false │ ─┘ │ │ - │ │ └───────────────────────────────────┘ │ │ - │ │ │ │ │ - │ │ │ Neg(i < 10) │ │ - │ │ ▼ │ │ - │ │ ┌───────────────────────────────────┐ │ │ - │ │ │ loops.c:44:3-44:11 │ │ │ - │ │ │ (loops.c:44:10-44:11) │ │ │ - │ │ │ YAML loc: loops.c:44:3-44:11 │ │ │ - │ │ │ GraphML: true; server: true │ │ │ - │ │ └───────────────────────────────────┘ │ │ - │ │ │ │ │ - │ │ │ return 0 │ │ - │ │ ▼ │ │ - │ │ ┌───────────────────────────────────┐ │ │ - │ │ │ return of main() │ │ │ - │ │ └───────────────────────────────────┘ │ │ - │ │ │ │ - └─────────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┘ │ - │ │ - │ │ - └──────────────────────────────────────────────────────────────────────────────┘ + │ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:8-34:17 │ │ + │ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:17 (synthetic)) │ │ + │ GraphML: true; server: false │ │ YAML loc: loops.c:34:8-34:17 │ │ + ┌────── │ │ │ GraphML: true; server: false │ │ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ + │ │ │ + │ │ j = 0 │ + │ ▼ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ + │ │ loops.c:35:5-35:23 │ │ loops.c:34:3-36:3 (synthetic) │ │ + │ │ (loops.c:35:5-35:23) │ │ (loops.c:34:7-34:30 (synthetic)) │ │ + │ │ YAML loc: loops.c:35:5-35:23 │ │ YAML loop: loops.c:34:3-36:3 │ │ + │ │ GraphML: true; server: true │ Pos(j < 10) │ GraphML: true; server: false │ j = j + 1 │ + │ │ │ ◀───────────── │ loop: loops.c:34:3-36:3 │ ◀─────────────────────┼────┐ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ __goblint_check(1) │ Neg(j < 10) │ │ + │ ▼ ▼ │ │ + │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ loops.c:34:8-34:17 (synthetic) │ │ loops.c:39:8-39:23 │ │ │ + │ │ (loops.c:34:12-34:17 (synthetic)) │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ + │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:8-39:23 │ │ │ + │ │ │ │ GraphML: true; server: false │ │ │ + │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ │ │ i = 0 │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:39:8-39:23 (synthetic) │ │ │ + │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ + │ │ │ GraphML: true; server: false │ │ │ + │ │ └───────────────────────────────────┘ │ │ + │ │ │ │ │ + │ ┌────┘ │ k = i │ │ + │ │ ▼ │ │ + │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ + │ │ │ loops.c:40:5-40:23 │ │ loops.c:39:3-41:3 (synthetic) │ │ │ + │ │ │ (loops.c:40:5-40:23) │ │ (loops.c:39:7-39:36 (synthetic)) │ │ │ + │ │ │ YAML loc: loops.c:40:5-40:23 │ │ YAML loop: loops.c:39:3-41:3 │ │ │ + │ │ │ GraphML: true; server: true │ Pos(i < 10) │ GraphML: true; server: false │ i = i + 1 │ │ + │ │ │ │ ◀───────────── │ loop: loops.c:39:3-41:3 │ ◀─────────────────────┼────┼─────────────┐ + │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ __goblint_check(1) │ Neg(i < 10) │ │ │ + │ │ ▼ ▼ │ │ │ + │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │ + │ │ │ loops.c:39:8-39:23 (synthetic) │ │ loops.c:44:3-44:8 │ │ │ │ + │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ (loops.c:44:3-44:8) │ │ │ │ + │ │ │ GraphML: true; server: false │ │ YAML loc: loops.c:44:3-44:8 │ │ │ │ + │ │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ i = 0 │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:46:5-46:8 │ │ │ │ + │ │ │ │ (loops.c:46:5-46:8) │ │ │ │ + │ │ │ │ YAML loc: loops.c:46:5-46:8 │ │ │ │ + │ │ │ │ YAML loop: loops.c:45:3-47:19 │ │ │ │ + │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ │ │ loop: loops.c:45:3-47:19 │ ◀┐ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ │ + │ │ │ │ │ │ │ │ + │ │ │ │ i = i + 1 │ Pos(i < 10) │ │ │ + │ │ │ ▼ │ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ │ + │ │ │ │ loops.c:45:3-47:19 (synthetic) │ │ │ │ │ + │ │ │ │ (loops.c:47:12-47:19 (synthetic)) │ │ │ │ │ + │ │ │ │ GraphML: true; server: false │ ─┘ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ │ │ │ Neg(i < 10) │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ loops.c:49:3-49:11 │ │ │ │ + │ │ │ │ (loops.c:49:10-49:11) │ │ │ │ + │ │ │ │ YAML loc: loops.c:49:3-49:11 │ │ │ │ + │ │ │ │ GraphML: true; server: true │ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ │ + │ └────┼────────────────────────────────────┐ │ return 0 │ │ │ + │ │ │ ▼ │ │ │ + │ │ │ ┌───────────────────────────────────┐ │ │ │ + │ │ │ │ return of main() │ │ │ │ + │ │ │ └───────────────────────────────────┘ │ │ │ + │ │ │ │ │ │ + └─────────┼────────────────────────────────────┼─────────────────────────────────────────────────────────────────────────┘ │ │ + │ │ │ │ + │ │ │ │ + │ └──────────────────────────────────────────────────────────────────────────────┘ │ + │ │ + │ │ + └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ $ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' loops.c [Success][Assert] Assertion "1" will succeed (loops.c:14:5-14:23) [Success][Assert] Assertion "1" will succeed (loops.c:30:5-30:23) [Success][Assert] Assertion "1" will succeed (loops.c:35:5-35:23) + [Success][Assert] Assertion "1" will succeed (loops.c:40:5-40:23) [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 18 + live: 20 dead: 0 - total lines: 18 + total lines: 20 [Info][Witness] witness generation summary: - total generation entries: 39 + total generation entries: 53 $ yamlWitnessStrip < witness.yml - entry_type: loop_invariant location: file_name: loops.c file_hash: $FILE_HASH - line: 40 + line: 45 column: 2 function: main loop_invariant: - string: j == 0 + string: k == 0 type: assertion format: C - entry_type: loop_invariant location: file_name: loops.c file_hash: $FILE_HASH - line: 40 + line: 45 + column: 2 + function: main + loop_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 45 column: 2 function: main loop_invariant: @@ -225,7 +259,51 @@ location: file_name: loops.c file_hash: $FILE_HASH - line: 40 + line: 45 + column: 2 + function: main + loop_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 + column: 2 + function: main + loop_invariant: + string: i <= 10 + type: assertion + format: C + - entry_type: loop_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 39 column: 2 function: main loop_invariant: @@ -240,7 +318,7 @@ column: 2 function: main loop_invariant: - string: j == 0 + string: j <= 10 type: assertion format: C - entry_type: loop_invariant @@ -251,7 +329,7 @@ column: 2 function: main loop_invariant: - string: i <= 10 + string: i == 10 type: assertion format: C - entry_type: loop_invariant @@ -262,7 +340,7 @@ column: 2 function: main loop_invariant: - string: 0 <= i + string: 0 <= j type: assertion format: C - entry_type: loop_invariant @@ -375,6 +453,94 @@ string: 0 <= i type: assertion format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 49 + column: 2 + function: main + location_invariant: + string: i == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: i <= 9 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 46 + column: 4 + function: main + location_invariant: + string: 0 <= i + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 44 + column: 2 + function: main + location_invariant: + string: k == 0 + type: assertion + format: C - entry_type: location_invariant location: file_name: loops.c @@ -383,7 +549,7 @@ column: 2 function: main location_invariant: - string: j == 0 + string: j == 10 type: assertion format: C - entry_type: location_invariant @@ -401,18 +567,29 @@ location: file_name: loops.c file_hash: $FILE_HASH - line: 41 + line: 40 column: 4 function: main location_invariant: - string: j == 0 + string: k == 0 type: assertion format: C - entry_type: location_invariant location: file_name: loops.c file_hash: $FILE_HASH - line: 41 + line: 40 + column: 4 + function: main + location_invariant: + string: j == 10 + type: assertion + format: C + - entry_type: location_invariant + location: + file_name: loops.c + file_hash: $FILE_HASH + line: 40 column: 4 function: main location_invariant: @@ -423,7 +600,7 @@ location: file_name: loops.c file_hash: $FILE_HASH - line: 41 + line: 40 column: 4 function: main location_invariant: @@ -438,7 +615,7 @@ column: 2 function: main location_invariant: - string: j == 0 + string: j == 10 type: assertion format: C - entry_type: location_invariant @@ -460,7 +637,7 @@ column: 4 function: main location_invariant: - string: j == 0 + string: j <= 9 type: assertion format: C - entry_type: location_invariant @@ -471,7 +648,7 @@ column: 4 function: main location_invariant: - string: i <= 9 + string: i == 10 type: assertion format: C - entry_type: location_invariant @@ -482,7 +659,7 @@ column: 4 function: main location_invariant: - string: 0 <= i + string: 0 <= j type: assertion format: C - entry_type: location_invariant From b21c8843fe0730303f8d61dc51a307da9edfb2db Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 13:24:59 +0200 Subject: [PATCH 14/15] Fix statement location for for initializer declaration --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- tests/regression/cfg/loops.t/run.t | 12 ++++++------ 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/goblint.opam b/goblint.opam index 5f16b5842a..0d53da497b 100644 --- a/goblint.opam +++ b/goblint.opam @@ -78,7 +78,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/goblint.opam.locked b/goblint.opam.locked index d6c156c9dc..0ec1f95865 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -134,7 +134,7 @@ post-messages: [ pin-depends: [ [ "goblint-cil.2.0.3" - "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" + "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ] [ "ppx_deriving.5.2.1" diff --git a/goblint.opam.template b/goblint.opam.template index a3bb99ff5c..2d5ef10bc9 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -3,7 +3,7 @@ available: os-distribution != "alpine" & arch != "arm64" pin-depends: [ # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed - [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#fb471582d7e9685ab705ba57f7a6675b97ca8f64" ] + [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ] # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252) [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ] ] diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t index bcbe66d126..01216a624e 100644 --- a/tests/regression/cfg/loops.t/run.t +++ b/tests/regression/cfg/loops.t/run.t @@ -115,9 +115,9 @@ │ __goblint_check(1) │ Neg(i < 10) │ ▼ ▼ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ - │ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:8-34:17 │ │ + │ loops.c:29:3-31:3 (synthetic) │ │ loops.c:34:3-36:3 │ │ │ (loops.c:29:7-29:21 (synthetic)) │ │ (loops.c:34:12-34:17 (synthetic)) │ │ - │ GraphML: true; server: false │ │ YAML loc: loops.c:34:8-34:17 │ │ + │ GraphML: true; server: false │ │ YAML loc: loops.c:34:3-36:3 │ │ ┌────── │ │ │ GraphML: true; server: false │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ │ @@ -134,16 +134,16 @@ │ │ __goblint_check(1) │ Neg(j < 10) │ │ │ ▼ ▼ │ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ - │ │ loops.c:34:8-34:17 (synthetic) │ │ loops.c:39:8-39:23 │ │ │ + │ │ loops.c:34:3-36:3 (synthetic) │ │ loops.c:39:3-41:3 │ │ │ │ │ (loops.c:34:12-34:17 (synthetic)) │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ - │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:8-39:23 │ │ │ + │ │ GraphML: true; server: false │ │ YAML loc: loops.c:39:3-41:3 │ │ │ │ │ │ │ GraphML: true; server: false │ │ │ │ └───────────────────────────────────┘ └───────────────────────────────────┘ │ │ │ │ │ │ │ │ │ │ i = 0 │ │ │ │ ▼ │ │ │ │ ┌───────────────────────────────────┐ │ │ - │ │ │ loops.c:39:8-39:23 (synthetic) │ │ │ + │ │ │ loops.c:39:3-41:3 (synthetic) │ │ │ │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ │ │ │ │ GraphML: true; server: false │ │ │ │ │ └───────────────────────────────────┘ │ │ @@ -161,7 +161,7 @@ │ │ │ __goblint_check(1) │ Neg(i < 10) │ │ │ │ │ ▼ ▼ │ │ │ │ │ ┌───────────────────────────────────┐ ┌───────────────────────────────────┐ │ │ │ - │ │ │ loops.c:39:8-39:23 (synthetic) │ │ loops.c:44:3-44:8 │ │ │ │ + │ │ │ loops.c:39:3-41:3 (synthetic) │ │ loops.c:44:3-44:8 │ │ │ │ │ │ │ (loops.c:39:12-39:23 (synthetic)) │ │ (loops.c:44:3-44:8) │ │ │ │ │ │ │ GraphML: true; server: false │ │ YAML loc: loops.c:44:3-44:8 │ │ │ │ │ │ │ │ │ GraphML: true; server: true │ │ │ │ From bb1a2aedc6f93c0b321d0601a3c6e04d123e60e6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 16:37:17 +0200 Subject: [PATCH 15/15] Suppress backtraces in cram tests --- .../regression/55-loop-unrolling/11-unrolled-loop-invariant.t | 3 +++ tests/regression/70-transform/01-ordering.t | 3 +++ 2 files changed, 6 insertions(+) diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index c46c468642..b154f8f57a 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -1,3 +1,6 @@ +Suppress backtrace with code locations, especially for CI. + $ export OCAMLRUNPARAM=b=0 + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c [Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370). Fatal error: exception Failure("Option error") diff --git a/tests/regression/70-transform/01-ordering.t b/tests/regression/70-transform/01-ordering.t index cd7ec8e36a..9ff5a9b739 100644 --- a/tests/regression/70-transform/01-ordering.t +++ b/tests/regression/70-transform/01-ordering.t @@ -1,3 +1,6 @@ +Suppress backtrace with code locations, especially for CI. + $ export OCAMLRUNPARAM=b=0 + Check that assert transform is not allowed to happen after dead code removal $ ./transform.sh --stderr remove_dead_code assert -- 01-empty.c [Error] trans.activated: the 'assert' transform may not occur after the 'remove_dead_code' transform