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 11#include <assert.h>
2+ #include <stdbool.h>
23
34void test_function (void * input )
45{
56 assert (input == 0 );
67}
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_void_array
4+ \[test_void_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
5+ \[test_void_array\.assertion\.2\] line \d+ 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