Skip to content

Commit edfcbd3

Browse files
committed
Add test 56-witness/71-var_eq-str-invariant (issue #1722)
1 parent 765cede commit edfcbd3

File tree

2 files changed

+30
-0
lines changed

2 files changed

+30
-0
lines changed
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
// CRAM PARAM: --set ana.activated[+] var_eq
2+
int main() {
3+
char text = "foobar";
4+
return 0;
5+
}
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
$ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled --enable witness.invariant.other 71-var_eq-str-invariant.c
2+
[Info][Deadcode] Logical lines of code (LLoC) summary:
3+
live: 3
4+
dead: 0
5+
total lines: 3
6+
[Info][Witness] witness generation summary:
7+
location invariants: 1
8+
loop invariants: 0
9+
flow-insensitive invariants: 0
10+
total generation entries: 1
11+
12+
Should not contain invariant with string literal equality:
13+
14+
$ yamlWitnessStrip < witness.yml
15+
- entry_type: invariant_set
16+
content:
17+
- invariant:
18+
type: location_invariant
19+
location:
20+
file_name: 71-var_eq-str-invariant.c
21+
line: 4
22+
column: 3
23+
function: main
24+
value: '"foobar" == text'
25+
format: c_expression

0 commit comments

Comments
 (0)