goblint/analyzer

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

Opened this issue · 1 comments

In #1444 a bug ignoring external initializers was removed fixing an unsoundness. However, together with bdc1eec, 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.

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.