Option --no-built-in-assertions

This commit changes the behahaviour of --no-assertions so that
only user assertions are ignored.
Built-in assertions can be hidden by the new option
--no-built-in-assertions.

src/analyses/goto_check.cpp

@@ -55,6 +55,7 @@ public:
     retain_trivial=_options.get_bool_option("retain-trivial");
     enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
     enable_assertions=_options.get_bool_option("assertions");
+    enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
   }
@@ -125,6 +126,7 @@ protected:
   bool retain_trivial;
   bool enable_assert_to_assume;
   bool enable_assertions;
+  bool enable_built_in_assertions;
   bool enable_assumptions;
 
   typedef optionst::value_listt error_labelst;
@@ -1730,9 +1732,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
     }
     else if(i.is_assert())
     {
-      if(i.source_location.get_bool("user-provided") &&
-         i.source_location.get_property_class()!="error label" &&
-         !enable_assertions)
+      bool is_user_provided=i.source_location.get_bool("user-provided");
+      if((is_user_provided && !enable_assertions &&
+          i.source_location.get_property_class()!="error label") ||
+         (!is_user_provided && !enable_built_in_assertions))
         i.type=SKIP;
     }
     else if(i.is_assume())

src/cbmc/cbmc_parse_options.cpp

@@ -237,6 +237,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("assertions", true);
 
+  // check built-in assertions
+  if(cmdline.isset("no-built-in-assertions"))
+    options.set_option("built-in-assertions", false);
+  else
+    options.set_option("built-in-assertions", true);
+
   // use assumptions
   if(cmdline.isset("no-assumptions"))
     options.set_option("assumptions", false);
@@ -1148,6 +1154,7 @@ void cbmc_parse_optionst::help()
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --no-assertions              ignore user assertions\n"
+    " --no-built-in-assertions     ignore assertions in built-in library\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -32,6 +32,7 @@ class optionst;
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
+  "(no-built-in-assertions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \

src/goto-programs/builtin_functions.cpp

@@ -1304,7 +1304,9 @@ void goto_convertt::do_function_call_symbol(
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=arguments[0];
     t->source_location=function.source_location();
-    t->source_location.set("user-provided", true);
+    t->source_location.set(
+      "user-provided",
+      !function.source_location().is_built_in());
     t->source_location.set_property_class(ID_assertion);
     t->source_location.set_comment(description);