-
Notifications
You must be signed in to change notification settings - Fork 277
Closed
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersaws-highpending merge
Description
CBMC version: 5.60
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: I expected that at least one of the assertions in this code would fail.
What happened instead: CBMC verification is successful.
This is the test case I created.
#include<assert.h>
struct PtrWrapper {
char* value_c;
};
void fn(struct PtrWrapper wrapper) {
assert(wrapper.value_c == 'B');
}
void indirect(int (*fn_ptr) (char*), char* data) {
fn_ptr(data);
assert(0);
}
int main() {
struct PtrWrapper wrapper;
wrapper.value_c = 'A';
int (*alias) (char*) = (int (*) (char*)) fn;
indirect(alias, &wrapper.value_c);
}
When I run cbmc main.c
, I get the following:
** Results:
missing_fn.c function fn
[fn.assertion.1] line 9 assertion wrapper.value_c == 'B': SUCCESS
missing_fn.c function indirect
[indirect.assertion.1] line 14 assertion 0: SUCCESS
** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL
If I add --pointer-check
there is one failure:
no candidates for dereferenced function pointer: FAILURE
When I execute this code after compiling it with either gcc
or clang
, I get the following assertion failure:
missing_fn: missing_fn.c:9: fn: Assertion `wrapper.value_c == 'B'' failed.
Questions?
- Is this function pointer conversion invalid?
- Even if this function pointer conversion is incorrect, I would expect the
assert(0)
statement to be reachable. Why isn't this the case?
Metadata
Metadata
Assignees
Labels
awsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersaws-highpending merge