Skip to content

Commit 990cf0c

Browse files
sim642sim642
committed
Add test for synthetic YAML witness invariant locations (PR #758)
1 parent 6c9d719 commit 990cf0c

File tree

4 files changed

+150
-6
lines changed

4 files changed

+150
-6
lines changed

‎tests/regression/56-witness/dune‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,2 @@
1-
(env
2-
(_
3-
(binaries ../../util/yamlWitnessStrip.exe)))
4-
51
(cram
6-
(deps (glob_files *.c) %{bin:yamlWitnessStrip}))
2+
(deps (glob_files *.c)))

‎tests/regression/dune‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
(env
2+
(_
3+
(binaries ../util/yamlWitnessStrip.exe)))
4+
15
(cram
26
(applies_to :whole_subtree)
3-
(deps %{bin:goblint} (package goblint))) ; need entire package for includes/
7+
(deps
8+
%{bin:goblint}
9+
(package goblint) ; need entire package for includes/
10+
%{bin:yamlWitnessStrip}))

‎tests/regression/pr-758.t/pr-758.c‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Code from https://github.com/goblint/cil/pull/98
2+
3+
int main() {
4+
// for loop
5+
int x = 42;
6+
for (x = 0; x < 10; x++) { // there shouldn't be invariants x <= 9, x <= 10 and 0 <= x before this line
7+
// ...
8+
}
9+
10+
// expression with side effect
11+
int i, k;
12+
i = k = 0; // there shouldn't be invariant k == 0 before this line
13+
14+
// compound initializers
15+
struct kala {
16+
int kaal;
17+
int hind;
18+
};
19+
20+
struct kala a = {2, 3}; // there shouldn't be invariant a.kaal == 2 before this line
21+
return 0;
22+
}

‎tests/regression/pr-758.t/run.t‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
$ goblint --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["loop_invariant", "location_invariant"]' pr-758.c
2+
[Info][Deadcode] Logical lines of code (LLoC) summary:
3+
live: 6
4+
dead: 0
5+
total lines: 6
6+
[Info][Witness] witness generation summary:
7+
total generation entries: 10
8+
9+
$ yamlWitnessStrip < witness.yml
10+
- entry_type: loop_invariant
11+
location:
12+
file_name: pr-758.c
13+
file_hash: $FILE_HASH
14+
line: 6
15+
column: 2
16+
function: main
17+
loop_invariant:
18+
string: (0 <= x && (x <= 9 || x <= 10))
19+
type: assertion
20+
format: C
21+
- entry_type: location_invariant
22+
location:
23+
file_name: pr-758.c
24+
file_hash: $FILE_HASH
25+
line: 21
26+
column: 2
27+
function: main
28+
location_invariant:
29+
string: x == 10
30+
type: assertion
31+
format: C
32+
- entry_type: location_invariant
33+
location:
34+
file_name: pr-758.c
35+
file_hash: $FILE_HASH
36+
line: 21
37+
column: 2
38+
function: main
39+
location_invariant:
40+
string: k == 0
41+
type: assertion
42+
format: C
43+
- entry_type: location_invariant
44+
location:
45+
file_name: pr-758.c
46+
file_hash: $FILE_HASH
47+
line: 21
48+
column: 2
49+
function: main
50+
location_invariant:
51+
string: i == 0
52+
type: assertion
53+
format: C
54+
- entry_type: location_invariant
55+
location:
56+
file_name: pr-758.c
57+
file_hash: $FILE_HASH
58+
line: 21
59+
column: 2
60+
function: main
61+
location_invariant:
62+
string: a.kaal == 2
63+
type: assertion
64+
format: C
65+
- entry_type: location_invariant
66+
location:
67+
file_name: pr-758.c
68+
file_hash: $FILE_HASH
69+
line: 21
70+
column: 2
71+
function: main
72+
location_invariant:
73+
string: a.hind == 3
74+
type: assertion
75+
format: C
76+
- entry_type: location_invariant
77+
location:
78+
file_name: pr-758.c
79+
file_hash: $FILE_HASH
80+
line: 20
81+
column: 2
82+
function: main
83+
location_invariant:
84+
string: x == 10
85+
type: assertion
86+
format: C
87+
- entry_type: location_invariant
88+
location:
89+
file_name: pr-758.c
90+
file_hash: $FILE_HASH
91+
line: 20
92+
column: 2
93+
function: main
94+
location_invariant:
95+
string: k == 0
96+
type: assertion
97+
format: C
98+
- entry_type: location_invariant
99+
location:
100+
file_name: pr-758.c
101+
file_hash: $FILE_HASH
102+
line: 20
103+
column: 2
104+
function: main
105+
location_invariant:
106+
string: i == 0
107+
type: assertion
108+
format: C
109+
- entry_type: location_invariant
110+
location:
111+
file_name: pr-758.c
112+
file_hash: $FILE_HASH
113+
line: 12
114+
column: 2
115+
function: main
116+
location_invariant:
117+
string: x == 10
118+
type: assertion
119+
format: C

0 commit comments

Comments
 (0)