goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

Relational: `exp.hide-std-globals` makes analysis unsound #1486

Open michael-schwarz opened 4 months ago

michael-schwarz commented 4 months ago

In #1444 a bug ignoring external initializers was removed fixing an unsoundness. However, together with https://github.com/goblint/analyzer/commit/bdc1eec5883ff3819479e891d5305f5c39d96c4b, we are now sound for most programs, except those that use specific variable names:

// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval
// Checks that branching over extern or volatile variables does not yield to both branches being dead.
// This fails unless exp.hide-std-globals is deactivated
#include<pthread.h>
extern int optind;

void* a(void* arg) {
  // Just go multi-threaded
}

void main() {
  pthread_t t;

  pthread_create(&t, 0, a, 0);
  if (optind)
    ;

  // __goblint_check(1); // Reachable
}

This materializes, e.g., on aget from our benchmark suite. For #1417, I simply deactivate this option globally.

sim642 commented 4 months ago

Hmm, yes, real-world programs might actually use these. The sensible thing would be to actually check if the program uses them other than the declaration.