2022-03-09 11:25:44 /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.save --set save_run original local-wp-read.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' '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. Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1. Unstable solver start vars in 1. phase: call of main on local-wp-read.c:11:1-24:1 Data after solve completed: |rho|=32 |stable|=32 |infl|=32 |wpoint|=0 |side_dep|=0 |side_infl|=0 Postsolving Saving the solver result to original/solver.marshalled Data after postsolve: |rho|=32 |stable|=32 |infl|=32 |wpoint|=0 |side_dep|=21 |side_infl|=7 Saving the current configuration to original/config.json, meta-data about this run to original/meta.json, and solver statistics to original/solver_stats.csv runtime: 00:00:00.064 vars: 32, evals: 14 max updates: 2 for var node 88 "assert(x == 1);" on local-wp-read.c:19:9-19:23 |rho|=32 |called|=0 |stable|=32 |infl|=32 |wpoint|=0 |side_dep|=21 |side_infl|=7 Found 4 contexts for 2 functions. Top 5 functions: 2 contexts for entry state of t_fun on local-wp-read.c:6:1-9:1 2 contexts for entry state of main on local-wp-read.c:11:1-24:1 Memory statistics: total=32.39MB, max=7.32MB, minor=30.39MB, major=6.70MB, promoted=4.71MB minor collections=15 major collections=2 compactions=0 [Warning][Race] Memory location g@local-wp-read.c:4:5-4:7 (race with conf. 110): read with thread:[main] (conf. 110) (local-wp-read.c:16:5-16:10) read with thread:[main] (conf. 110) (local-wp-read.c:20:9-20:14) write with thread:[main, t_fun] (conf. 110) (local-wp-read.c:7:5-7:10) write with thread:[main] (conf. 110) (local-wp-read.c:18:9-18:14) Summary for all memory locations: safe: 0 vulnerable: 0 unsafe: 1 ------------------- total: 1 vars = 32 evals = 14 narrow_reuses = 1 aborts = 0 Timings: TOTAL 0.035 s parse 0.016 s convert to CIL 0.010 s analysis 0.011 s global_inits 0.001 s solving 0.001 s S.Dom.equal 0.001 s postsolver 0.000 s warn_global 0.001 s access 0.001 s Timing used Memory statistics: total=32.58MB, max=7.32MB, minor=30.59MB, major=6.70MB, promoted=4.71MB minor collections=15 major collections=2 compactions=0 === APPENDED BY BENCHMARKING SCRIPT === Analysis began: 2022-03-09 11:25:44 +0200 Analysis ended: 2022-03-09 11:25:44 +0200 Duration: 0.10 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.save --set save_run original local-wp-read.c --enable dbg.uncalled --enable allglobs --enable printstats 1>/home/simmo/dev/goblint/sv-comp/goblint-bench/bench_result/local-wp-read.FromScratch.txt 2>&1