Add option not to transform self-loops into assumes

This allow disabling an optimisation in goto-symex
which is not compatible with termination checking.

Author: peterschrammel

src/cbmc/bmc.h

@@ -90,6 +90,8 @@ class bmct:public safety_checkert
     symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
       !options.get_option("symex-coverage-report").empty();
+    symex.self_loops_to_assumptions=
+      options.get_bool_option("self-loops-to-assumptions");
   }
 
   virtual resultt run(const goto_functionst &goto_functions)

src/cbmc/cbmc_parse_options.cpp

@@ -187,6 +187,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("propagation", true);
 
+  // transform self loops to assumptions
+  if(cmdline.isset("no-self-loops-to-assumptions"))
+    options.set_option("self-loops-to-assumptions", false);
+  else
+    options.set_option("self-loops-to-assumptions", true);
+
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

src/cbmc/cbmc_parse_options.h

@@ -71,6 +71,8 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
+  "(graphml-witness):" \
+  "(no-self-loops-to-assumptions)" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)

src/goto-symex/goto_symex.h

@@ -74,6 +74,7 @@ class goto_symext
     : total_vccs(0),
       remaining_vccs(0),
       constant_propagation(true),
+      self_loops_to_assumptions(true),
       language_mode(),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
@@ -210,6 +211,7 @@ class goto_symext
   unsigned total_vccs, remaining_vccs;
 
   bool constant_propagation;
+  bool self_loops_to_assumptions;
 
   optionst options;
 

src/goto-symex/symex_goto.cpp

@@ -58,9 +58,10 @@ void goto_symext::symex_goto(statet &state)
   if(!forward) // backwards?
   {
     // is it label: goto label; or while(cond); - popular in SV-COMP
-    if(goto_target==state.source.pc ||
-       (instruction.incoming_edges.size()==1 &&
-        *instruction.incoming_edges.begin()==goto_target))
+    if(self_loops_to_assumptions &&
+       (goto_target==state.source.pc ||
+        (instruction.incoming_edges.size()==1 &&
+         *instruction.incoming_edges.begin()==goto_target)))
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto