2022-03-09 11:25:51
/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 justglob.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' 'justglob.c' '-o' '.goblint/preprocessed/justglob.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/justglob.i
Converting CABS->CIL
Pre-merging (0) .goblint/preprocessed/stdlib.i
Pre-merging (1) .goblint/preprocessed/pthread.i
Pre-merging (2) .goblint/preprocessed/justglob.i
Final merging phase (0): .goblint/preprocessed/stdlib.i
Final merging phase (1): .goblint/preprocessed/pthread.i
Final merging phase (2): .goblint/preprocessed/justglob.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|=4
|stable|=4
|infl|=4
|wpoint|=0
|side_dep|=1
|side_infl|=1
change_info = { unchanged = 441; changed = 0; added = 0; removed = 0 }
Removing data for changed and removed functions...
Destabilizing sides of changed functions, primary old nodes and removed functions ...
Destabilizing and restarting removed start var entry state of main on justglob.c:2:1-2:9
Restarting to bot entry state of main on justglob.c:2:1-2:9
Restarting to bot main
Data after clean-up:
|rho|=5
|stable|=2
|infl|=5
|wpoint|=0
|side_dep|=0
|side_infl|=0
Unstable solver start vars in 1. phase:
call of main on justglob.c:2:1-2:9
Data after solve completed:
|rho|=7
|stable|=5
|infl|=7
|wpoint|=0
|side_dep|=0
|side_infl|=0
Postsolving
Saving the solver result to increment/solver.marshalled
Data after postsolve:
|rho|=5
|stable|=5
|infl|=5
|wpoint|=0
|side_dep|=1
|side_infl|=1
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.038
vars: 3, evals: 2
max updates: 1 for var node 77 "return (0);" on justglob.c:2:9-2:9
|rho|=5
|called|=0
|stable|=5
|infl|=5
|wpoint|=0
|side_dep|=1
|side_infl|=1
Found 3 contexts for 1 functions. Top 5 functions:
3 contexts for entry state of main on justglob.c:2:1-2:9
Memory statistics: total=27.26MB, max=6.37MB, minor=24.70MB, major=6.16MB, promoted=3.59MB
minor collections=12 major collections=2 compactions=0
vars = 3 evals = 2 narrow_reuses = 0 aborts = 0
Timings:
TOTAL 0.011 s
parse 0.002 s
convert to CIL 0.005 s
compareCilFiles 0.002 s
analysis 0.004 s
global_inits 0.001 s
solving 0.001 s
S.Dom.equal 0.001 s
postsolver 0.001 s
warn_global 0.001 s
Timing used
Memory statistics: total=27.30MB, max=6.37MB, minor=24.73MB, major=6.16MB, promoted=3.59MB
minor collections=12 major collections=2 compactions=0
=== APPENDED BY BENCHMARKING SCRIPT ===
Analysis began: 2022-03-09 11:25:51 +0200
Analysis ended: 2022-03-09 11:25:51 +0200
Duration: 0.07 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 justglob.c --enable dbg.uncalled --enable allglobs --enable printstats 1>/home/simmo/dev/goblint/sv-comp/goblint-bench/bench_result/justglob.patch.FuelInf.txt 2>&1