Skip to content

Add support for void* pointers in goto-harness #5290

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 11 commits into from
Apr 9, 2020
Merged

Add support for void* pointers in goto-harness #5290

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
652bf92
Add test for intializing a void* pointer
Apr 8, 2020
dc62373
Add missing includes to tests
Apr 8, 2020
0151c89
Special case handling for void* pointers
Apr 8, 2020
c65edee
Adapt comment to more accurately reflect generated code
Apr 8, 2020
06a95b5
Combine code for assigning null pointer
Apr 8, 2020
1bbd0f8
Add a test for array of void* pointers
Apr 8, 2020
33294f6
Add tests for when pointer parameters have special semantics
Apr 9, 2020
ff1f4b0
Ensure void* pointers instructed to be arrays are null-initalized
Apr 9, 2020
117f553
Add a test for an array we can initalize
Apr 9, 2020
11a48f4
Consolidate check for void* pointer initilization
Apr 9, 2020
2f2a233
Change assert false assertions
Apr 9, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions regression/goto-harness/void-star-pointer/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,14 @@
#include <assert.h>
#include <stdbool.h>

void test_function(void *input)
{
assert(input == 0);
}

void test_void_array(void *input_array[10])
{
__CPROVER_assume(input_array != 0);
assert(input_array[0] == 0);
assert(false);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 A lot of tests forget this step

}
12 changes: 12 additions & 0 deletions regression/goto-harness/void-star-pointer/test-array.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c
--harness-type call-function --function test_void_array
\[test_void_array\.assertion\.1\] line \d+ assertion input_array\[0\] == 0: SUCCESS
\[test_void_array\.assertion\.2\] line \d+ assertion false: FAILURE
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
Ensure the harness is able to initalize an array of void* pointers where
the array is non-null, but the elements are null.