Skip to content

Unsound evaluation of sizeof expressions #1809

@sim642

Description

@sim642

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).

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions