Open vogler opened 3 years ago
The following programs in bench/single-thread don't terminate:
The programs in bench/coreutils all terminate.
~Configuration:~ ~./goblint -v single-thread/wget-1.12_comb.c --enable exp.solver.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable exp.widen-context --sets exp.privatization none~
./goblint -v single-thread/wget-1.12_comb.c --enable exp.solver.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable exp.widen-context --sets exp.privatization none
Configuration after renames: ./goblint -v single-thread/wget-1.12_comb.c --enable solvers.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable ana.context.widen --sets ana.base.privatization none
./goblint -v single-thread/wget-1.12_comb.c --enable solvers.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable ana.context.widen --sets ana.base.privatization none
With that configuration, all programs should terminate. The question is why they don't and how to debug it.
The following only terminate with --enable exp.widen-context and are therefore likely recursive:
--enable exp.widen-context
Still the case also with current Goblint.
@SchiJoha would maybe be interesting to find out if your strategies from the new PR can enforce termination here?
The following programs in bench/single-thread don't terminate:
The programs in bench/coreutils all terminate.
~Configuration:~ ~
./goblint -v single-thread/wget-1.12_comb.c --enable exp.solver.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable exp.widen-context --sets exp.privatization none
~Configuration after renames:
./goblint -v single-thread/wget-1.12_comb.c --enable solvers.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --enable ana.context.widen --sets ana.base.privatization none
With that configuration, all programs should terminate. The question is why they don't and how to debug it.
The following only terminate with
--enable exp.widen-context
and are therefore likely recursive: