Skip to content

Commit 24ef4c5

Browse files
thomasspriggsEnrico Steffinlongo
authored andcommitted
Add array read regression test
1 parent 6d5f292 commit 24ef4c5

File tree

2 files changed

+17
-0
lines changed

2 files changed

+17
-0
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
int example_array[10000];
4+
unsigned int index;
5+
__CPROVER_assume(index < 10000);
6+
__CPROVER_assert(example_array[index] != 42, "Array condition");
7+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
array_read.c
3+
4+
Passing problem to incremental SMT2 solving
5+
\[main\.assertion\.1\] line \d+ Array condition: FAILURE
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
--
10+
Test of reading an index of an array.

0 commit comments

Comments
 (0)