analyzer
analyzer copied to clipboard
Unsound evaluation of `sizeof` expressions
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).