Merge pull request #681 from peterschrammel/no-assertions-for-user-only

No-assertions should not affect assertions in built-ins

Author: Daniel Kroening

src/analyses/goto_check.cpp

@@ -55,6 +55,7 @@ class goto_checkt
     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 @@ class goto_checkt
   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);
@@ -1142,6 +1148,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/cbmc/symex_coverage.cpp

@@ -318,7 +318,7 @@ void symex_coveraget::compute_overall_coverage(
       it!=file_records.end();
       ++it)
   {
-    if(has_prefix(id2string(it->first), "<builtin-"))
+    if(source_locationt::is_built_in(id2string(it->first)))
       continue;
 
     const coverage_recordt &f_cov=it->second;

src/goto-instrument/count_eloc.cpp

@@ -44,7 +44,7 @@ static void collect_eloc(
       const irep_idt &file=it->source_location.get_file();
 
       if(!file.empty() &&
-         !has_prefix(id2string(file), "<built-in-"))
+         !it->source_location.is_built_in())
         files[file].insert(it->source_location.get_line());
     }
   }

src/goto-instrument/cover.cpp

@@ -1082,9 +1082,7 @@ void instrument_cover_goals(
 
   // ignore if built-in library
   if(!goto_program.instructions.empty() &&
-     has_prefix(
-       id2string(goto_program.instructions.front().source_location.get_file()),
-       "<builtin-library-"))
+     goto_program.instructions.front().source_location.is_built_in())
     return;
 
   const irep_idt coverage_criterion=as_string(criterion);

src/goto-programs/builtin_functions.cpp

@@ -1320,7 +1320,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);
 

src/goto-programs/graphml_witness.cpp

@@ -196,7 +196,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
        (it->is_goto() && it->pc->guard.is_true()) ||
        source_location.is_nil() ||
        source_location.get_file().empty() ||
-       source_location.get_file()=="<built-in-additions>" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[it->step_nr]=sink;
@@ -392,7 +392,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
        (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
        (it->is_goto() && it->source.pc->guard.is_true()) ||
        source_location.is_nil() ||
-       source_location.get_file()=="<built-in-additions>" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[step_nr]=sink;

src/util/source_location.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_SOURCE_LOCATION_H
 
 #include "irep.h"
+#include "prefix.h"
 
 class source_locationt:public irept
 {
@@ -138,6 +139,18 @@ class source_locationt:public irept
     return get_bool(ID_hide);
   }
 
+  static bool is_built_in(const std::string &s)
+  {
+    std::string built_in1="<built-in-"; // "<built-in-additions>";
+    std::string built_in2="<builtin-"; // "<builtin-architecture-strings>";
+    return has_prefix(s, built_in1) || has_prefix(s, built_in2);
+  }
+
+  bool is_built_in() const
+  {
+    return is_built_in(id2string(get_file()));
+  }
+
   static const source_locationt &nil()
   {
     return static_cast<const source_locationt &>(get_nil_irep());