2022-03-09 11:25:35 /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 example.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' 'example.c' '-o' '.goblint/preprocessed/example.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/example.i Converting CABS->CIL Pre-merging (0) .goblint/preprocessed/stdlib.i Pre-merging (1) .goblint/preprocessed/pthread.i Pre-merging (2) .goblint/preprocessed/example.i Final merging phase (0): .goblint/preprocessed/stdlib.i Final merging phase (1): .goblint/preprocessed/pthread.i Final merging phase (2): .goblint/preprocessed/example.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 2 globals. Executing 11 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 108 "return (1);" on example.c:13:5-13:13: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: bot diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot either either unprotected or protected or FlagConfiguredTID: prefix * set:fp: original more precise than increment original: lifted compound and compound:{&good, NULL} more precise than increment: lifted compound and compound:{&bad, &good, NULL} reverse diff: HoarePO: {bad, good, NULL} not leq {good, NULL} node 88 "res = 0;" on example.c:24:5-24:12: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([-7,7]),[0,1]) } Parameter { arg -> (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:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([-7,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: res = (Unknown int([-7,7]),[0,1]) instead of (Unknown int([0,7]),[0,1]). varinfo:bad: original more precise than increment original: bot more precise than increment: readwrite * write:({mutex}, All mutexes) reverse diff: readwrite * write:({mutex}, All mutexes) instead of bot node 86 "pthread_mutex_unlock(& mutex);" on example.c:22:5-22:33: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good, NULL} } Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good, NULL} } Local { res -> (Unknown int([-7,7]),[-1,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: ([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good, NULL} } Local { res -> (Unknown int([-7,7]),[-1,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good, NULL} } Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { }) because Map: fp = HoarePO: {bad, good, NULL} not leq {good, NULL} Map: res = (Unknown int([-7,7]),[-1,1]) instead of (Unknown int([0,7]),[0,1]). entry state of good on example.c:12:1-14:1: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot call of good on example.c:12:1-14:1: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Temp { RETURN -> (1,[1,1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Temp { RETURN -> (1,[1,1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot node 109 "return (-1);" on example.c:9:5-9:14: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot entry state of good on example.c:12:1-14:1: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: bot diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot call of good on example.c:12:1-14:1: original less precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } Temp { RETURN -> (1,[1,1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} less precise than increment: bot diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } Temp { RETURN -> (1,[1,1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot node 87 "assert(res >= 0);" on example.c:23:5-23:21: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([-7,7]),[-1,1]) } Parameter { arg -> (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:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([-7,7]),[-1,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Local { res -> (Unknown int([0,7]),[0,1]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {}), lifted node:Unknown node, Unit:()], mapping { }) because Map: res = (Unknown int([-7,7]),[-1,1]) instead of (Unknown int([0,7]),[0,1]). entry state of bad on example.c:8:1-10:1: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot node 84 "res = (*fp)();" on example.c:20:9-20:19: original more precise than increment original: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } Local { res -> (0,[0,0]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Local { res -> (0,[0,0]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: ([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Local { res -> (0,[0,0]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { }): not leq ([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:True, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } Local { res -> (0,[0,0]) } Parameter { arg -> (0,[0,0]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { }) because Map: fp = HoarePO: {bad, good} not leq {good}. either varinfo * std option * std or varinfo:((fp, ), (int (*)())): original more precise than increment original: lifted Set (std) and Set (varinfo * std option * std):{110, false, example.c:19:5-21:5, & fp, [lock:{mutex}, thread:[main, consumer]], 110, false, example.c:20:9-20:19, & fp, [lock:{mutex}, thread:[main, consumer]], 110, true, example.c:32:5-32:14, & fp, [lock:{mutex}, thread:[main, producer]]} more precise than increment: lifted Set (std) and Set (varinfo * std option * std):{110, false, example.c:19:5-21:5, & fp, [lock:{mutex}, thread:[main, consumer]], 110, false, example.c:20:9-20:19, & fp, [lock:{mutex}, thread:[main, consumer]], 110, true, example.c:32:5-32:13, & fp, [lock:{mutex}, thread:[main, producer]], 110, true, example.c:32:5-32:14, & fp, [lock:{mutex}, thread:[main, producer]]} reverse diff: Set (std): {110, false, example.c:19:5-21:5, & fp, [lock:{mutex}, thread:[main, consumer]], 110, false, example.c:20:9-20:19, & fp, [lock:{mutex}, thread:[main, consumer]], 110, true, example.c:32:5-32:13, & fp, [lock:{mutex}, thread:[main, producer]], 110, true, example.c:32:5-32:14, & fp, [lock:{mutex}, thread:[main, producer]]} not leq {110, false, example.c:19:5-21:5, & fp, [lock:{mutex}, thread:[main, consumer]], 110, false, example.c:20:9-20:19, & fp, [lock:{mutex}, thread:[main, consumer]], 110, true, example.c:32:5-32:14, & fp, [lock:{mutex}, thread:[main, producer]]} because 110, true, example.c:32:5-32:13, & fp, [lock:{mutex}, thread:[main, producer]] bad: original more precise than increment original: bot more precise than increment: {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], [Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} reverse diff: {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], [Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} instead of bot node 108 "return (1);" on example.c:13:5-13:13: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot either either unprotected or protected or FlagConfiguredTID: prefix * set:fp: original more precise than increment original: lifted compound and compound:{&good, NULL} more precise than increment: lifted compound and compound:{&bad, &good, NULL} reverse diff: HoarePO: {bad, good, NULL} not leq {good, NULL} good: original incomparable to increment original: {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} incomparable to increment: {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} 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)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} not leq {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} because [Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), 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)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} not leq {[Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()]} because [Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()] entry state of bad on example.c:8:1-10:1: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot call of bad on example.c:8:1-10:1: original more precise than increment original: bot more precise than increment: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Temp { RETURN -> (-1,[-1,-1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} reverse diff: {([Reversed (top or Set (Normal Lvals * booleans)):{mutex}, Unit:(), top or Set (variables):{}, booleans:False, MT mode:Multithreaded (other), Thread * lifted created and Unit:([main, consumer], bot), value domain * array partitioning deps * Vars with Weak Update * P:(mapping { Global { fp -> {&bad, &good} } Temp { RETURN -> (-1,[-1,-1]) } }, mapping { }, {}, {fp}), lifted node:Unknown node, Unit:()], mapping { })} instead of bot Comparison summary: original incomparable to increment (more precise: 17, less precise: 4, total: 64) [Warning][Deadcode] Function "bad" will never be called: 1LoC (example.c:8:1-10:1) [Warning][Unknown] Calculated state for undefined function: unexpected node Statement fp = (int (*)())(& good); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement pthread_mutex_unlock(& mutex); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement return (1); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement return ((void *)0); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement pthread_mutex_lock(& mutex); [Warning][Unknown] Calculated state for undefined function: unexpected node Statement res = 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.025 s parse 0.009 s convert to CIL 0.006 s analysis 0.012 s global_inits 0.005 s warn_global 0.001 s access 0.001 s Timing used Memory statistics: total=34.72MB, max=7.32MB, minor=32.67MB, major=7.44MB, promoted=5.38MB minor collections=17 major collections=3 compactions=0