ultimate-pa
Impossible variable values in FailurePath
Ultimate provides impossible value assignments for certain FailurePath couterexamples.
bmp is of type BITMAP, which is defined to have uint8_t width and height:
typedef struct {
uint8_t width, height;
const uint8_t *data;
} BITMAP;
Ultimate now falsely claims bmp->width to be of the concrete value -255 during FailurePath generation, which is clearly outside of the general range for the uint8_t type and therefore not a valid counterexample:
[L2755] EXPR, FCALL bmp->width
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}, bmp={2919:1024}, bmp->width=-255, i=0, x=0, y=0]
During discussion, @danieldietsch and @jhoenicke acknowledged this problem and noted that this behavior can be attributed to the current implementation of reading from undefined memory of the heap, which does not regard more specific integer type limitations and treats them as full-range int.
longer excerpt:
- CounterExampleResult [Line: 1]: pointer dereference may fail
pointer dereference may fail
We found a FailurePath:
IVAL [\old(_oledbuffer)=null, \old(_oledbuffer)=null, _oledbuffer={1333:2495}]
[L2511] FCALL static uint8_t _oledbuffer[1024];
VAL [_oledbuffer={1334:0}]
[L3094] CALL oledDrawBitmap(0, 0, &bmp_logo_mini_evil)
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}]
[L2755] int i = 0;
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}, bmp={2919:1024}, i=0, x=0, y=0]
[L2755] EXPR, FCALL bmp->width
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}, bmp={2919:1024}, bmp->width=-255, i=0, x=0, y=0]
[L2755] COND TRUE i < bmp->width
[L2756] int j = 0;
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}, bmp={2919:1024}, i=0, j=0, x=0, y=0]
[L2756] FCALL bmp->height
VAL [\old(x)=0, \old(y)=0, _oledbuffer={1334:0}, bmp={2919:1024}, bmp={2919:1024}, i=0, j=0, x=0, y=0]
Version affected: including 0.1.23-97ca168. Currently regression #309 blocks further testing.
Settings:
- AutomizerMemDerefMemtrack.xml
- svcomp-DerefFreeMemtrack-32bit-Automizer_Default.epf
A minified example will be uploaded after the blocking regression is solved.
