-
Notifications
You must be signed in to change notification settings - Fork 84
Open
Labels
Description
The following obscure examples are from https://blog.aaronballman.com/2013/06/interesting-note-about-the-sizeof-operator/.
#include <stdio.h>
int main( void ) {
int a = 12;
int b = sizeof( ++a );
printf( "%d\n", a );
return 0;
}
should print 12
.
CIL seems to correctly drop the increment side effect here.
#include <stdio.h>
int main(void) {
size_t Count = 10;
size_t Size = sizeof(int[Count++]);
printf("%zu, %zu", Size, Count);
}
should print 40, 11
.
CIL prints foo2.c:5: Warning: POSTINCR or POSTDECR in constant
and somehow leaves no expression in the VLA length, causing us to incorrectly believe that the output would be 0, 10
.
For some reason there's also a tmp
variable in scope, but not used.
Fixing this probably is in conjunction with CIL: CIL has to know which side effects to keep and pull out, but also Goblint has to know when the side-effect–free argument is evaluated to determine warnings (overflows, div by 0, races, etc).