diff --git a/regression/cbmc/self_loops_to_assumptions1/default.desc b/regression/cbmc/self_loops_to_assumptions1/default.desc index a7a038cf94d..5cec41df787 100644 --- a/regression/cbmc/self_loops_to_assumptions1/default.desc +++ b/regression/cbmc/self_loops_to_assumptions1/default.desc @@ -1,6 +1,8 @@ CORE main.c --unwind 1 --unwinding-assertions +^replacing self-loop at file main.c line 3 function main by assume\(FALSE\)$ +^no unwinding assertion will be generated for self-loop at file main.c line 3 function main$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc index 519dfddbd15..b75ec34a1bc 100644 --- a/regression/cbmc/self_loops_to_assumptions1/no-assume.desc +++ b/regression/cbmc/self_loops_to_assumptions1/no-assume.desc @@ -5,3 +5,4 @@ main.c ^SIGNAL=0$ ^VERIFICATION FAILED$ -- +^replacing self-loop diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index cf0e8431648..8d32b3ba1ac 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -9,11 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution -#include "goto_symex.h" -#include "goto_symex_is_constant.h" - -#include - #include #include #include @@ -22,11 +17,16 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include +#include "goto_symex.h" +#include "goto_symex_is_constant.h" #include "path_storage.h" +#include + void goto_symext::apply_goto_condition( goto_symex_statet ¤t_state, goto_statet &jump_taken_state, @@ -279,10 +279,19 @@ void goto_symext::symex_goto(statet &state) { // generate assume(false) or a suitable negation if this // instruction is a conditional goto - if(new_guard.is_true()) - symex_assume_l2(state, false_exprt()); - else - symex_assume_l2(state, not_exprt(new_guard)); + exprt negated_guard = not_exprt{new_guard}; + do_simplify(negated_guard); + log.statistics() << "replacing self-loop at " + << state.source.pc->source_location() << " by assume(" + << from_expr(ns, state.source.function_id, negated_guard) + << ")" << messaget::eom; + if(symex_config.unwinding_assertions) + { + log.warning() + << "no unwinding assertion will be generated for self-loop at " + << state.source.pc->source_location() << messaget::eom; + } + symex_assume_l2(state, negated_guard); // next instruction symex_transition(state);