2022-03-09 11:25:49 /home/simmo/dev/goblint/sv-comp/analyzer/goblint --conf /home/simmo/dev/goblint/sv-comp/goblint-bench/index/conf/td3.json -v --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs original increment justglob.c Custom include dirs: 1. /home/simmo/dev/goblint/sv-comp/goblint/includes (exists=true) Preprocessing files. Preprocessor cpp: is_bad=false 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/stdlib.c' '-o' '.goblint/preprocessed/stdlib.i' 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/pthread.c' '-o' '.goblint/preprocessed/pthread.i' 'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' 'justglob.c' '-o' '.goblint/preprocessed/justglob.i' Parsing files. Frontc is parsing .goblint/preprocessed/stdlib.i Converting CABS->CIL Frontc is parsing .goblint/preprocessed/pthread.i Converting CABS->CIL Frontc is parsing .goblint/preprocessed/justglob.i Converting CABS->CIL Pre-merging (0) .goblint/preprocessed/stdlib.i Pre-merging (1) .goblint/preprocessed/pthread.i Pre-merging (2) .goblint/preprocessed/justglob.i Final merging phase (0): .goblint/preprocessed/stdlib.i Final merging phase (1): .goblint/preprocessed/pthread.i Final merging phase (2): .goblint/preprocessed/justglob.i Constructors: Adding constructors to: main And now... the Goblin! Startfuns: [main] Exitfuns: [] Otherfuns: [] Using new format for phases! Activated analyses for phase 0: expRelation, base, threadid, threadflag, threadreturn, escape, mutex, access, mallocWrapper Activated transformations for phase 0: Generating the control flow graph. Initializing 1 globals. Executing 2 assigns. Unmarshalling original/solver.marshalled... If type of content changed, this will result in a segmentation fault! Unmarshalling increment/solver.marshalled... If type of content changed, this will result in a segmentation fault! Comparing precision of original (left) with increment (right) as EqConstrSys: call of main on justglob.c:2:1-2:9: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } Temp { RETURN -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } Temp { RETURN -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot main: original more precise than increment original: {[Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (4,[4,4]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()]} more precise than increment: {[Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (4,[4,4]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], [Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()]} reverse diff: Set (HConsed [expRelation:(Unit), mallocWrapper:(lifted node), base:(value domain * array partitioning deps * Vars with Weak Update * P), threadid:(Thread * lifted created and Unit), threadflag:(MT mode), threadreturn:(booleans), escape:(top or Set (variables)), access:(Unit), mutex:(Reversed (top or Set (Normal Lvals * booleans)))]): {[Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (4,[4,4]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], [Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()]} not leq {[Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (4,[4,4]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()]} because [Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()] node 77 "return (0);" on justglob.c:2:9-2:9: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot entry state of main on justglob.c:2:1-2:9: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Singlethreaded, Thread * lifted created and Unit:([main], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { __tzname -> (Array: {}, (2,[2,2])) __daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) __timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) tzname -> (Array: {}, (2,[2,2])) daylight -> (Unknown int([-31,31]),[-2147483648,2147483647]) timezone -> (Unknown int([-63,63]),[-9223372036854775808,9223372036854775807]) max_domains -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot Comparison summary: original more precise than increment (more precise: 4, less precise: 0, total: 7) vars = 0 evals = 0 narrow_reuses = 0 aborts = 0 Timings: TOTAL 0.010 s parse 0.004 s convert to CIL 0.003 s analysis 0.004 s global_inits 0.001 s warn_global 0.001 s Timing used Memory statistics: total=21.93MB, max=5.76MB, minor=20.14MB, major=5.65MB, promoted=3.86MB minor collections=10 major collections=1 compactions=0