Closed
Description
Minimal sample
#include <stdlib.h>
typedef struct {
union {
struct {
uint8_t x;
uint8_t y;
} a;
struct {
uint8_t x;
uint8_t z;
} b;
};
} union_t;
typedef struct {
uint32_t magic;
union_t unions[];
} flex;
int flex_init(flex * flex, size_t num)
{
if (num == 0 || num >= 200) {
return -1;
}
flex->unions[num - 1].b.z = 255;
return 0;
}
int main() {
uint8_t num = nondet_size();
flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t));
int ret = flex_init(pool, num);
if (num > 0 && num < 200) {
__CPROVER_assert(ret == 0, "Accept inside range");
} else {
__CPROVER_assert(ret != 0, "Reject outside range");
}
}
Run log
% cbmc min.c
CBMC version 5.8 64-bit x86_64 macos
Parsing min.c
Converting
Type-checking min
file min.c line 31 function main: function `nondet_size' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 84 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
[1] 24540 segmentation fault cbmc min.c
Exit code = 139