2022-03-09 11:25:47 /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 local-wp-read.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' 'local-wp-read.c' '-o' '.goblint/preprocessed/local-wp-read.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/local-wp-read.i Converting CABS->CIL Pre-merging (0) .goblint/preprocessed/stdlib.i Pre-merging (1) .goblint/preprocessed/pthread.i Pre-merging (2) .goblint/preprocessed/local-wp-read.i Final merging phase (0): .goblint/preprocessed/stdlib.i Final merging phase (1): .goblint/preprocessed/pthread.i Final merging phase (2): .goblint/preprocessed/local-wp-read.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: node 88 "assert(x == 1);" on local-wp-read.c:19:9-19:23: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (1,[1,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (Unknown int([0,7]),[0,1]) } }, 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:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (Unknown int([0,7]),[0,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (1,[1,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: x = (Unknown int([0,7]),[0,1]) instead of (1,[1,1]). either either unprotected or protected or FlagConfiguredTID: prefix * set:g: original more precise than increment original: lifted compound and compound:(1,[1,1]) more precise than increment: lifted compound and compound:(Unknown int([0,7]),[0,1]) reverse diff: (Unknown int([0,7]),[0,1]) instead of (1,[1,1]) node 87 "g = x;" on local-wp-read.c:18:9-18:14: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (1,[1,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (Unknown int([0,7]),[0,1]) } }, 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:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (Unknown int([0,7]),[0,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (main), Thread * lifted created and Unit:([main], {t_fun}), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { id -> {[main, t_fun]} x -> (1,[1,1]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: x = (Unknown int([0,7]),[0,1]) instead of (1,[1,1]). Comparison summary: original more precise than increment (more precise: 3, less precise: 0, total: 31) [Warning][Unknown] Calculated state for undefined function: unexpected node Statement return ((void *)0); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement return (0); Summary for all memory locations: safe: 1 vulnerable: 0 unsafe: 0 ------------------- total: 1 vars = 0 evals = 0 narrow_reuses = 0 aborts = 0 Timings: TOTAL 0.020 s parse 0.008 s convert to CIL 0.005 s analysis 0.008 s global_inits 0.001 s warn_global 0.001 s access 0.001 s Timing used Memory statistics: total=29.45MB, max=7.32MB, minor=27.52MB, major=6.75MB, promoted=4.82MB minor collections=14 major collections=2 compactions=0