Merge pull request #6624 from tautschnig/features/self-loop-status-output

goto-symex: print status note and conditional warning for self-loops

Author: tautschnig

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$

regression/cbmc/self_loops_to_assumptions1/no-assume.desc

@@ -5,3 +5,4 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
+^replacing self-loop

src/goto-symex/symex_goto.cpp

@@ -9,11 +9,6 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
-#include "goto_symex.h"
-#include "goto_symex_is_constant.h"
-
-#include <algorithm>
-
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -22,11 +17,16 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include <langapi/language_util.h>
 #include <pointer-analysis/add_failed_symbols.h>
 #include <pointer-analysis/value_set_dereference.h>
 
+#include "goto_symex.h"
+#include "goto_symex_is_constant.h"
 #include "path_storage.h"
 
+#include <algorithm>
+
 void goto_symext::apply_goto_condition(
   goto_symex_statet &current_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);