analyzer
analyzer copied to clipboard
Published
20 hours ago •
goblint
goblint
Fixpoints not being reached
SV-Comp '21 revealed a few example programs where we do not reach the fixpoint:
- [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml
- [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.1.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
- [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml
- [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.3.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
- [ ] c/seq-mthreaded-reduced/pals_opt-floodmax.5.4.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
- [ ] c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c (surfaced after merging 0f9f068ee53e181405515191ad8b9ffe66800fc9)
It seems like this is an issue with the thread analysis (#130), if I disable it, we reach the fixpoint.
For the first example at least, var_eq contains an additional equality between {0, main__i2} in what the solver computed, that is not there for the RHS, but he value domain still knows that main__i2 is [0,0].
Could it be that this is also the fault of WitnessConstraints.PathSensitive3? Or does this also happen outside of SV-COMP mode?
Because it seems weird that the difference is in var_eq but somehow thread is at fault? Also #130 and #137 didn't really change the local domain of thread, so I'm not sure how it's related. But I also haven't looked into this yet.
This is weird. I just locally tried all of them under the svcomp21 tag and they all give unknown result instead of ERROR (verify). So I can't even reproduce this issue.
The log for those from SV-COMP preruns also has a weird like:
Difference: Set (Set (Cil expressions)): These are fine!.
That seems to indicate there is no problem.
I can reproduce it, also with the latest commits on master:
./goblint --conf conf/svcomp21.json --sets ana.specification ../../sv-comp/sv-benchmarks/c/properties/unreach-call.prp --html ../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
Fixpoint not reached at node 501 "(int )assert__arg == 0" on pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:722 (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:722)
Solver computed:
(mapping {
[Topped Set (variables):{}, lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, assert__arg, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
Unit:(), Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{}, MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (Unknown int([-7,7]),[-1,127])
p12_new -> (-1,[-1,-1])
ep12 -> (Unknown int([0,1]),[0,1])
p13 -> (0,[0,0])
p13_old -> (Unknown int([-7,7]),[-1,127])
p13_new -> (-1,[-1,-1])
ep13 -> (Unknown int([0,1]),[0,1])
p14 -> (0,[0,0])
p14_old -> (Unknown int([-7,7]),[-1,127])
p14_new -> (-1,[-1,-1])
ep14 -> (Unknown int([0,1]),[0,1])
p21 -> (0,[0,0])
p21_old -> (Unknown int([-7,7]),[-1,127])
p21_new -> (-1,[-1,-1])
ep21 -> (Unknown int([0,1]),[0,1])
p23 -> (0,[0,0])
p23_old -> (Unknown int([-7,7]),[-1,127])
p23_new -> (-1,[-1,-1])
ep23 -> (Unknown int([0,1]),[0,1])
p24 -> (0,[0,0])
p24_old -> (Unknown int([-7,7]),[-1,127])
p24_new -> (-1,[-1,-1])
ep24 -> (Unknown int([0,1]),[0,1])
p31 -> (0,[0,0])
p31_old -> (Unknown int([-7,7]),[-1,127])
p31_new -> (-1,[-1,-1])
ep31 -> (Unknown int([0,1]),[0,1])
p32 -> (0,[0,0])
p32_old -> (Unknown int([-7,7]),[-1,127])
p32_new -> (-1,[-1,-1])
ep32 -> (Unknown int([0,1]),[0,1])
p34 -> (0,[0,0])
p34_old -> (Unknown int([-7,7]),[-1,127])
p34_new -> (-1,[-1,-1])
ep34 -> (Unknown int([0,1]),[0,1])
p41 -> (0,[0,0])
p41_old -> (Unknown int([-7,7]),[-1,127])
p41_new -> (-1,[-1,-1])
ep41 -> (Unknown int([0,1]),[0,1])
p42 -> (0,[0,0])
p42_old -> (Unknown int([-7,7]),[-1,127])
p42_new -> (-1,[-1,-1])
ep42 -> (Unknown int([0,1]),[0,1])
p43 -> (0,[0,0])
p43_old -> (Unknown int([-7,7]),[-1,127])
p43_new -> (-1,[-1,-1])
ep43 -> (Unknown int([0,1]),[0,1])
id1 -> (Unknown int([-7,7]),[0,127])
r1 -> (Unknown int([0,8]),[0,255])
st1 -> (Unknown int([0,7]),[0,127])
nl1 -> (Unknown int([0,7]),[0,127])
m1 -> (Unknown int([-7,7]),[-128,127])
max1 -> (Unknown int([-7,7]),[0,127])
mode1 -> (Unknown int([0,7]),[0,1])
newmax1 -> (Unknown int([0,1]),[0,1])
id2 -> (Unknown int([-7,7]),[0,127])
r2 -> (Unknown int([0,8]),[0,255])
st2 -> (Unknown int([0,7]),[0,127])
nl2 -> (Unknown int([0,7]),[0,127])
m2 -> (Unknown int([-7,7]),[-128,127])
max2 -> (Unknown int([-7,7]),[0,127])
mode2 -> (Unknown int([0,7]),[0,1])
newmax2 -> (Unknown int([0,1]),[0,1])
id3 -> (Unknown int([-7,7]),[0,127])
r3 -> (Unknown int([0,8]),[0,255])
st3 -> (Unknown int([0,7]),[0,127])
nl3 -> (Unknown int([0,7]),[0,127])
m3 -> (Unknown int([-7,7]),[-128,127])
max3 -> (Unknown int([-7,7]),[0,127])
mode3 -> (Unknown int([0,7]),[0,1])
newmax3 -> (Unknown int([0,1]),[0,1])
id4 -> (Unknown int([-7,7]),[0,127])
r4 -> (Unknown int([0,8]),[0,255])
st4 -> (Unknown int([0,7]),[0,127])
nl4 -> (Unknown int([0,7]),[0,127])
m4 -> (Unknown int([-7,7]),[-128,127])
max4 -> (Unknown int([-7,7]),[0,127])
mode4 -> (Unknown int([0,7]),[0,1])
newmax4 -> (Unknown int([0,1]),[0,1])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (1,[1,1])
__return_3681 -> (Unknown int([0,7]),[0,1])
}
Local {
main__c1 -> (Unknown int([0,7]),[0,1])
main__i2 -> (0,[0,0])
init__r121 -> (Unknown int([0,1]),[0,1])
init__r131 -> (Unknown int([0,1]),[0,1])
init__r141 -> (Unknown int([0,1]),[0,1])
init__r211 -> (Unknown int([0,1]),[0,1])
init__r231 -> (Unknown int([0,1]),[0,1])
init__r241 -> (Unknown int([0,1]),[0,1])
init__r311 -> (Unknown int([0,1]),[0,1])
init__r321 -> (Unknown int([0,1]),[0,1])
init__r341 -> (Unknown int([0,1]),[0,1])
init__r411 -> (Unknown int([0,1]),[0,1])
init__r421 -> (Unknown int([0,1]),[0,1])
init__r431 -> (Unknown int([0,1]),[0,1])
init__r122 -> (Unknown int([0,1]),[0,1])
init__tmp -> (Unknown int([0,7]),[0,1])
init__r132 -> (Unknown int([0,1]),[0,1])
init__tmp___0 -> (Unknown int([0,7]),[0,1])
init__r142 -> (Unknown int([0,1]),[0,1])
init__tmp___1 -> (Unknown int([0,7]),[0,1])
init__r212 -> (Unknown int([0,1]),[0,1])
init__tmp___2 -> (Unknown int([0,7]),[0,1])
init__r232 -> (Unknown int([0,1]),[0,1])
init__tmp___3 -> (Unknown int([0,7]),[0,1])
init__r242 -> (Unknown int([0,1]),[0,1])
init__tmp___4 -> (Unknown int([0,7]),[0,1])
init__r312 -> (Unknown int([0,1]),[0,1])
init__tmp___5 -> (Unknown int([0,7]),[0,1])
init__r322 -> (Unknown int([0,1]),[0,1])
init__tmp___6 -> (Unknown int([0,7]),[0,1])
init__r342 -> (Unknown int([0,1]),[0,1])
init__tmp___7 -> (Unknown int([0,7]),[0,1])
init__r412 -> (Unknown int([0,1]),[0,1])
init__tmp___8 -> (Unknown int([0,7]),[0,1])
init__r422 -> (Unknown int([0,1]),[0,1])
init__tmp___9 -> (Unknown int([0,7]),[0,1])
init__r432 -> (Unknown int([0,1]),[0,1])
init__tmp___10 -> (Unknown int([0,7]),[0,1])
init__r123 -> (Not {0}([0,1]),[0,1])
init__tmp___11 -> (Unknown int([0,7]),[0,1])
init__r133 -> (Not {0}([0,1]),[0,1])
init__tmp___12 -> (Unknown int([0,7]),[0,1])
init__r143 -> (Not {0}([0,1]),[0,1])
init__tmp___13 -> (Unknown int([0,7]),[0,1])
init__r213 -> (Not {0}([0,1]),[0,1])
init__tmp___14 -> (Unknown int([0,7]),[0,1])
init__r233 -> (Not {0}([0,1]),[0,1])
init__tmp___15 -> (Unknown int([0,7]),[0,1])
init__r243 -> (Not {0}([0,1]),[0,1])
init__tmp___16 -> (Unknown int([0,7]),[0,1])
init__r313 -> (Not {0}([0,1]),[0,1])
init__tmp___17 -> (Unknown int([0,7]),[0,1])
init__r323 -> (Not {0}([0,1]),[0,1])
init__tmp___18 -> (Unknown int([0,7]),[0,1])
init__r343 -> (Not {0}([0,1]),[0,1])
init__tmp___19 -> (Unknown int([0,7]),[0,1])
init__r413 -> (Not {0}([0,1]),[0,1])
init__tmp___20 -> (Unknown int([0,7]),[0,1])
init__r423 -> (Not {0}([0,1]),[0,1])
init__tmp___21 -> (Unknown int([0,7]),[0,1])
init__r433 -> (Not {0}([0,1]),[0,1])
init__tmp___22 -> (Unknown int([0,7]),[0,1])
init__tmp___23 -> (1,[1,1])
node1__newmax -> (Unknown int([0,7]),[0,1])
node2__newmax -> (Unknown int([0,7]),[0,1])
node3__newmax -> (Unknown int([0,7]),[0,1])
node4__newmax -> (Unknown int([0,7]),[0,1])
check__tmp -> (Unknown int([0,7]),[0,1])
__tmp_1 -> (Unknown int([0,1]),[0,1])
assert__arg -> (Unknown int([0,1]),[0,1])
node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
}
Global {
main -> (Unknown int([0,1]),[0,1])
}
}, mapping {
}),
lifted proglines:Unknown line] -> {((node 500 "assert__arg = __tmp_1;", [Topped Set (variables):{},
lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{},
Unit:(),
Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{},
MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (0,[0,0])
p12_new -> (0,[0,0])
ep12 -> (0,[0,0])
p13 -> (0,[0,0])
p13_old -> (0,[0,0])
p13_new -> (0,[0,0])
ep13 -> (0,[0,0])
p14 -> (0,[0,0])
p14_old -> (0,[0,0])
p14_new -> (0,[0,0])
ep14 -> (0,[0,0])
p21 -> (0,[0,0])
p21_old -> (0,[0,0])
p21_new -> (0,[0,0])
ep21 -> (0,[0,0])
p23 -> (0,[0,0])
p23_old -> (0,[0,0])
p23_new -> (0,[0,0])
ep23 -> (0,[0,0])
p24 -> (0,[0,0])
p24_old -> (0,[0,0])
p24_new -> (0,[0,0])
ep24 -> (0,[0,0])
p31 -> (0,[0,0])
p31_old -> (0,[0,0])
p31_new -> (0,[0,0])
ep31 -> (0,[0,0])
p32 -> (0,[0,0])
p32_old -> (0,[0,0])
p32_new -> (0,[0,0])
ep32 -> (0,[0,0])
p34 -> (0,[0,0])
p34_old -> (0,[0,0])
p34_new -> (0,[0,0])
ep34 -> (0,[0,0])
p41 -> (0,[0,0])
p41_old -> (0,[0,0])
p41_new -> (0,[0,0])
ep41 -> (0,[0,0])
p42 -> (0,[0,0])
p42_old -> (0,[0,0])
p42_new -> (0,[0,0])
ep42 -> (0,[0,0])
p43 -> (0,[0,0])
p43_old -> (0,[0,0])
p43_new -> (0,[0,0])
ep43 -> (0,[0,0])
id1 -> (0,[0,0])
r1 -> (0,[0,0])
st1 -> (0,[0,0])
nl1 -> (0,[0,0])
m1 -> (0,[0,0])
max1 -> (0,[0,0])
mode1 -> (0,[0,0])
newmax1 -> (0,[0,0])
id2 -> (0,[0,0])
r2 -> (0,[0,0])
st2 -> (0,[0,0])
nl2 -> (0,[0,0])
m2 -> (0,[0,0])
max2 -> (0,[0,0])
mode2 -> (0,[0,0])
newmax2 -> (0,[0,0])
id3 -> (0,[0,0])
r3 -> (0,[0,0])
st3 -> (0,[0,0])
nl3 -> (0,[0,0])
m3 -> (0,[0,0])
max3 -> (0,[0,0])
mode3 -> (0,[0,0])
newmax3 -> (0,[0,0])
id4 -> (0,[0,0])
r4 -> (0,[0,0])
st4 -> (0,[0,0])
nl4 -> (0,[0,0])
m4 -> (0,[0,0])
max4 -> (0,[0,0])
mode4 -> (0,[0,0])
newmax4 -> (0,[0,0])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (0,[0,0])
__return_3681 -> (0,[0,0])
}
}, mapping {
}),
lifted proglines:Unknown line], [Topped Set (variables):{},
lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
Unit:(),
Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{},
MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (Unknown int([-7,7]),[-1,127])
p12_new -> (-1,[-1,-1])
ep12 -> (Unknown int([0,1]),[0,1])
p13 -> (0,[0,0])
p13_old -> (Unknown int([-7,7]),[-1,127])
p13_new -> (-1,[-1,-1])
ep13 -> (Unknown int([0,1]),[0,1])
p14 -> (0,[0,0])
p14_old -> (Unknown int([-7,7]),[-1,127])
p14_new -> (-1,[-1,-1])
ep14 -> (Unknown int([0,1]),[0,1])
p21 -> (0,[0,0])
p21_old -> (Unknown int([-7,7]),[-1,127])
p21_new -> (-1,[-1,-1])
ep21 -> (Unknown int([0,1]),[0,1])
p23 -> (0,[0,0])
p23_old -> (Unknown int([-7,7]),[-1,127])
p23_new -> (-1,[-1,-1])
ep23 -> (Unknown int([0,1]),[0,1])
p24 -> (0,[0,0])
p24_old -> (Unknown int([-7,7]),[-1,127])
p24_new -> (-1,[-1,-1])
ep24 -> (Unknown int([0,1]),[0,1])
p31 -> (0,[0,0])
p31_old -> (Unknown int([-7,7]),[-1,127])
p31_new -> (-1,[-1,-1])
ep31 -> (Unknown int([0,1]),[0,1])
p32 -> (0,[0,0])
p32_old -> (Unknown int([-7,7]),[-1,127])
p32_new -> (-1,[-1,-1])
ep32 -> (Unknown int([0,1]),[0,1])
p34 -> (0,[0,0])
p34_old -> (Unknown int([-7,7]),[-1,127])
p34_new -> (-1,[-1,-1])
ep34 -> (Unknown int([0,1]),[0,1])
p41 -> (0,[0,0])
p41_old -> (Unknown int([-7,7]),[-1,127])
p41_new -> (-1,[-1,-1])
ep41 -> (Unknown int([0,1]),[0,1])
p42 -> (0,[0,0])
p42_old -> (Unknown int([-7,7]),[-1,127])
p42_new -> (-1,[-1,-1])
ep42 -> (Unknown int([0,1]),[0,1])
p43 -> (0,[0,0])
p43_old -> (Unknown int([-7,7]),[-1,127])
p43_new -> (-1,[-1,-1])
ep43 -> (Unknown int([0,1]),[0,1])
id1 -> (Unknown int([-7,7]),[0,127])
r1 -> (Unknown int([0,8]),[0,255])
st1 -> (Unknown int([0,7]),[0,127])
nl1 -> (Unknown int([0,7]),[0,127])
m1 -> (Unknown int([-7,7]),[-128,127])
max1 -> (Unknown int([-7,7]),[0,127])
mode1 -> (Unknown int([0,7]),[0,1])
newmax1 -> (Unknown int([0,1]),[0,1])
id2 -> (Unknown int([-7,7]),[0,127])
r2 -> (Unknown int([0,8]),[0,255])
st2 -> (Unknown int([0,7]),[0,127])
nl2 -> (Unknown int([0,7]),[0,127])
m2 -> (Unknown int([-7,7]),[-128,127])
max2 -> (Unknown int([-7,7]),[0,127])
mode2 -> (Unknown int([0,7]),[0,1])
newmax2 -> (Unknown int([0,1]),[0,1])
id3 -> (Unknown int([-7,7]),[0,127])
r3 -> (Unknown int([0,8]),[0,255])
st3 -> (Unknown int([0,7]),[0,127])
nl3 -> (Unknown int([0,7]),[0,127])
m3 -> (Unknown int([-7,7]),[-128,127])
max3 -> (Unknown int([-7,7]),[0,127])
mode3 -> (Unknown int([0,7]),[0,1])
newmax3 -> (Unknown int([0,1]),[0,1])
id4 -> (Unknown int([-7,7]),[0,127])
r4 -> (Unknown int([0,8]),[0,255])
st4 -> (Unknown int([0,7]),[0,127])
nl4 -> (Unknown int([0,7]),[0,127])
m4 -> (Unknown int([-7,7]),[-128,127])
max4 -> (Unknown int([-7,7]),[0,127])
mode4 -> (Unknown int([0,7]),[0,1])
newmax4 -> (Unknown int([0,1]),[0,1])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (1,[1,1])
__return_3681 -> (Unknown int([0,7]),[0,1])
}
Local {
main__c1 -> (Unknown int([0,7]),[0,1])
main__i2 -> (0,[0,0])
init__r121 -> (Unknown int([0,1]),[0,1])
init__r131 -> (Unknown int([0,1]),[0,1])
init__r141 -> (Unknown int([0,1]),[0,1])
init__r211 -> (Unknown int([0,1]),[0,1])
init__r231 -> (Unknown int([0,1]),[0,1])
init__r241 -> (Unknown int([0,1]),[0,1])
init__r311 -> (Unknown int([0,1]),[0,1])
init__r321 -> (Unknown int([0,1]),[0,1])
init__r341 -> (Unknown int([0,1]),[0,1])
init__r411 -> (Unknown int([0,1]),[0,1])
init__r421 -> (Unknown int([0,1]),[0,1])
init__r431 -> (Unknown int([0,1]),[0,1])
init__r122 -> (Unknown int([0,1]),[0,1])
init__tmp -> (Unknown int([0,7]),[0,1])
init__r132 -> (Unknown int([0,1]),[0,1])
init__tmp___0 -> (Unknown int([0,7]),[0,1])
init__r142 -> (Unknown int([0,1]),[0,1])
init__tmp___1 -> (Unknown int([0,7]),[0,1])
init__r212 -> (Unknown int([0,1]),[0,1])
init__tmp___2 -> (Unknown int([0,7]),[0,1])
init__r232 -> (Unknown int([0,1]),[0,1])
init__tmp___3 -> (Unknown int([0,7]),[0,1])
init__r242 -> (Unknown int([0,1]),[0,1])
init__tmp___4 -> (Unknown int([0,7]),[0,1])
init__r312 -> (Unknown int([0,1]),[0,1])
init__tmp___5 -> (Unknown int([0,7]),[0,1])
init__r322 -> (Unknown int([0,1]),[0,1])
init__tmp___6 -> (Unknown int([0,7]),[0,1])
init__r342 -> (Unknown int([0,1]),[0,1])
init__tmp___7 -> (Unknown int([0,7]),[0,1])
init__r412 -> (Unknown int([0,1]),[0,1])
init__tmp___8 -> (Unknown int([0,7]),[0,1])
init__r422 -> (Unknown int([0,1]),[0,1])
init__tmp___9 -> (Unknown int([0,7]),[0,1])
init__r432 -> (Unknown int([0,1]),[0,1])
init__tmp___10 -> (Unknown int([0,7]),[0,1])
init__r123 -> (Not {0}([0,1]),[0,1])
init__tmp___11 -> (Unknown int([0,7]),[0,1])
init__r133 -> (Not {0}([0,1]),[0,1])
init__tmp___12 -> (Unknown int([0,7]),[0,1])
init__r143 -> (Not {0}([0,1]),[0,1])
init__tmp___13 -> (Unknown int([0,7]),[0,1])
init__r213 -> (Not {0}([0,1]),[0,1])
init__tmp___14 -> (Unknown int([0,7]),[0,1])
init__r233 -> (Not {0}([0,1]),[0,1])
init__tmp___15 -> (Unknown int([0,7]),[0,1])
init__r243 -> (Not {0}([0,1]),[0,1])
init__tmp___16 -> (Unknown int([0,7]),[0,1])
init__r313 -> (Not {0}([0,1]),[0,1])
init__tmp___17 -> (Unknown int([0,7]),[0,1])
init__r323 -> (Not {0}([0,1]),[0,1])
init__tmp___18 -> (Unknown int([0,7]),[0,1])
init__r343 -> (Not {0}([0,1]),[0,1])
init__tmp___19 -> (Unknown int([0,7]),[0,1])
init__r413 -> (Not {0}([0,1]),[0,1])
init__tmp___20 -> (Unknown int([0,7]),[0,1])
init__r423 -> (Not {0}([0,1]),[0,1])
init__tmp___21 -> (Unknown int([0,7]),[0,1])
init__r433 -> (Not {0}([0,1]),[0,1])
init__tmp___22 -> (Unknown int([0,7]),[0,1])
init__tmp___23 -> (1,[1,1])
node1__newmax -> (Unknown int([0,7]),[0,1])
node2__newmax -> (Unknown int([0,7]),[0,1])
node3__newmax -> (Unknown int([0,7]),[0,1])
node4__newmax -> (Unknown int([0,7]),[0,1])
check__tmp -> (Unknown int([0,7]),[0,1])
__tmp_1 -> (Unknown int([0,1]),[0,1])
assert__arg -> (Unknown int([0,1]),[0,1])
node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
}
Global {
main -> (Unknown int([0,1]),[0,1])
}
}, mapping {
}),
lifted proglines:Unknown line]), Assign 'assert__arg = __tmp_1' )}
}, mapping {
})
Right-Hand-Side:
(mapping {
[Topped Set (variables):{}, lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{{__tmp_1, assert__arg, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
Unit:(), Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{}, MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (Unknown int([-7,7]),[-1,127])
p12_new -> (-1,[-1,-1])
ep12 -> (Unknown int([0,1]),[0,1])
p13 -> (0,[0,0])
p13_old -> (Unknown int([-7,7]),[-1,127])
p13_new -> (-1,[-1,-1])
ep13 -> (Unknown int([0,1]),[0,1])
p14 -> (0,[0,0])
p14_old -> (Unknown int([-7,7]),[-1,127])
p14_new -> (-1,[-1,-1])
ep14 -> (Unknown int([0,1]),[0,1])
p21 -> (0,[0,0])
p21_old -> (Unknown int([-7,7]),[-1,127])
p21_new -> (-1,[-1,-1])
ep21 -> (Unknown int([0,1]),[0,1])
p23 -> (0,[0,0])
p23_old -> (Unknown int([-7,7]),[-1,127])
p23_new -> (-1,[-1,-1])
ep23 -> (Unknown int([0,1]),[0,1])
p24 -> (0,[0,0])
p24_old -> (Unknown int([-7,7]),[-1,127])
p24_new -> (-1,[-1,-1])
ep24 -> (Unknown int([0,1]),[0,1])
p31 -> (0,[0,0])
p31_old -> (Unknown int([-7,7]),[-1,127])
p31_new -> (-1,[-1,-1])
ep31 -> (Unknown int([0,1]),[0,1])
p32 -> (0,[0,0])
p32_old -> (Unknown int([-7,7]),[-1,127])
p32_new -> (-1,[-1,-1])
ep32 -> (Unknown int([0,1]),[0,1])
p34 -> (0,[0,0])
p34_old -> (Unknown int([-7,7]),[-1,127])
p34_new -> (-1,[-1,-1])
ep34 -> (Unknown int([0,1]),[0,1])
p41 -> (0,[0,0])
p41_old -> (Unknown int([-7,7]),[-1,127])
p41_new -> (-1,[-1,-1])
ep41 -> (Unknown int([0,1]),[0,1])
p42 -> (0,[0,0])
p42_old -> (Unknown int([-7,7]),[-1,127])
p42_new -> (-1,[-1,-1])
ep42 -> (Unknown int([0,1]),[0,1])
p43 -> (0,[0,0])
p43_old -> (Unknown int([-7,7]),[-1,127])
p43_new -> (-1,[-1,-1])
ep43 -> (Unknown int([0,1]),[0,1])
id1 -> (Unknown int([-7,7]),[0,127])
r1 -> (Unknown int([0,8]),[0,255])
st1 -> (Unknown int([0,7]),[0,127])
nl1 -> (Unknown int([0,7]),[0,127])
m1 -> (Unknown int([-7,7]),[-128,127])
max1 -> (Unknown int([-7,7]),[0,127])
mode1 -> (Unknown int([0,7]),[0,1])
newmax1 -> (Unknown int([0,1]),[0,1])
id2 -> (Unknown int([-7,7]),[0,127])
r2 -> (Unknown int([0,8]),[0,255])
st2 -> (Unknown int([0,7]),[0,127])
nl2 -> (Unknown int([0,7]),[0,127])
m2 -> (Unknown int([-7,7]),[-128,127])
max2 -> (Unknown int([-7,7]),[0,127])
mode2 -> (Unknown int([0,7]),[0,1])
newmax2 -> (Unknown int([0,1]),[0,1])
id3 -> (Unknown int([-7,7]),[0,127])
r3 -> (Unknown int([0,8]),[0,255])
st3 -> (Unknown int([0,7]),[0,127])
nl3 -> (Unknown int([0,7]),[0,127])
m3 -> (Unknown int([-7,7]),[-128,127])
max3 -> (Unknown int([-7,7]),[0,127])
mode3 -> (Unknown int([0,7]),[0,1])
newmax3 -> (Unknown int([0,1]),[0,1])
id4 -> (Unknown int([-7,7]),[0,127])
r4 -> (Unknown int([0,8]),[0,255])
st4 -> (Unknown int([0,7]),[0,127])
nl4 -> (Unknown int([0,7]),[0,127])
m4 -> (Unknown int([-7,7]),[-128,127])
max4 -> (Unknown int([-7,7]),[0,127])
mode4 -> (Unknown int([0,7]),[0,1])
newmax4 -> (Unknown int([0,1]),[0,1])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (1,[1,1])
__return_3681 -> (Unknown int([0,7]),[0,1])
}
Local {
main__c1 -> (Unknown int([0,7]),[0,1])
main__i2 -> (0,[0,0])
init__r121 -> (Unknown int([0,1]),[0,1])
init__r131 -> (Unknown int([0,1]),[0,1])
init__r141 -> (Unknown int([0,1]),[0,1])
init__r211 -> (Unknown int([0,1]),[0,1])
init__r231 -> (Unknown int([0,1]),[0,1])
init__r241 -> (Unknown int([0,1]),[0,1])
init__r311 -> (Unknown int([0,1]),[0,1])
init__r321 -> (Unknown int([0,1]),[0,1])
init__r341 -> (Unknown int([0,1]),[0,1])
init__r411 -> (Unknown int([0,1]),[0,1])
init__r421 -> (Unknown int([0,1]),[0,1])
init__r431 -> (Unknown int([0,1]),[0,1])
init__r122 -> (Unknown int([0,1]),[0,1])
init__tmp -> (Unknown int([0,7]),[0,1])
init__r132 -> (Unknown int([0,1]),[0,1])
init__tmp___0 -> (Unknown int([0,7]),[0,1])
init__r142 -> (Unknown int([0,1]),[0,1])
init__tmp___1 -> (Unknown int([0,7]),[0,1])
init__r212 -> (Unknown int([0,1]),[0,1])
init__tmp___2 -> (Unknown int([0,7]),[0,1])
init__r232 -> (Unknown int([0,1]),[0,1])
init__tmp___3 -> (Unknown int([0,7]),[0,1])
init__r242 -> (Unknown int([0,1]),[0,1])
init__tmp___4 -> (Unknown int([0,7]),[0,1])
init__r312 -> (Unknown int([0,1]),[0,1])
init__tmp___5 -> (Unknown int([0,7]),[0,1])
init__r322 -> (Unknown int([0,1]),[0,1])
init__tmp___6 -> (Unknown int([0,7]),[0,1])
init__r342 -> (Unknown int([0,1]),[0,1])
init__tmp___7 -> (Unknown int([0,7]),[0,1])
init__r412 -> (Unknown int([0,1]),[0,1])
init__tmp___8 -> (Unknown int([0,7]),[0,1])
init__r422 -> (Unknown int([0,1]),[0,1])
init__tmp___9 -> (Unknown int([0,7]),[0,1])
init__r432 -> (Unknown int([0,1]),[0,1])
init__tmp___10 -> (Unknown int([0,7]),[0,1])
init__r123 -> (Not {0}([0,1]),[0,1])
init__tmp___11 -> (Unknown int([0,7]),[0,1])
init__r133 -> (Not {0}([0,1]),[0,1])
init__tmp___12 -> (Unknown int([0,7]),[0,1])
init__r143 -> (Not {0}([0,1]),[0,1])
init__tmp___13 -> (Unknown int([0,7]),[0,1])
init__r213 -> (Not {0}([0,1]),[0,1])
init__tmp___14 -> (Unknown int([0,7]),[0,1])
init__r233 -> (Not {0}([0,1]),[0,1])
init__tmp___15 -> (Unknown int([0,7]),[0,1])
init__r243 -> (Not {0}([0,1]),[0,1])
init__tmp___16 -> (Unknown int([0,7]),[0,1])
init__r313 -> (Not {0}([0,1]),[0,1])
init__tmp___17 -> (Unknown int([0,7]),[0,1])
init__r323 -> (Not {0}([0,1]),[0,1])
init__tmp___18 -> (Unknown int([0,7]),[0,1])
init__r343 -> (Not {0}([0,1]),[0,1])
init__tmp___19 -> (Unknown int([0,7]),[0,1])
init__r413 -> (Not {0}([0,1]),[0,1])
init__tmp___20 -> (Unknown int([0,7]),[0,1])
init__r423 -> (Not {0}([0,1]),[0,1])
init__tmp___21 -> (Unknown int([0,7]),[0,1])
init__r433 -> (Not {0}([0,1]),[0,1])
init__tmp___22 -> (Unknown int([0,7]),[0,1])
init__tmp___23 -> (1,[1,1])
node1__newmax -> (Unknown int([0,7]),[0,1])
node2__newmax -> (Unknown int([0,7]),[0,1])
node3__newmax -> (Unknown int([0,7]),[0,1])
node4__newmax -> (Unknown int([0,7]),[0,1])
check__tmp -> (Unknown int([0,7]),[0,1])
__tmp_1 -> (Unknown int([0,1]),[0,1])
assert__arg -> (Unknown int([0,1]),[0,1])
node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
}
Global {
main -> (Unknown int([0,1]),[0,1])
}
}, mapping {
}),
lifted proglines:Unknown line] -> {((node 500 "assert__arg = __tmp_1;", [Topped Set (variables):{},
lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{},
Unit:(),
Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{},
MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (0,[0,0])
p12_new -> (0,[0,0])
ep12 -> (0,[0,0])
p13 -> (0,[0,0])
p13_old -> (0,[0,0])
p13_new -> (0,[0,0])
ep13 -> (0,[0,0])
p14 -> (0,[0,0])
p14_old -> (0,[0,0])
p14_new -> (0,[0,0])
ep14 -> (0,[0,0])
p21 -> (0,[0,0])
p21_old -> (0,[0,0])
p21_new -> (0,[0,0])
ep21 -> (0,[0,0])
p23 -> (0,[0,0])
p23_old -> (0,[0,0])
p23_new -> (0,[0,0])
ep23 -> (0,[0,0])
p24 -> (0,[0,0])
p24_old -> (0,[0,0])
p24_new -> (0,[0,0])
ep24 -> (0,[0,0])
p31 -> (0,[0,0])
p31_old -> (0,[0,0])
p31_new -> (0,[0,0])
ep31 -> (0,[0,0])
p32 -> (0,[0,0])
p32_old -> (0,[0,0])
p32_new -> (0,[0,0])
ep32 -> (0,[0,0])
p34 -> (0,[0,0])
p34_old -> (0,[0,0])
p34_new -> (0,[0,0])
ep34 -> (0,[0,0])
p41 -> (0,[0,0])
p41_old -> (0,[0,0])
p41_new -> (0,[0,0])
ep41 -> (0,[0,0])
p42 -> (0,[0,0])
p42_old -> (0,[0,0])
p42_new -> (0,[0,0])
ep42 -> (0,[0,0])
p43 -> (0,[0,0])
p43_old -> (0,[0,0])
p43_new -> (0,[0,0])
ep43 -> (0,[0,0])
id1 -> (0,[0,0])
r1 -> (0,[0,0])
st1 -> (0,[0,0])
nl1 -> (0,[0,0])
m1 -> (0,[0,0])
max1 -> (0,[0,0])
mode1 -> (0,[0,0])
newmax1 -> (0,[0,0])
id2 -> (0,[0,0])
r2 -> (0,[0,0])
st2 -> (0,[0,0])
nl2 -> (0,[0,0])
m2 -> (0,[0,0])
max2 -> (0,[0,0])
mode2 -> (0,[0,0])
newmax2 -> (0,[0,0])
id3 -> (0,[0,0])
r3 -> (0,[0,0])
st3 -> (0,[0,0])
nl3 -> (0,[0,0])
m3 -> (0,[0,0])
max3 -> (0,[0,0])
mode3 -> (0,[0,0])
newmax3 -> (0,[0,0])
id4 -> (0,[0,0])
r4 -> (0,[0,0])
st4 -> (0,[0,0])
nl4 -> (0,[0,0])
m4 -> (0,[0,0])
max4 -> (0,[0,0])
mode4 -> (0,[0,0])
newmax4 -> (0,[0,0])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (0,[0,0])
__return_3681 -> (0,[0,0])
}
}, mapping {
}),
lifted proglines:Unknown line], [Topped Set (variables):{},
lifted regmap:mapping {
},
Reversed (Topped Set (Cil expressions)):{},
Topped Set (Set (Cil expressions)):{{__tmp_1, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
Unit:(),
Topped Set (variables):{},
Reversed (Topped Set (Normal Lvals * booleans)):{},
MT mode:Singlethreaded,
Thread:main,
value domain * array partitioning deps:(mapping {
Global {
__return_main -> (0,[0,0])
nomsg -> (-1,[-1,-1])
p12 -> (0,[0,0])
p12_old -> (Unknown int([-7,7]),[-1,127])
p12_new -> (-1,[-1,-1])
ep12 -> (Unknown int([0,1]),[0,1])
p13 -> (0,[0,0])
p13_old -> (Unknown int([-7,7]),[-1,127])
p13_new -> (-1,[-1,-1])
ep13 -> (Unknown int([0,1]),[0,1])
p14 -> (0,[0,0])
p14_old -> (Unknown int([-7,7]),[-1,127])
p14_new -> (-1,[-1,-1])
ep14 -> (Unknown int([0,1]),[0,1])
p21 -> (0,[0,0])
p21_old -> (Unknown int([-7,7]),[-1,127])
p21_new -> (-1,[-1,-1])
ep21 -> (Unknown int([0,1]),[0,1])
p23 -> (0,[0,0])
p23_old -> (Unknown int([-7,7]),[-1,127])
p23_new -> (-1,[-1,-1])
ep23 -> (Unknown int([0,1]),[0,1])
p24 -> (0,[0,0])
p24_old -> (Unknown int([-7,7]),[-1,127])
p24_new -> (-1,[-1,-1])
ep24 -> (Unknown int([0,1]),[0,1])
p31 -> (0,[0,0])
p31_old -> (Unknown int([-7,7]),[-1,127])
p31_new -> (-1,[-1,-1])
ep31 -> (Unknown int([0,1]),[0,1])
p32 -> (0,[0,0])
p32_old -> (Unknown int([-7,7]),[-1,127])
p32_new -> (-1,[-1,-1])
ep32 -> (Unknown int([0,1]),[0,1])
p34 -> (0,[0,0])
p34_old -> (Unknown int([-7,7]),[-1,127])
p34_new -> (-1,[-1,-1])
ep34 -> (Unknown int([0,1]),[0,1])
p41 -> (0,[0,0])
p41_old -> (Unknown int([-7,7]),[-1,127])
p41_new -> (-1,[-1,-1])
ep41 -> (Unknown int([0,1]),[0,1])
p42 -> (0,[0,0])
p42_old -> (Unknown int([-7,7]),[-1,127])
p42_new -> (-1,[-1,-1])
ep42 -> (Unknown int([0,1]),[0,1])
p43 -> (0,[0,0])
p43_old -> (Unknown int([-7,7]),[-1,127])
p43_new -> (-1,[-1,-1])
ep43 -> (Unknown int([0,1]),[0,1])
id1 -> (Unknown int([-7,7]),[0,127])
r1 -> (Unknown int([0,8]),[0,255])
st1 -> (Unknown int([0,7]),[0,127])
nl1 -> (Unknown int([0,7]),[0,127])
m1 -> (Unknown int([-7,7]),[-128,127])
max1 -> (Unknown int([-7,7]),[0,127])
mode1 -> (Unknown int([0,7]),[0,1])
newmax1 -> (Unknown int([0,1]),[0,1])
id2 -> (Unknown int([-7,7]),[0,127])
r2 -> (Unknown int([0,8]),[0,255])
st2 -> (Unknown int([0,7]),[0,127])
nl2 -> (Unknown int([0,7]),[0,127])
m2 -> (Unknown int([-7,7]),[-128,127])
max2 -> (Unknown int([-7,7]),[0,127])
mode2 -> (Unknown int([0,7]),[0,1])
newmax2 -> (Unknown int([0,1]),[0,1])
id3 -> (Unknown int([-7,7]),[0,127])
r3 -> (Unknown int([0,8]),[0,255])
st3 -> (Unknown int([0,7]),[0,127])
nl3 -> (Unknown int([0,7]),[0,127])
m3 -> (Unknown int([-7,7]),[-128,127])
max3 -> (Unknown int([-7,7]),[0,127])
mode3 -> (Unknown int([0,7]),[0,1])
newmax3 -> (Unknown int([0,1]),[0,1])
id4 -> (Unknown int([-7,7]),[0,127])
r4 -> (Unknown int([0,8]),[0,255])
st4 -> (Unknown int([0,7]),[0,127])
nl4 -> (Unknown int([0,7]),[0,127])
m4 -> (Unknown int([-7,7]),[-128,127])
max4 -> (Unknown int([-7,7]),[0,127])
mode4 -> (Unknown int([0,7]),[0,1])
newmax4 -> (Unknown int([0,1]),[0,1])
nodes ->
(Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
__return_3435 -> (1,[1,1])
__return_3681 -> (Unknown int([0,7]),[0,1])
}
Local {
main__c1 -> (Unknown int([0,7]),[0,1])
main__i2 -> (0,[0,0])
init__r121 -> (Unknown int([0,1]),[0,1])
init__r131 -> (Unknown int([0,1]),[0,1])
init__r141 -> (Unknown int([0,1]),[0,1])
init__r211 -> (Unknown int([0,1]),[0,1])
init__r231 -> (Unknown int([0,1]),[0,1])
init__r241 -> (Unknown int([0,1]),[0,1])
init__r311 -> (Unknown int([0,1]),[0,1])
init__r321 -> (Unknown int([0,1]),[0,1])
init__r341 -> (Unknown int([0,1]),[0,1])
init__r411 -> (Unknown int([0,1]),[0,1])
init__r421 -> (Unknown int([0,1]),[0,1])
init__r431 -> (Unknown int([0,1]),[0,1])
init__r122 -> (Unknown int([0,1]),[0,1])
init__tmp -> (Unknown int([0,7]),[0,1])
init__r132 -> (Unknown int([0,1]),[0,1])
init__tmp___0 -> (Unknown int([0,7]),[0,1])
init__r142 -> (Unknown int([0,1]),[0,1])
init__tmp___1 -> (Unknown int([0,7]),[0,1])
init__r212 -> (Unknown int([0,1]),[0,1])
init__tmp___2 -> (Unknown int([0,7]),[0,1])
init__r232 -> (Unknown int([0,1]),[0,1])
init__tmp___3 -> (Unknown int([0,7]),[0,1])
init__r242 -> (Unknown int([0,1]),[0,1])
init__tmp___4 -> (Unknown int([0,7]),[0,1])
init__r312 -> (Unknown int([0,1]),[0,1])
init__tmp___5 -> (Unknown int([0,7]),[0,1])
init__r322 -> (Unknown int([0,1]),[0,1])
init__tmp___6 -> (Unknown int([0,7]),[0,1])
init__r342 -> (Unknown int([0,1]),[0,1])
init__tmp___7 -> (Unknown int([0,7]),[0,1])
init__r412 -> (Unknown int([0,1]),[0,1])
init__tmp___8 -> (Unknown int([0,7]),[0,1])
init__r422 -> (Unknown int([0,1]),[0,1])
init__tmp___9 -> (Unknown int([0,7]),[0,1])
init__r432 -> (Unknown int([0,1]),[0,1])
init__tmp___10 -> (Unknown int([0,7]),[0,1])
init__r123 -> (Not {0}([0,1]),[0,1])
init__tmp___11 -> (Unknown int([0,7]),[0,1])
init__r133 -> (Not {0}([0,1]),[0,1])
init__tmp___12 -> (Unknown int([0,7]),[0,1])
init__r143 -> (Not {0}([0,1]),[0,1])
init__tmp___13 -> (Unknown int([0,7]),[0,1])
init__r213 -> (Not {0}([0,1]),[0,1])
init__tmp___14 -> (Unknown int([0,7]),[0,1])
init__r233 -> (Not {0}([0,1]),[0,1])
init__tmp___15 -> (Unknown int([0,7]),[0,1])
init__r243 -> (Not {0}([0,1]),[0,1])
init__tmp___16 -> (Unknown int([0,7]),[0,1])
init__r313 -> (Not {0}([0,1]),[0,1])
init__tmp___17 -> (Unknown int([0,7]),[0,1])
init__r323 -> (Not {0}([0,1]),[0,1])
init__tmp___18 -> (Unknown int([0,7]),[0,1])
init__r343 -> (Not {0}([0,1]),[0,1])
init__tmp___19 -> (Unknown int([0,7]),[0,1])
init__r413 -> (Not {0}([0,1]),[0,1])
init__tmp___20 -> (Unknown int([0,7]),[0,1])
init__r423 -> (Not {0}([0,1]),[0,1])
init__tmp___21 -> (Unknown int([0,7]),[0,1])
init__r433 -> (Not {0}([0,1]),[0,1])
init__tmp___22 -> (Unknown int([0,7]),[0,1])
init__tmp___23 -> (1,[1,1])
node1__newmax -> (Unknown int([0,7]),[0,1])
node2__newmax -> (Unknown int([0,7]),[0,1])
node3__newmax -> (Unknown int([0,7]),[0,1])
node4__newmax -> (Unknown int([0,7]),[0,1])
check__tmp -> (Unknown int([0,7]),[0,1])
__tmp_1 -> (Unknown int([0,1]),[0,1])
assert__arg -> (Unknown int([0,1]),[0,1])
node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
}
Global {
main -> (Unknown int([0,1]),[0,1])
}
}, mapping {
}),
lifted proglines:Unknown line]), Assign 'assert__arg = __tmp_1' )}
}, mapping {
})
Difference: Set (Set (Cil expressions)): These are fine!.
File '../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c':
function 'main' has dead code on lines: 912, 934, 956, 1077, 1099, 1121, 1242, 1264, 1286, 1407, 1429, 1451, 1479
Found dead code on 13 lines!
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:912)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:934)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:956)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1077)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1099)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1121)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1242)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1264)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1286)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1407)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1429)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1451)
Dead code: the else branch over expression 'main__i2 != 0' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1479)
SV-COMP result: ERROR (verify)
Writing xml to temp. file: /tmp/ocaml6cb765tmp
Timings:
TOTAL 36.244 s
parse 0.008 s
convert to CIL 0.008 s
analysis 36.229 s
global_inits 0.023 s
solving 16.905 s
S.Dom.equal 0.029 s
verify 4.179 s
reachability 3.793 s
witness 0.000 s
Timing used
Memory statistics: total=38432.33MB, max=58.97MB, minor=38429.26MB, major=180.19MB, promoted=177.12MB
minor collections=18337 major collections=27 compactions=0
Time needed: 7446 ms
I think the message with Difference: Set (Set (Cil expressions)): These are fine!. is due to some functor not modifying pretty_diff despite changing leq.
The difference is
Solver computed:
Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, assert__arg, main__c1}, ....
RHS:
Topped Set (Set (Cil expressions)):{{__tmp_1, assert__arg, main__c1}, ...
I can run the same command (with relative paths changed) and get a different result:
./goblint --conf conf/svcomp21.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --html ../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
File '../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c':
function 'main' has dead code on lines: 912, 934, 956, 1077, 1099, 1121, 1242, 1264, 1286, 1407, 1429, 1451, 1479
Found dead code on 13 lines!
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:912)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:934)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:956)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1077)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1099)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1121)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1242)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1264)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1286)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1407)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1429)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1451)
Dead code: the else branch over expression 'main__i2 != 0' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1479)
SV-COMP result: unknown
Writing xml to temp. file: /tmp/ocamla7250atmp
Timings:
TOTAL 22.186 s
parse 0.010 s
convert to CIL 0.016 s
analysis 22.160 s
global_inits 0.008 s
solving 11.073 s
S.Dom.equal 0.020 s
verify 2.065 s
reachability 1.967 s
witness 1.914 s
determine 0.003 s
write 1.910 s
Timing used
Memory statistics: total=40548.70MB, max=58.97MB, minor=40501.04MB, major=250.22MB, promoted=202.56MB
minor collections=19327 major collections=31 compactions=0
Time needed: 6604 ms
This is bizarre, I don't have any uncommited changes and have made a clean build.
Strange indeed, after going back to an older commit and another make clean, I can also no longer observe this problem when I build from scratch.
However, if I use the binary from the release, this problem still happens (I tried with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c).
Was the release maybe dirty?
I don't think it was because I always made the archive build on our Ubuntu 20.04 server where I didn't do any development and also did it after make clean. Also, if it was dirty, then the version number would say -dirty.
I will try that soon. It would be quite impossible to debug and fix it though if it somehow doesn't happen on new builds.
it might be a hint in itself as to where the issue is. Like maybe somewhere physical equality (==) is accidentally being used. Not sure what else could give such non-deterministic behavior.
I tried with the exact executable from the verifier archive (SHA-256 below) and I still gives the unknown answer:
simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ sha256sum ./asd/goblint/goblint
16574d3cacb6ab22b29fada00cdeecc14c74706cf6d90526e4068329616d3618 ./asd/goblint/goblint
simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ ./asd/goblint/goblint --conf conf/svcomp21.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
SV-COMP result: unknown
Timings:
TOTAL 13.621 s
parse 0.004 s
convert to CIL 0.004 s
analysis 13.614 s
global_inits 0.011 s
solving 9.102 s
S.Dom.equal 0.007 s
verify 1.838 s
reachability 1.729 s
witness 0.930 s
determine 0.002 s
write 0.928 s
Timing used
Memory statistics: total=25569.06MB, max=58.97MB, minor=25521.33MB, major=235.14MB, promoted=187.41MB
minor collections=12184 major collections=29 compactions=0
Can you try with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c, too?
I still get the error with that (same sha256 as you posted above).
mbs@mbs-VirtualBox:~/Desktop/goblint$ sha256sum goblint
16574d3cacb6ab22b29fada00cdeecc14c74706cf6d90526e4068329616d3618 goblint
Or maybe it is the GCC version or something?
mbs@mbs-VirtualBox:~/Desktop/goblint$ gcc -v
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/9/lto-wrapper
OFFLOAD_TARGET_NAMES=nvptx-none:hsa
OFFLOAD_TARGET_DEFAULT=1
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu 9.2.1-9ubuntu2' --with-bugurl=file:///usr/share/doc/gcc-9/README.Bugs --enable-languages=c,ada,c++,go,brig,d,fortran,objc,obj-c++,gm2 --prefix=/usr --with-gcc-major-version-only --program-suffix=-9 --program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --libdir=/usr/lib --enable-nls --enable-bootstrap --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new --enable-gnu-unique-object --disable-vtable-verify --enable-plugin --enable-default-pie --with-system-zlib --with-target-system-zlib=auto --enable-multiarch --disable-werror --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic --enable-offload-targets=nvptx-none,hsa --without-cuda-driver --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix
gcc version 9.2.1 20191008 (Ubuntu 9.2.1-9ubuntu2)
mbs@mbs-VirtualBox:~/Desktop/goblint$ ldd --version
ldd (Ubuntu GLIBC 2.30-0ubuntu2.2) 2.30
Copyright (C) 2019 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Written by Roland McGrath and Ulrich Drepper.
mbs@mbs-VirtualBox:~/Desktop/goblint$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description: Ubuntu 19.10
Release: 19.10
Codename: eoan
Hmm yeah, it does happen with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c on the archive build, so there is some consistency.
In the supposedly final results (linked in Slack) there's one more case: seq-mthreaded-reduced/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c. It didn't show in the preruns so something weird is even happening there without any change to the archive. And it's nowhere near the timeout.
For the first example at least, var_eq contains an additional equality between {0, main__i2} in what the solver computed, that is not there for the RHS, but he value domain still knows that main__i2 is [0,0].
After merging 0f9f068ee53e181405515191ad8b9ffe66800fc9/ pull #249 this also applies to c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
