From 554605b2b1e3ba22f5823bb5f682ecc9b6104b51 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 15 Apr 2017 16:21:13 +0100 Subject: [PATCH] Configure built-in-assertions for all callers of goto_check This was CBMC-only. Thus invoking, e.g., goto-instrument would remove all generated assertions as goto_check replaced them by SKIP. --- src/analyses/goto_check.h | 6 ++++-- src/cbmc/cbmc_parse_options.cpp | 7 ------- 2 files changed, 4 insertions(+), 9 deletions(-) diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index 4e1bbbbba60..2089d744fd2 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -33,7 +33,7 @@ void goto_check( "(bounds-check)(pointer-check)(memory-leak-check)" \ "(div-by-zero-check)(signed-overflow-check)(unsigned-overflow-check)" \ "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ - "(float-overflow-check)(nan-check)" + "(float-overflow-check)(nan-check)(no-built-in-assertions)" #define HELP_GOTO_CHECK \ " --bounds-check enable array bounds checks\n" \ @@ -47,6 +47,7 @@ void goto_check( " --undefined-shift-check check shift greater than bit-width\n" \ " --float-overflow-check check floating-point for +/-Inf\n" \ " --nan-check check floating-point for NaN\n" \ + " --no-built-in-assertions ignore assertions in built-in library\n" \ #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ @@ -59,6 +60,7 @@ void goto_check( options.set_option("conversion-check", cmdline.isset("conversion-check")); \ options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("nan-check", cmdline.isset("nan-check")) + options.set_option("nan-check", cmdline.isset("nan-check")); \ + options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */ #endif // CPROVER_ANALYSES_GOTO_CHECK_H diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 50629651dca..af92610d2c6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -237,12 +237,6 @@ 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); @@ -1147,7 +1141,6 @@ 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(*)