Merge pull request #1056 from diffblue/smowton/cleanup/remove_skip_before_cover_annotation

Remove skips before cover annotation

Author: smowton

src/cbmc/cbmc_parse_options.cpp

@@ -887,6 +887,10 @@ bool cbmc_parse_optionst::process_goto_program(
       remove_unused_functions(goto_functions, ui_message_handler);
     }
 
+    // remove skips such that trivial GOTOs are deleted and not considered
+    // for coverage annotation:
+    remove_skip(goto_functions);
+
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
@@ -915,7 +919,7 @@ bool cbmc_parse_optionst::process_goto_program(
         full_slicer(goto_functions, ns);
     }
 
-    // remove skips
+    // remove any skips introduced since coverage instrumentation
     remove_skip(goto_functions);
     goto_functions.update();
   }

src/symex/symex_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/xml_goto_trace.h>
 #include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_exceptions.h>
@@ -321,6 +322,10 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
       remove_unused_functions(goto_model.goto_functions, ui_message_handler);
     }
 
+    // remove skips such that trivial GOTOs are deleted and not considered
+    // for coverage annotation:
+    remove_skip(goto_model.goto_functions);
+
     if(cmdline.isset("cover"))
     {
       std::string criterion=cmdline.get_value("cover");