ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
200 stars 41 forks source link

Bug: Designated initializers for C structs broken in C translation #693

Open bahnwaerter opened 1 week ago

bahnwaerter commented 1 week ago

Designated initializers for C structs according to C99 are broken in Ultimate in version 0.3.0-dev-f28124e. The C translation plugin does not seem to correctly handle the lookup of C struct field names from specified initializers, thus violating the assertion in the CTranslationUtil in line 253.

The following reduced program from a large embedded program can be used to reproduce the issue:

typedef unsigned char __uint8_t;
typedef short unsigned int __uint16_t;
typedef long unsigned int __uint32_t;

typedef __uint8_t uint8_t;
typedef __uint16_t uint16_t;
typedef __uint32_t uint32_t;

typedef struct {
    uint8_t Channel;
    uint8_t Direction;
    uint16_t Value;
    uint8_t Gain;
} SB17_SENSOR_DATA_t;

typedef struct {
    uint32_t Timestamp;
    SB17_SENSOR_DATA_t Reading;
} SB17_SENSOR_READING_t;

typedef struct {
    /* ... */
    uint32_t default_value;
} cyhal_timer_t;

uint32_t cyhal_timer_read(const cyhal_timer_t *obj);

static SB17_SENSOR_DATA_t _sb17_read_single_sensor_value();

static cyhal_timer_t timestamp_timer;

int main()
{
    /* ... */
    SB17_SENSOR_DATA_t data = _sb17_read_single_sensor_value();
    /* ... */
    SB17_SENSOR_READING_t reading = { .Timestamp = cyhal_timer_read(&timestamp_timer), .Reading = data };
    /* ... */
    return 0;
}