2022-03-09 11:25:36 /home/simmo/dev/goblint/sv-comp/analyzer/goblint --conf /home/simmo/dev/goblint/sv-comp/goblint-bench/index/conf/td3.json -v --set dbg.timeout 60 --enable incremental.restart.sided.enabled --set incremental.restart.sided.fuel 1 --enable incremental.load --set save_run increment example.c --enable dbg.uncalled --enable allglobs --enable printstats 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 Unmarshalling /home/simmo/dev/goblint/sv-comp/goblint-bench/synthetic/incremental/incremental_data/results/ast.data... If type of content changed, this will result in a segmentation fault! Unmarshalling /home/simmo/dev/goblint/sv-comp/goblint-bench/synthetic/incremental/incremental_data/results/version.data... If type of content changed, this will result in a segmentation fault! Unmarshalling /home/simmo/dev/goblint/sv-comp/goblint-bench/synthetic/incremental/incremental_data/results/solver.data... If type of content changed, this will result in a segmentation fault! 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. Unmarshalling /home/simmo/dev/goblint/sv-comp/goblint-bench/synthetic/incremental/incremental_data/results/analysis.data... If type of content changed, this will result in a segmentation fault! Initializing 2 globals. Executing 11 assigns. Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1. Loaded data for incremental analysis: |rho|=55 |stable|=54 |infl|=55 |wpoint|=0 |side_dep|=30 |side_infl|=13 change_info = { unchanged = 444; changed = 3; added = 0; removed = 0 } Completely changed function: producer Completely changed function: good Completely changed function: bad Destabilizing changed functions and primary old nodes ... Restarting to bot entry state of producer on example.c:29:1-35:1 Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:[main, producer] Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:fp Restarting to bot entry state of consumer on example.c:16:1-27:1 Restarting to bot varinfo:fp Restarting to bot entry state of bad on example.c:8:1-10:1 Restarting to bot bad Restarting to bot either varinfo * std option * std or varinfo:((fp, ), (int (*)())) Restarting to bot either varinfo * std option * std or varinfo:fp Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:fp Restarting to bot varinfo:bad Restarting to bot consumer Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__tzname Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__daylight Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__timezone Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:tzname Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:daylight Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:timezone Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:mutex Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__tzname Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__daylight Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:__timezone Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:tzname Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:daylight Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:timezone Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:mutex Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:[main, consumer] Restarting to bot producer Restarting to bot varinfo:producer Removing data for changed and removed functions... Destabilizing sides of changed functions, primary old nodes and removed functions ... Data after clean-up: |rho|=55 |stable|=5 |infl|=55 |wpoint|=0 |side_dep|=1 |side_infl|=1 Unstable solver start vars in 1. phase: call of main on example.c:37:1-42:1 Data after solve completed: |rho|=65 |stable|=54 |infl|=65 |wpoint|=0 |side_dep|=0 |side_infl|=0 Postsolving Saving the solver result to increment/solver.marshalled Data after postsolve: |rho|=55 |stable|=54 |infl|=55 |wpoint|=0 |side_dep|=29 |side_infl|=12 Saving the current configuration to increment/config.json, meta-data about this run to increment/meta.json, and solver statistics to increment/solver_stats.csv runtime: 00:00:00.090 vars: 10, evals: 32 max updates: 2 for var node 86 "pthread_mutex_unlock(& mutex);" on example.c:22:5-22:33 |rho|=55 |called|=0 |stable|=54 |infl|=55 |wpoint|=0 |side_dep|=29 |side_infl|=12 Found 8 contexts for 4 functions. Top 5 functions: 2 contexts for entry state of consumer on example.c:16:1-27:1 2 contexts for entry state of producer on example.c:29:1-35:1 2 contexts for entry state of good on example.c:12:1-14:1 2 contexts for entry state of main on example.c:37:1-42:1 Memory statistics: total=48.95MB, max=7.97MB, minor=46.14MB, major=7.71MB, promoted=4.90MB minor collections=24 major collections=4 compactions=0 [Warning][Deadcode] Function "bad" will never be called: 1LoC (example.c:8:1-10:1) [Success][Race] Memory location fp@example.c:6:5-6:13 (safe): read with [lock:{mutex}, thread:[main, consumer]] (conf. 110) (example.c:19:5-21:5) read with [lock:{mutex}, thread:[main, consumer]] (conf. 110) (example.c:20:9-20:19) write with [lock:{mutex}, thread:[main, producer]] (conf. 110) (example.c:32:5-32:14) Summary for all memory locations: safe: 1 vulnerable: 0 unsafe: 0 ------------------- total: 1 vars = 10 evals = 32 narrow_reuses = 0 aborts = 0 Timings: TOTAL 0.053 s parse 0.013 s convert to CIL 0.015 s compareCilFiles 0.009 s analysis 0.017 s global_inits 0.001 s solving 0.016 s S.Dom.equal 0.001 s postsolver 0.003 s warn_global 0.001 s access 0.001 s Timing used Memory statistics: total=49.17MB, max=7.97MB, minor=46.36MB, major=7.71MB, promoted=4.90MB minor collections=24 major collections=4 compactions=0 === APPENDED BY BENCHMARKING SCRIPT === Analysis began: 2022-03-09 11:25:36 +0200 Analysis ended: 2022-03-09 11:25:36 +0200 Duration: 0.12 s Goblint params: /home/simmo/dev/goblint/sv-comp/analyzer/goblint --conf /home/simmo/dev/goblint/sv-comp/goblint-bench/index/conf/td3.json -v --set dbg.timeout 60 --enable incremental.restart.sided.enabled --set incremental.restart.sided.fuel 1 --enable incremental.load --set save_run increment example.c --enable dbg.uncalled --enable allglobs --enable printstats 1>/home/simmo/dev/goblint/sv-comp/goblint-bench/bench_result/example.patch.Fuel1.txt 2>&1