Skip to content

Commit e68253e

Browse files
tjj2017tjj2017
committed
Add tests for ASVAT modelling features.
1 parent f72fe39 commit e68253e

File tree

10 files changed

+354
-0
lines changed

10 files changed

+354
-0
lines changed

‎testsuite/gnat2goto/tests/nondet_enum_sub/nondet_enum_sub.adb

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
procedure Nondet_Enum_Sub is
2+
type My_Enum is (one, two, three, four, five, six);
3+
4+
subtype My_Sub_Enum is My_Enum range two .. four;
5+
6+
subtype Sub_Int is Integer range 0 .. 10;
7+
8+
function Nondet_My_Enum return My_Enum
9+
with Annotate => (ASVAT, Nondet_Function),
10+
Import;
11+
12+
function In_Type (V : My_Enum) return Boolean
13+
with Annotate => (ASVAT, In_Type_Function),
14+
Import;
15+
16+
function Nondet_Sub_Int return Sub_Int
17+
with Annotate => (ASVAT, Nondet_Function),
18+
Import;
19+
20+
function In_Type (V : Sub_Int) return Boolean
21+
with Annotate => (ASVAT, In_Type_Function),
22+
Import;
23+
24+
Var_Enum : My_Enum := three;
25+
Var_Sub_Int : Sub_Int := 5;
26+
begin
27+
pragma Assert (In_Type (Var_Enum));
28+
pragma Assert (In_Type (Var_Sub_Int));
29+
30+
Var_Enum := Nondet_My_Enum;
31+
Var_Sub_Int := Nondet_Sub_Int;
32+
33+
pragma Assert (In_Type (Var_Enum));
34+
pragma Assert (In_Type (Var_Sub_Int));
35+
36+
pragma Assume (In_Type (Var_Enum));
37+
pragma Assume (In_Type (Var_Sub_Int));
38+
39+
pragma Assert (Var_Enum in Var_Enum);
40+
pragma Assert (Var_Enum >= My_Enum'First and Var_Enum <= My_Enum'Last);
41+
pragma Assert (In_Type (Var_Sub_Int));
42+
pragma Assert (Var_Sub_Int in Sub_Int);
43+
44+
end Nondet_Enum_Sub;

‎testsuite/gnat2goto/tests/nondet_enum_sub/test.out

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
[nondet_enum_sub.assertion.1] line 27 assertion In_Type (Var_Enum): SUCCESS
2+
[nondet_enum_sub.assertion.2] line 28 assertion In_Type (Var_Sub_Int): SUCCESS
3+
[nondet_enum_sub.assertion.3] line 33 assertion In_Type (Var_Enum): SUCCESS
4+
[nondet_enum_sub.assertion.4] line 34 assertion In_Type (Var_Sub_Int): FAILURE
5+
[nondet_enum_sub.assertion.5] line 39 assertion Var_Enum in Var_Enum: SUCCESS
6+
[nondet_enum_sub.assertion.6] line 40 assertion Var_Enum >= My_Enum'First and Var_Enum <= My_Enum'Last: SUCCESS
7+
[nondet_enum_sub.assertion.7] line 41 assertion In_Type (Var_Sub_Int): SUCCESS
8+
[nondet_enum_sub.assertion.8] line 42 assertion Var_Sub_Int in Sub_Int: SUCCESS
9+
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/nondet_enum_sub/test.py

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()

‎testsuite/gnat2goto/tests/nondet_function/nondet_function.adb

Lines changed: 208 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,208 @@
1+
procedure Nondet_Function is
2+
type My_Int is range -500 .. 500;
3+
4+
subtype My_Sub_Int is My_Int range 0 .. 100;
5+
6+
type My_Enum is (one, two, three, four, five, six);
7+
8+
subtype My_Sub_Enum is My_Enum range two .. four;
9+
10+
subtype Index is Integer range 1 .. 10;
11+
12+
type Fixed_Array is array (Index) of My_Sub_Int;
13+
14+
type Rec is record
15+
A : My_Sub_Int;
16+
B : My_Enum;
17+
I : Index;
18+
D : Fixed_Array;
19+
end record;
20+
21+
function Nondet_My_Int return My_Int
22+
with Annotate => (ASVAT, Nondet_Function),
23+
Import;
24+
25+
function Nondet_My_Sub_Int return My_Sub_Int
26+
with Annotate => (ASVAT, Nondet_Function),
27+
Import;
28+
29+
function Nondet_My_Enum return My_Enum
30+
with Annotate => (ASVAT, Nondet_Function),
31+
Import;
32+
33+
function Nondet_My_Sub_Enum return My_Sub_Enum
34+
with Annotate => (ASVAT, Nondet_Function),
35+
Import;
36+
37+
function Nondet_Integer return Integer
38+
with Annotate => (ASVAT, Nondet_Function),
39+
Import;
40+
41+
function Nondet_Index return Index
42+
with Annotate => (ASVAT, Nondet_Function),
43+
Import;
44+
45+
function In_Type (V : My_Int) return Boolean
46+
with Annotate => (ASVAT, In_Type_Function),
47+
Import;
48+
49+
function In_Type_Sub (V : My_Sub_Int) return Boolean
50+
with Annotate => (ASVAT, In_Type_Function),
51+
Import;
52+
53+
function In_Type (V : My_Enum) return Boolean
54+
with Annotate => (ASVAT, In_Type_Function),
55+
Import;
56+
57+
function In_Type_Sub (V : My_Sub_Enum) return Boolean
58+
with Annotate => (ASVAT, In_Type_Function),
59+
Import;
60+
61+
function In_Type (I : Index) return Boolean
62+
with Annotate => (ASVAT, In_Type_Function),
63+
Import;
64+
65+
Var_My_Int : My_Int := 3;
66+
Var_My_Sub_Int : My_Sub_Int := 5;
67+
68+
Var_My_Enum : My_Enum := one;
69+
Var_My_Sub_Enum : My_Sub_Enum := three;
70+
71+
Var_Fixed_Array : Fixed_Array := (others => 7);
72+
Var_Rec : Rec := (11,
73+
five,
74+
1,
75+
(others => 13));
76+
begin
77+
pragma Assert (Var_My_Int = 3);
78+
pragma Assert (Var_My_Sub_Int = 5);
79+
80+
pragma Assert (Var_My_Enum = one);
81+
pragma Assert (Var_My_Sub_Enum = three);
82+
83+
for I in Index loop
84+
pragma Assert (Var_Fixed_Array (I) = 7);
85+
end loop;
86+
87+
pragma Assert (Var_Rec.A = 11);
88+
pragma Assert (Var_Rec.B = five);
89+
pragma Assert (Var_Rec.I = 1);
90+
for I in Index loop
91+
pragma Assert (Var_Rec.D (I) = 13);
92+
end loop;
93+
94+
pragma Assert (Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last);
95+
pragma Assert (Var_My_Sub_Int in My_Sub_Int);
96+
97+
pragma Assert (Var_My_Enum in My_Enum);
98+
pragma Assert (Var_My_Sub_Enum in My_Sub_Enum);
99+
100+
for I in Index loop
101+
pragma Assert (Var_Fixed_Array (I) in My_Sub_Int);
102+
end loop;
103+
104+
pragma Assert (Var_Rec.A in My_Sub_Int);
105+
pragma Assert (Var_Rec.B in My_Enum);
106+
pragma Assert (Var_Rec.I in Index);
107+
for I in Index loop
108+
pragma Assert (Var_Rec.D (I) in My_Sub_Int);
109+
end loop;
110+
111+
pragma Assert (In_Type (Var_My_Int));
112+
pragma Assert (In_Type_Sub (Var_My_Sub_Int));
113+
pragma Assert (In_Type (Var_My_Enum));
114+
pragma Assert (In_Type_Sub (Var_My_Sub_Enum));
115+
116+
for I in Index loop
117+
pragma Assert (In_Type_Sub (Var_Fixed_Array (I)));
118+
end loop;
119+
120+
pragma Assert (In_Type_Sub (Var_Rec.A));
121+
pragma Assert (In_Type (Var_Rec.B));
122+
pragma Assert (In_Type (Var_Rec.I));
123+
for I in Index loop
124+
pragma Assert (In_Type_Sub (Var_Rec.D (I)));
125+
end loop;
126+
127+
Var_My_Int := Nondet_My_Int;
128+
pragma Assert (Var_My_Int = 3);
129+
130+
Var_My_Sub_Int := Nondet_My_Sub_Int;
131+
pragma Assert (Var_My_Sub_Int = 5);
132+
133+
Var_My_Enum := Nondet_My_Enum;
134+
pragma Assert (Var_My_Enum = one);
135+
136+
Var_My_Sub_Enum := Nondet_My_Sub_Enum;
137+
pragma Assert (Var_My_Sub_Enum = three);
138+
139+
for I in Var_Fixed_Array'Range loop
140+
Var_Fixed_Array (I) := Nondet_My_Sub_Int;
141+
end loop;
142+
143+
for I in Index loop
144+
pragma Assert (Var_Fixed_Array (I) = 7);
145+
end loop;
146+
147+
Var_Rec :=
148+
(Nondet_My_Sub_Int, Nondet_My_Enum, Nondet_Index,
149+
(others => Nondet_My_Sub_Int));
150+
151+
pragma Assert (Var_Rec.A = 11);
152+
pragma Assert (Var_Rec.B = five);
153+
pragma Assert (Var_Rec.I = 1);
154+
for I in Index loop
155+
pragma Assert (Var_Rec.D (I) = 13);
156+
end loop;
157+
158+
pragma Assert (Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last);
159+
pragma Assert (Var_My_Sub_Int in My_Sub_Int);
160+
161+
pragma Assert (Var_My_Enum in My_Enum);
162+
pragma Assert (Var_My_Sub_Enum in My_Sub_Enum);
163+
164+
for I in Index loop
165+
pragma Assert (Var_Fixed_Array (I) in My_Sub_Int);
166+
end loop;
167+
168+
pragma Assert (Var_Rec.A in My_Sub_Int);
169+
pragma Assert (Var_Rec.B in My_Enum);
170+
pragma Assert (Var_Rec.I in Index);
171+
for I in Index loop
172+
pragma Assert (Var_Rec.D (I) in My_Sub_Int);
173+
end loop;
174+
175+
pragma Assume (In_Type (Var_My_Int));
176+
pragma Assume (In_Type_Sub (Var_My_Sub_Int));
177+
pragma Assume (In_Type (Var_My_Enum));
178+
pragma Assume (In_Type_Sub (Var_My_Sub_Enum));
179+
180+
for I in Index loop
181+
pragma Assume (In_Type_Sub (Var_Fixed_Array (I)));
182+
end loop;
183+
184+
pragma Assume (In_Type_Sub (Var_Rec.A));
185+
pragma Assume (In_Type (Var_Rec.B));
186+
pragma Assume (In_Type (Var_Rec.I));
187+
for I in Index loop
188+
pragma Assume (In_Type_Sub (Var_Rec.D (I)));
189+
end loop;
190+
191+
pragma Assert (Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last);
192+
pragma Assert (Var_My_Sub_Int in My_Sub_Int);
193+
194+
pragma Assert (Var_My_Enum >= My_Enum'First and Var_My_Enum <= My_Enum'Last);
195+
pragma Assert (Var_My_Sub_Enum in My_Sub_Enum);
196+
197+
for I in Index loop
198+
pragma Assert (Var_Fixed_Array (I) in My_Sub_Int);
199+
end loop;
200+
201+
pragma Assert (Var_Rec.A in My_Sub_Int);
202+
pragma Assert (Var_Rec.B in My_Enum);
203+
pragma Assert (Var_Rec.I in Index);
204+
for I in Index loop
205+
pragma Assert (Var_Rec.D (I) in My_Sub_Int);
206+
end loop;
207+
208+
end Nondet_Function;

‎testsuite/gnat2goto/tests/nondet_function/test.out

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
[precondition_instance.1] file <internal> memcpy src/dst overlap: SUCCESS
2+
[precondition_instance.2] file <internal> memcpy source region readable: SUCCESS
3+
[precondition_instance.3] file <internal> memcpy destination region writeable: SUCCESS
4+
[precondition_instance.4] file <internal> memcpy src/dst overlap: SUCCESS
5+
[precondition_instance.5] file <internal> memcpy source region readable: SUCCESS
6+
[precondition_instance.6] file <internal> memcpy destination region writeable: SUCCESS
7+
[precondition_instance.7] file <internal> memcpy src/dst overlap: SUCCESS
8+
[precondition_instance.8] file <internal> memcpy source region readable: SUCCESS
9+
[precondition_instance.9] file <internal> memcpy destination region writeable: SUCCESS
10+
[nondet_function.assertion.2] line 77 assertion Var_My_Int = 3: SUCCESS
11+
[nondet_function.assertion.3] line 78 assertion Var_My_Sub_Int = 5: SUCCESS
12+
[nondet_function.assertion.4] line 80 assertion Var_My_Enum = one: SUCCESS
13+
[nondet_function.assertion.5] line 81 assertion Var_My_Sub_Enum = three: SUCCESS
14+
[nondet_function.assertion.1] line 84 Ada Check assertion: SUCCESS
15+
[nondet_function.assertion.6] line 84 assertion Var_Fixed_Array (I) = 7: SUCCESS
16+
[nondet_function.assertion.7] line 87 assertion Var_Rec.A = 11: SUCCESS
17+
[nondet_function.assertion.8] line 88 assertion Var_Rec.B = five: SUCCESS
18+
[nondet_function.assertion.9] line 89 assertion Var_Rec.I = 1: SUCCESS
19+
[nondet_function.assertion.10] line 91 assertion Var_Rec.D (I) = 13: SUCCESS
20+
[nondet_function.assertion.11] line 94 assertion Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last: SUCCESS
21+
[nondet_function.assertion.12] line 95 assertion Var_My_Sub_Int in My_Sub_Int: SUCCESS
22+
[nondet_function.assertion.13] line 97 assertion Var_My_Enum in My_Enum: SUCCESS
23+
[nondet_function.assertion.14] line 98 assertion Var_My_Sub_Enum in My_Sub_Enum: SUCCESS
24+
[nondet_function.assertion.15] line 101 assertion Var_Fixed_Array (I) in My_Sub_Int: SUCCESS
25+
[nondet_function.assertion.16] line 104 assertion Var_Rec.A in My_Sub_Int: SUCCESS
26+
[nondet_function.assertion.17] line 105 assertion Var_Rec.B in My_Enum: SUCCESS
27+
[nondet_function.assertion.18] line 106 assertion Var_Rec.I in Index: SUCCESS
28+
[nondet_function.assertion.19] line 108 assertion Var_Rec.D (I) in My_Sub_Int: SUCCESS
29+
[nondet_function.assertion.20] line 111 assertion In_Type (Var_My_Int): SUCCESS
30+
[nondet_function.assertion.21] line 112 assertion In_Type_Sub (Var_My_Sub_Int): SUCCESS
31+
[nondet_function.assertion.22] line 113 assertion In_Type (Var_My_Enum): SUCCESS
32+
[nondet_function.assertion.23] line 114 assertion In_Type_Sub (Var_My_Sub_Enum): SUCCESS
33+
[nondet_function.assertion.24] line 117 assertion In_Type_Sub (Var_Fixed_Array (I)): SUCCESS
34+
[nondet_function.assertion.25] line 120 assertion In_Type_Sub (Var_Rec.A): SUCCESS
35+
[nondet_function.assertion.26] line 121 assertion In_Type (Var_Rec.B): SUCCESS
36+
[nondet_function.assertion.27] line 122 assertion In_Type (Var_Rec.I): SUCCESS
37+
[nondet_function.assertion.28] line 124 assertion In_Type_Sub (Var_Rec.D (I)): SUCCESS
38+
[nondet_function.assertion.29] line 128 assertion Var_My_Int = 3: FAILURE
39+
[nondet_function.assertion.30] line 131 assertion Var_My_Sub_Int = 5: FAILURE
40+
[nondet_function.assertion.31] line 134 assertion Var_My_Enum = one: FAILURE
41+
[nondet_function.assertion.32] line 137 assertion Var_My_Sub_Enum = three: FAILURE
42+
[nondet_function.assertion.33] line 144 assertion Var_Fixed_Array (I) = 7: FAILURE
43+
[nondet_function.assertion.34] line 151 assertion Var_Rec.A = 11: FAILURE
44+
[nondet_function.assertion.35] line 152 assertion Var_Rec.B = five: FAILURE
45+
[nondet_function.assertion.36] line 153 assertion Var_Rec.I = 1: FAILURE
46+
[nondet_function.assertion.37] line 155 assertion Var_Rec.D (I) = 13: FAILURE
47+
[nondet_function.assertion.38] line 158 assertion Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last: FAILURE
48+
[nondet_function.assertion.39] line 159 assertion Var_My_Sub_Int in My_Sub_Int: FAILURE
49+
[nondet_function.assertion.40] line 161 assertion Var_My_Enum in My_Enum: FAILURE
50+
[nondet_function.assertion.41] line 162 assertion Var_My_Sub_Enum in My_Sub_Enum: FAILURE
51+
[nondet_function.assertion.42] line 165 assertion Var_Fixed_Array (I) in My_Sub_Int: FAILURE
52+
[nondet_function.assertion.43] line 168 assertion Var_Rec.A in My_Sub_Int: FAILURE
53+
[nondet_function.assertion.44] line 169 assertion Var_Rec.B in My_Enum: FAILURE
54+
[nondet_function.assertion.45] line 170 assertion Var_Rec.I in Index: FAILURE
55+
[nondet_function.assertion.46] line 172 assertion Var_Rec.D (I) in My_Sub_Int: FAILURE
56+
[nondet_function.assertion.47] line 191 assertion Var_My_Int >= My_Int'First and Var_My_Int <= My_Int'Last: SUCCESS
57+
[nondet_function.assertion.48] line 192 assertion Var_My_Sub_Int in My_Sub_Int: SUCCESS
58+
[nondet_function.assertion.49] line 194 assertion Var_My_Enum >= My_Enum'First and Var_My_Enum <= My_Enum'Last: SUCCESS
59+
[nondet_function.assertion.50] line 195 assertion Var_My_Sub_Enum in My_Sub_Enum: SUCCESS
60+
[nondet_function.assertion.51] line 198 assertion Var_Fixed_Array (I) in My_Sub_Int: SUCCESS
61+
[nondet_function.assertion.52] line 201 assertion Var_Rec.A in My_Sub_Int: SUCCESS
62+
[nondet_function.assertion.53] line 202 assertion Var_Rec.B in My_Enum: SUCCESS
63+
[nondet_function.assertion.54] line 203 assertion Var_Rec.I in Index: SUCCESS
64+
[nondet_function.assertion.55] line 205 assertion Var_Rec.D (I) in My_Sub_Int: SUCCESS
65+
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/nondet_function/test.py

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()

‎testsuite/gnat2goto/tests/nondet_int/nondet_int.adb

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
procedure Nondet_Int is
2+
type My_Int is range -500 .. 500;
3+
4+
V : My_Int := 7;
5+
6+
function Nondet return My_Int
7+
with Annotate => (ASVAT, Nondet_Function),
8+
Import;
9+
10+
function In_Type (M : My_Int) return Boolean
11+
with Annotate => (ASVAT, In_Type_Function),
12+
Import;
13+
14+
begin
15+
pragma Assert (V >= My_Int'First and V <= My_Int'Last);
16+
pragma Assert (V in My_Int);
17+
end Nondet_Int;

‎testsuite/gnat2goto/tests/nondet_int/test.opt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
ALL XFAIL cbmc fails with "unimplemented"
2+

‎testsuite/gnat2goto/tests/nondet_int/test.out

Whitespace-only changes.

‎testsuite/gnat2goto/tests/nondet_int/test.py

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()

0 commit comments

Comments
 (0)