goblint / analyzer

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

Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis #1498

Open DrMichaelPetter opened 4 weeks ago

DrMichaelPetter commented 4 weeks ago

The following popped up when doing extensive benchmarking, so by creduce we get:

//SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain octagon --set sem.int.signed_overflow assume_none

#include <pthread.h>
#include <stdlib.h>

long *a;
pthread_t e;
void* b() {
  long c = *a;
  for (; (void*)0;) c=c;
}
int main() {
  a = malloc(sizeof(long));
  pthread_create(&e, 0, b, 0);
}

This gives us a [Error][Analyzer][Unsound] both branches over condition '(void *)0' are dead (line:10:7-10:19) , which is the void* bit

I have not much time right now to debug this myself, so I put it in an issue.

sim642 commented 4 weeks ago

This seems to be the same thing as #1440 came to.

michael-schwarz commented 4 weeks ago

Does #1492 fix the issue?

DrMichaelPetter commented 4 weeks ago

Does #1492 fix the issue?

Actually it does, you are right

michael-schwarz commented 4 weeks ago

Great to hear!

DrMichaelPetter commented 4 weeks ago

Great to hear!

Maybe this can serve as another regression test, then.