Merge remote-tracking branch 'origin/test_gen' into test_gen_mocks

Author: smowton

src/cbmc/cbmc_parse_options.cpp

@@ -465,6 +465,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover-function-only"))
     options.set_option("cover-function-only", true);
 
+  if(cmdline.isset("assertions-as-assumptions"))
+    options.set_option("assertions-as-assumptions", true);
+
   if(cmdline.isset("java-disable-mocks"))
     options.set_option("java-disable-mocks", true);
 }
@@ -952,6 +955,20 @@ bool cbmc_parse_optionst::process_goto_program(
         get_message_handler(), goto_functions);
     }
 
+    if(cmdline.isset("assertions-as-assumptions"))
+    {
+      // turn assertions (from generic checks) into assumptions
+      Forall_goto_functions(f_it, goto_functions)
+      {
+        goto_programt &body=f_it->second.body;
+        Forall_goto_program_instructions(i_it, body)
+        {
+          if(i_it->is_assert())
+  	    i_it->type= goto_program_instruction_typet::ASSUME;
+	}
+      }
+    }
+
     // add failed symbols
     // needs to be done before pointer analysis
     add_failed_symbols(symbol_table);
@@ -1166,7 +1183,8 @@ void cbmc_parse_optionst::help()
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
     " --gen-java-test-case         generate test case\n" 
-    " --cover-function-only        add coverage instrumentation only to the entry function" 
+    " --cover-function-only        add coverage instrumentation only to the entry function"
+    " --assertions-as-assumptions  convert assertions from generic checks into assumptions"
     "\n"
     "Semantic transformations:\n"
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n"

src/cbmc/cbmc_parse_options.h

@@ -45,6 +45,7 @@ class optionst;
   "(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
+  "(assertions-as-assumptions)" \
   "(cover):(cover-function-only)" \
   "(mm):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \