search

goblint / analyzer

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

Refinement causes (spurious) reports of unreached fixpoints #1455

Closed michael-schwarz closed 4 months ago

michael-schwarz commented 4 months ago

On master (5cd8650a2872341152f48a7d1cd20ac9fa0de994)

 ./goblint --conf /home/goblint/michael-schwarz-dissertation/analyzer/conf/traces.json --set ana.base.privatization lock --enable ana.int.interval --set ana.int.refinement once  ../bench/concrat/cava/cava.c

causes fixpoint errors that are clearly due to missing refinement:

  Difference: Map: [mutex:(lockset:{}, multiplicity:{})] = [base:Map: p =
   {Map: autobars = (Unknown int([0,1]),[0,2147483647],{0, 1}) instead of (Unknown int([0,1]),[0,1],{0, 1})
     Map: is_bin = (Unknown int([-7,7]),[-2147483648,2147483647],{-1, 0, 1}) instead of (Unknown int([-7,7]),[-1,1],{-1, 0, 1})
     Map: stereo = (Unknown int([-7,7]),[-2147483648,2147483647],{-1, 0, 1}) instead of (Unknown int([-7,7]),[-1,1],{-1, 0, 1})
     Map: xaxis = (Unknown int([0,7]),[0,4294967295],{0, 1, 2}) instead of (Unknown int([0,7]),[0,2],{0, 1, 2}) ...}]

The same holds when the refinement strategy is set to fixpoint.

sim642 commented 4 months ago

1005 already covers this, no? It might just be a slightly different instance.

michael-schwarz commented 4 months ago

Yes you're right! I remembered having fixed this at some point, but I guess that as one specific instance only.

Closing as duplicate of #1005