The following code has its assertion succeed when compiled with gcc or clang (with a small amount of code prepended), but not with cbmc:
typedef struct {
unsigned c : 1;
} inner_container_t;
struct container_t {
inner_container_t inner_container;
int i;
};
int main() {
container_t container;
container.inner_container.c = 1;
__CPROVER_printf("before: %d\n", container.inner_container.c);
*(&(&container) -> i) = 0;
__CPROVER_printf("after: %d\n", container.inner_container.c);
__CPROVER_assert(container.inner_container.c, "");
return 0;
}
The prepended code is
#include <stdio.h>
#include <assert.h>
#define __CPROVER_printf printf
void __CPROVER_assert(bool good, const char* msg) {
assert(good);
}
Removing the bitfield allows cbmc to succed, as does removing some of the pointer fuckery.
Am I missing something or is this a bug in cbmc?
The following code has its assertion succeed when compiled with gcc or clang (with a small amount of code prepended), but not with cbmc:
The prepended code is
Removing the bitfield allows cbmc to succed, as does removing some of the pointer fuckery.
Am I missing something or is this a bug in cbmc?