Skip to content

Commit d79c26c

Browse files
sim642sim642
committed
Add sv-comp/cfg/nondetcall_* to ARG tests
1 parent af5cf22 commit d79c26c

File tree

4 files changed

+258
-1
lines changed

4 files changed

+258
-1
lines changed

‎tests/sv-comp/cfg/nondetcall_same_true-unreach-call.expected‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
┌────────────────────────────────────────┐
2+
│ _ │
3+
└────────────────────────────────────────┘
4+
│
5+
│ Entry main
6+
▼
7+
┌────────────────────────────────────────┐
8+
│ _ │ ·┐
9+
└────────────────────────────────────────┘ :
10+
│ :
11+
│ InlineEntry '()' :
12+
▼ :
13+
┌────────────────────────────────────────┐ :
14+
│ _ │ :
15+
└────────────────────────────────────────┘ :
16+
│ :
17+
│ Entry __VERIFIER_nondet_int :
18+
▼ :
19+
┌────────────────────────────────────────┐ :
20+
│ _ │ : Inlined Proc 'tmp = __VERIFIER_nondet_int()'
21+
└────────────────────────────────────────┘ :
22+
│ :
23+
│ Ret (Some val, __VERIFIER_nondet_int) :
24+
▼ :
25+
┌────────────────────────────────────────┐ :
26+
│ _ │ :
27+
└────────────────────────────────────────┘ :
28+
│ :
29+
│ InlineReturn 'tmp' :
30+
▼ :
31+
┌───┐ Test (tmp,false) ┌────────────────────────────────────────┐ :
32+
│ _ │ ◀───────────────────────────────────────────── │ _ │ ◀┘
33+
└───┘ └────────────────────────────────────────┘
34+
│ │
35+
│ │ Test (tmp,true)
36+
│ ▼
37+
│ ┌────────────────────────────────────────┐
38+
│ │ _ │
39+
│ └────────────────────────────────────────┘
40+
│ │
41+
│ │ Assign 'fun = & foo'
42+
│ ▼
43+
│ Assign 'fun = & foo' ┌────────────────────────────────────────┐
44+
└────────────────────────────────────────────────▶ │ _ │ ·┐
45+
└────────────────────────────────────────┘ :
46+
│ :
47+
│ InlineEntry '(1)' :
48+
▼ :
49+
┌────────────────────────────────────────┐ :
50+
│ _ │ :
51+
└────────────────────────────────────────┘ :
52+
│ :
53+
│ Entry foo :
54+
▼ :
55+
┌────────────────────────────────────────┐ :
56+
┌············································ │ _ │ :
57+
: └────────────────────────────────────────┘ :
58+
: │ :
59+
: │ InlineEntry '(x - 1 < x)' :
60+
: ▼ :
61+
: ┌────────────────────────────────────────┐ :
62+
: │ _ │ :
63+
: └────────────────────────────────────────┘ :
64+
: │ :
65+
: │ Entry __VERIFIER_assert :
66+
: ▼ :
67+
: ┌────────────────────────────────────────┐ :
68+
: │ _ │ :
69+
: └────────────────────────────────────────┘ :
70+
: │ :
71+
: Inlined Proc '__VERIFIER_assert(x - 1 < x)' │ Test (! cond,false) : Inlined Proc '*fun(1)'
72+
: ▼ :
73+
: ┌────────────────────────────────────────┐ :
74+
: │ _ │ :
75+
: └────────────────────────────────────────┘ :
76+
: │ :
77+
: │ Ret (None, __VERIFIER_assert) :
78+
: ▼ :
79+
: ┌────────────────────────────────────────┐ :
80+
: │ _ │ :
81+
: └────────────────────────────────────────┘ :
82+
: │ :
83+
: │ InlineReturn :
84+
: ▼ :
85+
: ┌────────────────────────────────────────┐ :
86+
└···········································▶ │ _ │ :
87+
└────────────────────────────────────────┘ :
88+
│ :
89+
│ Ret (None, foo) :
90+
▼ :
91+
┌────────────────────────────────────────┐ :
92+
│ _ │ :
93+
└────────────────────────────────────────┘ :
94+
│ :
95+
│ InlineReturn :
96+
▼ :
97+
┌────────────────────────────────────────┐ :
98+
│ _ │ ◀┘
99+
└────────────────────────────────────────┘
100+
│
101+
│ Ret (Some 0, main)
102+
▼
103+
┌────────────────────────────────────────┐
104+
│ _ │
105+
└────────────────────────────────────────┘

0 commit comments

Comments
 (0)