Relational: `exp.hide-std-globals` makes analysis unsound
Opened this issue · 1 comments
michael-schwarz commented
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.
sim642 commented
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.