File tree Expand file tree Collapse file tree 2 files changed +20
-0
lines changed
regression/goto-harness/void-star-pointer Expand file tree Collapse file tree 2 files changed +20
-0
lines changed Original file line number Diff line number Diff line change 1
1
#include <assert.h>
2
+ #include <stdbool.h>
2
3
3
4
void test_function (void * input )
4
5
{
5
6
assert (input == 0 );
6
7
}
8
+
9
+ void test_void_array (void * input_array [10 ])
10
+ {
11
+ __CPROVER_assume (input_array != 0 );
12
+ assert (input_array [0 ] == 0 );
13
+ assert (false);
14
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+ --harness-type call-function --function test_function
4
+ \[test_void_array\.assertion\.1\] line 11 assertion input_array\[0\] == 0: SUCCESS
5
+ \[test_void_array\.assertion\.2\] line 12 assertion false: FAILURE
6
+ ^VERIFICATION FAILED$
7
+ ^EXIT=10$
8
+ ^SIGNAL=0$
9
+ --
10
+ --
11
+ Ensure the harness is able to initalize an array of void* pointers where
12
+ the array is non-null, but the elements are null.
You can’t perform that action at this time.
0 commit comments