Skip to content

Commit 8f9d75b

Browse files
Petr BauchPetr Bauch
authored andcommitted
Add failing test
Test tries to write and read from and array index.
1 parent c6e123c commit 8f9d75b

File tree

4 files changed

+11
-1
lines changed

4 files changed

+11
-1
lines changed

testsuite/gnat2goto/tests/arrays/arrays.adb

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,4 @@ procedure Arrays is
33
Actual7 : Arr7 := (1,2,3);
44
begin
55
Actual7(1) := 2;
6-
-- pragma Assert(Actual7(1) =2);
76
end Arrays;
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
procedure Arrays_Access is
2+
type Arr7 is array (1 .. 3) of Integer;
3+
Actual7 : Arr7 := (1,2,3);
4+
begin
5+
Actual7(1) := 2;
6+
pragma Assert(Actual7(1) = 2);
7+
end Arrays_Access;
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
ALL XFAIL cbmc crashes when reading gnat2goto output (in symex)
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)