Skip to content

Commit e67f9f7

Browse files
tjj2017martin
tjj2017
authored and
martin
committed
Add expected test results.
And, a few minor tweaks to the test cases.
1 parent aa33026 commit e67f9f7

File tree

9 files changed

+116
-73
lines changed

9 files changed

+116
-73
lines changed

‎testsuite/gnat2goto/tests/pointer_to_array/pointer_to_array.adb

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,10 +43,12 @@ begin
4343
pragma Assert (Arr (I) = I);
4444
end loop;
4545

46-
pragma Assert (Arr (3) = 5);
47-
pragma Assert (Ptr (5) = 3);
46+
pragma Assert (Arr (3) = 5, "This should fail");
47+
pragma Assert (Ptr (5) = 3, "This should fail");
48+
pragma Assert (Ptr (3) = 3);
49+
pragma Assert (Ptr (5) = 5);
4850
pragma Assert (Ptr.all (3) = 3);
49-
pragma Assert (Ptr.all (3) = 5);
51+
pragma Assert (Ptr.all (3) = 5, "This should fail");
5052

5153
for I in Index loop
5254
Ptr.all (I) := Index'Last - I + 1;
@@ -62,6 +64,7 @@ begin
6264

6365
pragma Assert (Arr (1) = Index'Last);
6466
pragma Assert (Ptr (Index'Last) = 1);
67+
pragma Assert (Ptr (1) = Index'Last);
6568
pragma Assert (Ptr.all (1) = Index'Last);
6669
pragma Assert (Ptr.all (Index'Last) = 1);
6770

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
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+
[pointer_to_array.assertion.1] line 21 Ada Check assertion: SUCCESS
5+
[pointer_to_array.assertion.2] line 25 assertion Arr (I) = Index'Last - I + 1: SUCCESS
6+
[pointer_to_array.assertion.3] line 31 assertion Ptr (I) = Index'Last - I + 1: SUCCESS
7+
[pointer_to_array.assertion.4] line 39 assertion Ptr (I) = I: SUCCESS
8+
[pointer_to_array.assertion.5] line 43 assertion Arr (I) = I: SUCCESS
9+
[pointer_to_array.assertion.6] line 46 assertion Arr (3) = 5: FAILURE
10+
[pointer_to_array.assertion.7] line 47 assertion Ptr (5) = 3: FAILURE
11+
[pointer_to_array.assertion.8] line 48 assertion Ptr (3) = 3: SUCCESS
12+
[pointer_to_array.assertion.9] line 49 assertion Ptr (5) = 5: SUCCESS
13+
[pointer_to_array.assertion.10] line 50 assertion Ptr.all (3) = 3: SUCCESS
14+
[pointer_to_array.assertion.11] line 51 assertion Ptr.all (3) = 5: FAILURE
15+
[pointer_to_array.assertion.12] line 58 assertion Ptr.all (I) = Index'Last - I + 1: SUCCESS
16+
[pointer_to_array.assertion.13] line 62 assertion Arr (I) = Index'Last - I + 1: SUCCESS
17+
[pointer_to_array.assertion.14] line 65 assertion Arr (1) = Index'Last: SUCCESS
18+
[pointer_to_array.assertion.15] line 66 assertion Ptr (Index'Last) = 1: SUCCESS
19+
[pointer_to_array.assertion.16] line 67 assertion Ptr (1) = Index'Last: SUCCESS
20+
[pointer_to_array.assertion.17] line 68 assertion Ptr.all (1) = Index'Last: SUCCESS
21+
[pointer_to_array.assertion.18] line 69 assertion Ptr.all (Index'Last) = 1: SUCCESS
22+
[pointer_to_array.assertion.19] line 71 assertion Ptr'Length = Index'Last: SUCCESS
23+
[pointer_to_array.assertion.20] line 74 Ada Check assertion: SUCCESS
24+
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/pointer_to_slice/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 Invariant violation - Postcondition
2+

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

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
2+
Error from cbmc pointer_to_slice:
3+
--- begin invariant violation report ---
4+
Invariant check failed
5+
File: simplify_expr.cpp:2660 function: simplify_rec
6+
Condition: as_const(tmp).type() == expr.type()
7+
Reason: Postcondition
8+
Backtrace:
9+
cbmc(+0x24192d) [0x55cf743dc92d]
10+
cbmc(+0x241e8f) [0x55cf743dce8f]
11+
cbmc(+0x16b8cc) [0x55cf743068cc]
12+
cbmc(+0x26c926) [0x55cf74407926]
13+
cbmc(+0x2709fe) [0x55cf7440b9fe]
14+
cbmc(+0x26c7a5) [0x55cf744077a5]
15+
cbmc(+0x2709fe) [0x55cf7440b9fe]
16+
cbmc(+0x26c7a5) [0x55cf744077a5]
17+
cbmc(+0x2709fe) [0x55cf7440b9fe]
18+
cbmc(+0x26c7a5) [0x55cf744077a5]
19+
cbmc(+0x270aba) [0x55cf7440baba]
20+
cbmc(+0x270b37) [0x55cf7440bb37]
21+
cbmc(+0x6237d6) [0x55cf747be7d6]
22+
cbmc(+0x6259c8) [0x55cf747c09c8]
23+
cbmc(+0x625ea3) [0x55cf747c0ea3]
24+
cbmc(+0x4c47bd) [0x55cf7465f7bd]
25+
cbmc(+0x625ede) [0x55cf747c0ede]
26+
cbmc(+0x6260f8) [0x55cf747c10f8]
27+
cbmc(+0x626e3a) [0x55cf747c1e3a]
28+
cbmc(+0x4a2666) [0x55cf7463d666]
29+
cbmc(+0x4a22eb) [0x55cf7463d2eb]
30+
cbmc(+0x2d0402) [0x55cf7446b402]
31+
cbmc(+0x2cb938) [0x55cf74466938]
32+
cbmc(+0x15fb09) [0x55cf742fab09]
33+
cbmc(+0x14f301) [0x55cf742ea301]
34+
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xeb) [0x7ff9ef28209b]
35+
cbmc(+0x1605da) [0x55cf742fb5da]
36+
37+
38+
--- end invariant violation report ---
39+
40+
ERROR code -6 returned by cbmc when processing pointer_to_slice
41+

‎testsuite/gnat2goto/tests/record_access_type/pointer_to_slice.adb

Lines changed: 0 additions & 68 deletions
This file was deleted.

‎testsuite/gnat2goto/tests/record_access_type/record_access_types.adb

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
procedure Record_Access_Types is
2+
type R is record
3+
I : Integer;
4+
end record;
5+
6+
type R_Pointer is access all R;
7+
8+
VR : aliased R;
9+
VP : R_Pointer;
10+
11+
begin
12+
VR.I := 5;
13+
pragma Assert (VR.I = 5);
14+
VP := VR'Access;
15+
VP.all.I := 3;
16+
pragma Assert (VR.I = 5, "This assertion should fail");
17+
pragma Assert (VR.I = 3);
18+
pragma Assert (VP.I = 3);
19+
20+
VP.I := 7;
21+
pragma Assert (VR.I = 5, "This assertion should fail");
22+
pragma Assert (VR.I = 7);
23+
24+
VR.I := 11;
25+
pragma Assert (VP.I = 7, "This assertion should fail");
26+
pragma Assert (VP.I = 11);
27+
28+
end Record_Access_Types;

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
[record_access_types.assertion.1] line 13 assertion VR.I = 5: SUCCESS
2+
[record_access_types.assertion.2] line 16 assertion VR.I = 5: FAILURE
3+
[record_access_types.assertion.3] line 17 assertion VR.I = 3: SUCCESS
4+
[record_access_types.assertion.4] line 18 assertion VP.I = 3: SUCCESS
5+
[record_access_types.assertion.5] line 21 assertion VR.I = 5: FAILURE
6+
[record_access_types.assertion.6] line 22 assertion VR.I = 7: SUCCESS
7+
[record_access_types.assertion.7] line 25 assertion VP.I = 7: FAILURE
8+
[record_access_types.assertion.8] line 26 assertion VP.I = 11: SUCCESS
9+
VERIFICATION FAILED

‎testsuite/gnat2goto/tests/simple_access_Types/simple_access_types.adb

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ begin
99
pragma Assert (I = 5);
1010
Acc := I'Access;
1111
Acc.all := 3;
12-
pragma Assert (I = 5);
13-
pragma Assert (I = 3);
12+
pragma Assert (I = 5, "This assertion should fail");
13+
pragma Assert (I = 3);
1414

1515
end Simple_Access_Types;

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
[simple_access_types.assertion.1] line 9 assertion I = 5: SUCCESS
2+
[simple_access_types.assertion.2] line 12 assertion I = 5: FAILURE
3+
[simple_access_types.assertion.3] line 13 assertion I = 3: SUCCESS
4+
VERIFICATION FAILED

0 commit comments

Comments
 (0)