diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 4494aa33e76..7bba83bd298 100644 --- a/src/analyses/goto_check.cpp +++ b/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()) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e33e700e0ca..a8081e7c8a2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index a3fc5e7e7d3..fc2c578b69f 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/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)" \ diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index 8f64f9900a8..69af02e9e9e 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/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), "first))) continue; const coverage_recordt &f_cov=it->second; diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 2988b8637d2..96b21195a82 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/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), "source_location.is_built_in()) files[file].insert(it->source_location.get_line()); } } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fa92bc27cc7..ede599b6d8b 100644 --- a/src/goto-instrument/cover.cpp +++ b/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()), - "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); diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 8e95a03d853..8b0bd6dc46c 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/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()=="" || + 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()=="" || + source_location.is_built_in() || source_location.get_line().empty()) { step_to_node[step_nr]=sink; diff --git a/src/util/source_location.h b/src/util/source_location.h index b24befcb8c4..b9cf434f3b0 100644 --- a/src/util/source_location.h +++ b/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=""; + std::string built_in2=""; + 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(get_nil_irep());