Skip to content

Commit 9c5877f

Browse files
Natasha Yogananda Jeppudanielsn
Natasha Yogananda Jeppu
authored andcommitted
Regression test for --show-array-constraints --json-ui
clang format regression test Adding KNOWNBUG flag to ignore failed test The --smt2 option does not go over arrayst class so no output is generated. The current test thus fails on test-cprover-smt2.
1 parent 1210a32 commit 9c5877f

File tree

2 files changed

+8
-8
lines changed

2 files changed

+8
-8
lines changed
Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
#include<stdlib.h>
1+
#include <stdlib.h>
22
int main()
33
{
4-
size_t array_size;
5-
int a[array_size];
4+
size_t array_size;
5+
int a[array_size];
66

7-
unsigned int index;
8-
a[index] = 1;
7+
unsigned int index;
8+
a[index] = 1;
99

10-
assert(a[index] == 1);
11-
return 0;
10+
assert(a[index] == 1);
11+
return 0;
1212
}

regression/cbmc/array-constraint/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--show-array-constraints --json-ui
44
activate-multi-line-match

0 commit comments

Comments
 (0)