2022-03-09 11:25:40
/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 8 --enable incremental.load --set save_run increment restart.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' 'restart.c' '-o' '.goblint/preprocessed/restart.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/restart.i
Converting CABS->CIL
Pre-merging (0) .goblint/preprocessed/stdlib.i
Pre-merging (1) .goblint/preprocessed/pthread.i
Pre-merging (2) .goblint/preprocessed/restart.i
Final merging phase (0): .goblint/preprocessed/stdlib.i
Final merging phase (1): .goblint/preprocessed/pthread.i
Final merging phase (2): .goblint/preprocessed/restart.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 1 globals.
Executing 2 assigns.
Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1.
Loaded data for incremental analysis:
|rho|=47
|stable|=46
|infl|=47
|wpoint|=0
|side_dep|=25
|side_infl|=10
change_info = { unchanged = 443; changed = 1; added = 0; removed = 0 }
Completely changed function: t_fun2
Destabilizing changed functions and primary old nodes ...
Restarting to bot entry state of t_fun2 on restart.c:12:1-15:1
Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:[main, t_fun2]
Restarting to bot varinfo:g
Restarting to bot either varinfo * std option * std or varinfo:((g, ), (int ))
Restarting to bot either varinfo * std option * std or varinfo:g
Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:g
Restarting to bot entry state of t_fun1 on restart.c:6:1-10:1
Restarting to bot t_fun1
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:__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:g
Restarting to bot either either unprotected or protected or FlagConfiguredTID: prefix * set:[main, t_fun1]
Restarting to bot t_fun2
Restarting to bot varinfo:t_fun2
Removing data for changed and removed functions...
Destabilizing sides of changed functions, primary old nodes and removed functions ...
Data after clean-up:
|rho|=47
|stable|=3
|infl|=47
|wpoint|=0
|side_dep|=1
|side_infl|=1
Unstable solver start vars in 1. phase:
call of main on restart.c:17:1-34:1
Data after solve completed:
|rho|=48
|stable|=45
|infl|=48
|wpoint|=0
|side_dep|=0
|side_infl|=0
Postsolving
Saving the solver result to increment/solver.marshalled
Data after postsolve:
|rho|=46
|stable|=45
|infl|=46
|wpoint|=0
|side_dep|=24
|side_infl|=8
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.057
vars: 1, evals: 27
max updates: 2 for var node 80 "return ((void *)0);" on restart.c:9:5-9:15
|rho|=46
|called|=0
|stable|=45
|infl|=46
|wpoint|=0
|side_dep|=24
|side_infl|=8
Found 6 contexts for 3 functions. Top 5 functions:
2 contexts for entry state of t_fun1 on restart.c:6:1-10:1
2 contexts for entry state of main on restart.c:17:1-34:1
2 contexts for entry state of t_fun2 on restart.c:12:1-14:1
Memory statistics: total=45.77MB, max=7.97MB, minor=42.99MB, major=7.59MB, promoted=4.81MB
minor collections=21 major collections=3 compactions=0
[Warning][Race] Memory location g@restart.c:4:5-4:6 (race with conf. 110):
read with thread:[main, t_fun1] (conf. 110) (restart.c:7:5-7:14)
write with thread:[main] (conf. 110) (restart.c:26:13-26:18)
Summary for all memory locations:
safe: 0
vulnerable: 0
unsafe: 1
-------------------
total: 1
vars = 1 evals = 27 narrow_reuses = 2 aborts = 0
Timings:
TOTAL 0.035 s
parse 0.005 s
convert to CIL 0.009 s
compareCilFiles 0.007 s
analysis 0.016 s
global_inits 0.002 s
solving 0.012 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=45.94MB, max=7.97MB, minor=43.16MB, major=7.60MB, promoted=4.82MB
minor collections=22 major collections=3 compactions=0
=== APPENDED BY BENCHMARKING SCRIPT ===
Analysis began: 2022-03-09 11:25:40 +0200
Analysis ended: 2022-03-09 11:25:40 +0200
Duration: 0.08 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 8 --enable incremental.load --set save_run increment restart.c --enable dbg.uncalled --enable allglobs --enable printstats 1>/home/simmo/dev/goblint/sv-comp/goblint-bench/bench_result/restart.patch.Fuel8.txt 2>&1