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

Unless CBMC is invoked with --no-self-loops-to-assumptions, self-loops
are replaced by assumptions. This commit now introduces a status output
that such replacement is happening, and also a warning when
--unwinding-assertions is set: as the loop is replaced by an assumption,
no unwinding assertions can possible be generated. This behaviour may be
unexpected by the user, and we should therefore let them know what is
going on.

Fixes: #6433

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

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
+#include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -279,10 +280,18 @@ 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("
+                       << format(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);