Skip to content

Commit 1487e6e

Browse files
sim642sim642
committed
Emit Unassume from other transfer functions
1 parent 10c28a0 commit 1487e6e

File tree

4 files changed

+137
-0
lines changed

4 files changed

+137
-0
lines changed

‎tests/regression/56-witness/12-apron-unassume-branch.c‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 12-apron-unassume-branch.yml
2+
#include <assert.h>
3+
4+
int main() {
5+
int i = 0;
6+
while (i < 100) {
7+
i++;
8+
}
9+
assert(i == 100); // TODO: avoid widening when unassume inside loop
10+
return 0;
11+
}

‎tests/regression/56-witness/12-apron-unassume-branch.yml‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
- entry_type: loop_invariant
2+
metadata:
3+
format_version: "0.1"
4+
uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
5+
creation_time: 2022-07-26T09:11:03Z
6+
producer:
7+
name: Goblint
8+
version: heads/yaml-witness-unassume-0-g48503c690-dirty
9+
command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
10+
''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
11+
''12-apron-unassume-branch.c'''
12+
task:
13+
input_files:
14+
- 12-apron-unassume-branch.c
15+
input_file_hashes:
16+
12-apron-unassume-branch.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
17+
data_model: LP64
18+
language: C
19+
location:
20+
file_name: 12-apron-unassume-branch.c
21+
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
22+
line: 7
23+
column: 4
24+
function: main
25+
loop_invariant:
26+
string: 99LL - (long long )i >= 0LL
27+
type: assertion
28+
format: C
29+
- entry_type: loop_invariant
30+
metadata:
31+
format_version: "0.1"
32+
uuid: 4e078bcd-9e55-4874-a86e-0563927704a5
33+
creation_time: 2022-07-26T09:11:03Z
34+
producer:
35+
name: Goblint
36+
version: heads/yaml-witness-unassume-0-g48503c690-dirty
37+
command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
38+
''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
39+
''12-apron-unassume-branch.c'''
40+
task:
41+
input_files:
42+
- 12-apron-unassume-branch.c
43+
input_file_hashes:
44+
12-apron-unassume-branch.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
45+
data_model: LP64
46+
language: C
47+
location:
48+
file_name: 12-apron-unassume-branch.c
49+
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
50+
line: 7
51+
column: 4
52+
function: main
53+
loop_invariant:
54+
string: (long long )i >= 0LL
55+
type: assertion
56+
format: C

‎tests/regression/56-witness/13-base-unassume-branch.c‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] unassume --set witness.yaml.unassume 13-base-unassume-branch.yml
2+
#include <assert.h>
3+
4+
int main() {
5+
int i = 0;
6+
while (i < 100) {
7+
i++;
8+
}
9+
assert(i == 100);
10+
return 0;
11+
}
12+
13+
// without unassuming: vars = 13 evals = 14
14+
// with unassuming: vars = 13 evals = 12

‎tests/regression/56-witness/13-base-unassume-branch.yml‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
- entry_type: loop_invariant
2+
metadata:
3+
format_version: "0.1"
4+
uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
5+
creation_time: 2022-07-26T09:11:03Z
6+
producer:
7+
name: Goblint
8+
version: heads/yaml-witness-unassume-0-g48503c690-dirty
9+
command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
10+
''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
11+
''13-base-unassume-branch.c'''
12+
task:
13+
input_files:
14+
- 13-base-unassume-branch.c
15+
input_file_hashes:
16+
13-base-unassume-branch.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
17+
data_model: LP64
18+
language: C
19+
location:
20+
file_name: 13-base-unassume-branch.c
21+
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
22+
line: 7
23+
column: 4
24+
function: main
25+
loop_invariant:
26+
string: 99LL - (long long )i >= 0LL
27+
type: assertion
28+
format: C
29+
- entry_type: loop_invariant
30+
metadata:
31+
format_version: "0.1"
32+
uuid: 4e078bcd-9e55-4874-a86e-0563927704a5
33+
creation_time: 2022-07-26T09:11:03Z
34+
producer:
35+
name: Goblint
36+
version: heads/yaml-witness-unassume-0-g48503c690-dirty
37+
command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
38+
''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
39+
''13-base-unassume-branch.c'''
40+
task:
41+
input_files:
42+
- 13-base-unassume-branch.c
43+
input_file_hashes:
44+
13-base-unassume-branch.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
45+
data_model: LP64
46+
language: C
47+
location:
48+
file_name: 13-base-unassume-branch.c
49+
file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
50+
line: 7
51+
column: 4
52+
function: main
53+
loop_invariant:
54+
string: (long long )i >= 0LL
55+
type: assertion
56+
format: C

0 commit comments

Comments
 (0)