File tree 2 files changed +36
-0
lines changed
regression/cbmc-incr-smt2/structs
2 files changed +36
-0
lines changed Original file line number Diff line number Diff line change
1
+ #include <assert.h>
2
+
3
+ #define ARRAY_SIZE 10000
4
+
5
+ int main ()
6
+ {
7
+ struct my_structt
8
+ {
9
+ int eggs ;
10
+ int ham ;
11
+ };
12
+ struct my_structt struct_array [ARRAY_SIZE ];
13
+ int x ;
14
+ __CPROVER_assume (x > 0 && x < ARRAY_SIZE );
15
+ struct_array [x ].eggs = 3 ;
16
+ assert (struct_array [x ].eggs + struct_array [x ].ham != 10 );
17
+ assert (struct_array [x ].eggs + struct_array [x ].ham != 11 );
18
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ large_array_of_struct_nondet_index.c
3
+ --trace
4
+ Passing problem to incremental SMT2 solving
5
+ ^EXIT=10$
6
+ ^SIGNAL=0$
7
+ line 16 assertion struct_array\[x\]\.eggs \+ struct_array\[x\]\.ham != 10\: FAILURE
8
+ line 17 assertion struct_array\[x\]\.eggs \+ struct_array\[x\]\.ham != 11\: FAILURE
9
+ \{\s*\.eggs=\d+,\s*\.ham=7\s*\}
10
+ \{\s*\.eggs=\d+,\s*\.ham=8\s*\}
11
+ x=\d{1,4}\s
12
+ struct_array\[\(signed long int\)x\]\.eggs=3
13
+ --
14
+ --
15
+ This test covers support for examples with large arrays of structs using nondet
16
+ indexes including trace generation. This combination of features is chosen in
17
+ order to avoid array cell sensitivity or struct field sensitivity simplifying
18
+ away the relevant `member_exprt` and `with_exprt` expressions.
You can’t perform that action at this time.
0 commit comments