search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
847 stars 262 forks source link

Variable sensitivity ­– functions shouldn’t affect value of globals they don’t write to #5653

Closed hannes-steffenhagen-diffblue closed 3 years ago

hannes-steffenhagen-diffblue commented 3 years ago

Take this test example:

int global = 0;
void remember(void) { }
int main(void) {
  remember();
  global = 1;
  remember();
  assert(global == 1);
}

We would expect the assertion to pass... but it doesn’t because remember has seen the state of global once and forevermore reports it back to us. I believe @martin-cs had some ideas for fixing this in a sound way in the past?

martin-cs commented 3 years ago

Try out --three-way-merge --vsd --vsd-data-dependencies, it is designed for exactly this use case and should work. There is some regression tests that demonstrate it. The paper on the Toyota system has some of the description. I believe that it has been independently invented as "sparse abstract interpretation".

hannes-steffenhagen-diffblue commented 3 years ago

Forgot about that!