Apron: Both branches dead when branching over global variable declared as `extern`

[michael-schwarz]

This happens on the nsc benchmark from SV-COMP and seems to have a cause different from what is fixed in #1481.

./goblint --conf conf/traces-rel.json --set dbg.timeout 900 --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval ../bench/svcomp/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i --enable ana.sv-comp.functions

[michael-schwarz]

It seems this is actually a wider issue :cry:

michael@michael-ThinkPad-X1-Carbon-6th:~/Documents/dissertation/bench_raw/0520$ grep -r "Both branches dead" .*
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.box.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.oct.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.oct.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.oct.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/libaco.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/pianobar.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.box.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.box.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/nnn.box.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.oct.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.oct.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/cava.box.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.oct.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.oct.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/nnn.box.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.oct.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/libaco.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.box.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/nnn.oct.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--nsc-ircc.ko.cil.i.box.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/pianobar.cluster12.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/nnn.oct.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.cluster12.txt.html:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/aget_comb.box.txt:[Error][Analyzer][Unsound] Both branches dead
../0522_rel/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i.box.txt.html:[Error][Analyzer][Unsound] Both branches dead

[michael-schwarz]

// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval
#include<pthread.h>
#include<goblint.h>
extern int d;

void* g(void* arg) {
  // Just go multithreaded!
}

void main() {
  pthread_t t;
  pthread_create(&t, 0, g, 0);

  if (d)
  ;
}

[michael-schwarz]

This does not seem to be a problem on master, but was at d8be11708, so it seems that it was fixed in-between.

[michael-schwarz]

Ok, it was #1444 (which I even reviewed :upside_down_face:)