Skip to content

Commit bb3d696

Browse files
karoliinehkaroliineh
committed
Add a cram test for violation witness generation
1 parent 19eb0bd commit bb3d696

File tree

3 files changed

+195
-0
lines changed

3 files changed

+195
-0
lines changed

‎tests/regression/witness/violation.t/callfpointer.c‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
extern void abort(void);
2+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
3+
void reach_error() { __assert_fail("0", "callfpointer.c", 3, "reach_error"); }
4+
5+
6+
void f(void g(int)) {
7+
g(1);
8+
}
9+
10+
void h(int i) {
11+
if(i==1) {
12+
ERROR: {reach_error();abort();}
13+
} else {
14+
15+
}
16+
}
17+
int main(void) {
18+
f(h);
19+
20+
return 0;
21+
}

‎tests/regression/witness/violation.t/callfpointer.expected‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
┌──────────────────────┐
2+
│ _ │
3+
└──────────────────────┘
4+
│
5+
│ Entry main
6+
▼
7+
┌──────────────────────┐
8+
│ _ │
9+
└──────────────────────┘
10+
│
11+
│ InlineEntry '(& h)'
12+
▼
13+
┌──────────────────────┐
14+
│ _ │
15+
└──────────────────────┘
16+
│
17+
│ Entry f
18+
▼
19+
┌──────────────────────┐
20+
│ _ │
21+
└──────────────────────┘
22+
│
23+
│ InlineEntry '(1)'
24+
▼
25+
┌──────────────────────┐
26+
│ _ │
27+
└──────────────────────┘
28+
│
29+
│ Entry h
30+
▼
31+
┌──────────────────────┐
32+
│ _ │
33+
└──────────────────────┘
34+
│
35+
│ Test (i == 1,true)
36+
▼
37+
┌──────────────────────┐
38+
│ _ │
39+
└──────────────────────┘
40+
│
41+
│ InlineEntry '()'
42+
▼
43+
┌──────────────────────┐
44+
│ _ │
45+
└──────────────────────┘
46+
│
47+
│ Entry reach_error
48+
▼
49+
┌──────────────────────┐
50+
│ _ │
51+
└──────────────────────┘

‎tests/regression/witness/violation.t/run.t‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
$ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} callfpointer.c --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --enable ana.wp --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other
2+
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
3+
[Warning][Deadcode] Function 'main' does not return
4+
[Warning][Deadcode] Function 'f' has dead code:
5+
on line 8 (callfpointer.c:8-8)
6+
[Warning][Deadcode] Function 'h' has dead code:
7+
on line 16 (callfpointer.c:16-16)
8+
[Warning][Deadcode] Function 'main' has dead code:
9+
on line 20 (callfpointer.c:20-20)
10+
[Warning][Deadcode] Logical lines of code (LLoC) summary:
11+
live: 8
12+
dead: 3
13+
total lines: 11
14+
[Warning][Deadcode][CWE-571] condition 'i == 1' is always true (callfpointer.c:11:5-11:9)
15+
[Info] fun316main(12)[7] =[Entry main]=> s11(12)[7]
16+
[Info] s11(12)[7] =[InlineEntry '(& h)']=> fun309f(18)[16]@s11(12)[7]
17+
[Info] fun309f(18)[16]@s11(12)[7] =[Entry f]=> s3(18)[16]@s11(12)[7]
18+
[Info] s3(18)[16]@s11(12)[7] =[InlineEntry '(1)']=> fun313h(24)[21]@s3(18)[16]@s11(12)[7]
19+
[Info] fun313h(24)[21]@s3(18)[16]@s11(12)[7] =[Entry h]=> s5(24)[21]@s3(18)[16]@s11(12)[7]
20+
[Info] s5(24)[21]@s3(18)[16]@s11(12)[7] =[Test (i == 1,true)]=> s7(24)[21]@s3(18)[16]@s11(12)[7]
21+
SV-COMP result: unknown
22+
23+
$ graph-easy --as=boxart arg.dot
24+
┌──────────────────────┐
25+
│ _ │
26+
└──────────────────────┘
27+
│
28+
│ Entry main
29+
▼
30+
┌──────────────────────┐
31+
│ _ │
32+
└──────────────────────┘
33+
│
34+
│ InlineEntry '(& h)'
35+
▼
36+
┌──────────────────────┐
37+
│ _ │
38+
└──────────────────────┘
39+
│
40+
│ Entry f
41+
▼
42+
┌──────────────────────┐
43+
│ _ │
44+
└──────────────────────┘
45+
│
46+
│ InlineEntry '(1)'
47+
▼
48+
┌──────────────────────┐
49+
│ _ │
50+
└──────────────────────┘
51+
│
52+
│ Entry h
53+
▼
54+
┌──────────────────────┐
55+
│ _ │
56+
└──────────────────────┘
57+
│
58+
│ Test (i == 1,true)
59+
▼
60+
┌──────────────────────┐
61+
│ _ │
62+
└──────────────────────┘
63+
│
64+
│ InlineEntry '()'
65+
▼
66+
┌──────────────────────┐
67+
│ _ │
68+
└──────────────────────┘
69+
│
70+
│ Entry reach_error
71+
▼
72+
┌──────────────────────┐
73+
│ _ │
74+
└──────────────────────┘
75+
76+
$ yamlWitnessStrip < witness.yml
77+
- entry_type: violation_sequence
78+
content:
79+
- segment:
80+
- waypoint:
81+
type: assumption
82+
location:
83+
file_name: callfpointer.c
84+
line: 18
85+
column: 2
86+
function: main
87+
action: follow
88+
constraint:
89+
value: "1"
90+
format: c_expression
91+
- segment:
92+
- waypoint:
93+
type: assumption
94+
location:
95+
file_name: callfpointer.c
96+
line: 7
97+
column: 2
98+
function: f
99+
action: follow
100+
constraint:
101+
value: "1"
102+
format: c_expression
103+
- segment:
104+
- waypoint:
105+
type: branching
106+
location:
107+
file_name: callfpointer.c
108+
line: 11
109+
column: 2
110+
function: h
111+
action: follow
112+
constraint:
113+
value: "true"
114+
format: c_expression
115+
- segment:
116+
- waypoint:
117+
type: target
118+
location:
119+
file_name: callfpointer.c
120+
line: 12
121+
column: 11
122+
function: h
123+
action: follow

0 commit comments

Comments
 (0)