CBMC segfaults when using flexible array member with union of struct

[fangyi-zhou]

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

[tautschnig]

Taking a look.

[tautschnig]

Some part of the code generates a struct expression without any operands. I'll continue debugging on Monday.

[tautschnig]

See #1211 for a bug fix.

[fangyi-zhou]

Thanks