diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml index 741b9c0d94..a0a81a7fec 100644 --- a/src/cdomains/c2poDomain.ml +++ b/src/cdomains/c2poDomain.ml @@ -292,8 +292,12 @@ module D = struct let remove_vars_not_in_scope scope cc = let not_in_scope t = let var = T.get_var t in - let var = Var.to_varinfo var in - InvariantCil.var_is_tmp var || not (InvariantCil.var_is_in_scope scope var) + (* let var = Var.to_varinfo var in *) + (* TODO: why Var.to_varinfo doesn't work? *) + match var with + | NormalVar var -> + InvariantCil.var_is_tmp var || not (InvariantCil.var_is_in_scope scope var) + | _ -> true in remove_terms not_in_scope cc end diff --git a/tests/regression/84-c2po/16-loops.t b/tests/regression/84-c2po/16-loops.t new file mode 100644 index 0000000000..f7f57b1b78 --- /dev/null +++ b/tests/regression/84-c2po/16-loops.t @@ -0,0 +1,232 @@ + $ goblint --set ana.activated[+] c2po --set ana.activated[+] startState --set ana.activated[+] taintPartialContexts --set ana.c2po.askbase false --enable witness.yaml.enabled --disable ana.base.invariant.enabled 16-loops.c + [Success][Assert] Assertion "(unsigned long )z == (unsigned long )(x + -1)" will succeed (16-loops.c:26:3-26:31) + [Warning][Assert] Assertion "y == *x2" is unknown. (16-loops.c:27:3-27:28) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 15 + dead: 0 + total lines: 15 + [Info][Witness] witness generation summary: + location invariants: 22 + loop invariants: 2 + flow-insensitive invariants: 0 + total generation entries: 1 + + $ yamlWitnessStrip < witness.yml + - entry_type: invariant_set + content: + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 13 + column: 3 + function: main + value: x2 == x + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 15 + column: 3 + function: main + value: x2 == x + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 16 + column: 3 + function: main + value: x2 == x + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 16 + column: 3 + function: main + value: y == *x + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 19 + column: 5 + function: main + value: '*x == *(z + 1)' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 19 + column: 5 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 20 + column: 5 + function: main + value: x != z + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 20 + column: 5 + function: main + value: x2 != z + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 20 + column: 5 + function: main + value: z != *x + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 21 + column: 5 + function: main + value: x != z + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 21 + column: 5 + function: main + value: x2 != z + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 21 + column: 5 + function: main + value: z != *(x + -1) + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 22 + column: 5 + function: main + value: '*(x + -1) == *z' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 22 + column: 5 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 23 + column: 5 + function: main + value: '*(x + -1) == *z' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 23 + column: 5 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 26 + column: 3 + function: main + value: '*x == *(z + 1)' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 26 + column: 3 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 27 + column: 3 + function: main + value: '*x == *(z + 1)' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 27 + column: 3 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 29 + column: 3 + function: main + value: '*x == *(z + 1)' + format: c_expression + - invariant: + type: location_invariant + location: + file_name: 16-loops.c + line: 29 + column: 3 + function: main + value: z == x + -1 + format: c_expression + - invariant: + type: loop_invariant + location: + file_name: 16-loops.c + line: 18 + column: 3 + function: main + value: '*x == *(z + 1)' + format: c_expression + - invariant: + type: loop_invariant + location: + file_name: 16-loops.c + line: 18 + column: 3 + function: main + value: z == x + -1 + format: c_expression diff --git a/tests/regression/84-c2po/dune b/tests/regression/84-c2po/dune new file mode 100644 index 0000000000..aff6f94276 --- /dev/null +++ b/tests/regression/84-c2po/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c) (glob_files ??-*.yml)))