From a2a68facf04275e42f22b1ac37a228d6808ab97d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 10 Nov 2023 16:07:00 +0000 Subject: [PATCH 1/8] [WIP] Enable default flags on for checks --- src/ansi-c/goto_check_c.h | 12 ++++++------ src/cbmc/cbmc_parse_options.cpp | 30 +++++++++++++++++++++++++++++- src/cbmc/cbmc_parse_options.h | 4 +++- 3 files changed, 38 insertions(+), 8 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 451bfa15c3c..d31cd4efb1e 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -79,21 +79,21 @@ void goto_check_c( // clang-format off #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ - options.set_option("bounds-check", cmdline.isset("bounds-check")); \ - options.set_option("pointer-check", cmdline.isset("pointer-check")); \ + options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \ + options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \ options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \ options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \ + options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \ options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \ - options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \ 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("undefined-shift-check", !cmdline.isset("no-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("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial-checks", \ cmdline.isset("retain-trivial-checks")); \ options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 6f090945d35..cab6a9d3a65 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -92,6 +92,9 @@ ::cbmc_parse_optionst::cbmc_parse_optionst( void cbmc_parse_optionst::set_default_options(optionst &options) { + // Enable the standard checks by default, unless a user overrides. + options.set_option("standard-checks", true); + // Default true options.set_option("built-in-assertions", true); options.set_option("propagation", true); @@ -106,6 +109,20 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("depth", UINT32_MAX); } +void cbmc_parse_optionst::set_soundness_on_by_default(optionst &options) +{ + // Analysis flags on by default + options.set_option("bounds-check", true); + options.set_option("pointer-check", true); + options.set_option("pointer-primitive-check", true); + options.set_option("malloc-may-fail", true); + // TODO: Default malloc-fail-profile + options.set_option("div-by-zero-check", true); + options.set_option("signed-overflow-check", true); + options.set_option("undefined-shift-check", true); + options.set_option("unwinding-assertions", true); +} + void cbmc_parse_optionst::get_command_line_options(optionst &options) { if(config.set(cmdline)) @@ -117,6 +134,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_options(options); parse_c_object_factory_options(cmdline, options); + // Enable flags that in combination provide analysis with no surprises + // (expected checks and no unsoundness by missing checks). + if (options.get_bool_option("standard-checks")) + set_soundness_on_by_default(options); + if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); @@ -309,8 +331,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // generate unwinding assertions - if(cmdline.isset("unwinding-assertions")) + // TODO: Fotis: revisit + if(cmdline.isset("no-unwinding-assertions")) { + options.set_option("unwinding-assertions", false); + options.set_option("paths-symex-explore-all", false); + } else { + // Not really needed, as it's now on by default, but keeping it here + // for completeness' sake. options.set_option("unwinding-assertions", true); options.set_option("paths-symex-explore-all", true); } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 8ec5b04ffaa..433c06c84f0 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -33,7 +33,8 @@ class optionst; // clang-format off #define CBMC_OPTIONS \ - OPT_BMC \ + OPT_BMC \ + "(standard-checks)" \ "(preprocess)(slice-by-trace):" \ OPT_FUNCTIONS \ "(no-simplify)(full-slice)" \ @@ -90,6 +91,7 @@ class cbmc_parse_optionst : public parse_options_baset /// This function can be called from clients that wish to emulate CBMC's /// default behaviour, for example unit tests. static void set_default_options(optionst &); + static void set_soundness_on_by_default(optionst &options); static bool process_goto_program(goto_modelt &, const optionst &, messaget &); From 0a615dec1eb5d7430a1f8f6a3af47d731b581ca9 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 23 Nov 2023 15:40:41 +0000 Subject: [PATCH 2/8] Group default options into own DEFINE --- src/ansi-c/goto_check_c.h | 25 +++++++++++++++---------- src/cbmc/cbmc_parse_options.cpp | 16 +++++++++------- src/cbmc/cbmc_parse_options.h | 4 ++-- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index d31cd4efb1e..85c921cd6b4 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -38,7 +38,7 @@ void goto_check_c( message_handlert &message_handler); #define OPT_GOTO_CHECK \ - "(bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \ + "(no-bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \ "(div-by-zero-check)(enum-range-check)" \ "(signed-overflow-check)(unsigned-overflow-check)" \ "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ @@ -77,31 +77,36 @@ void goto_check_c( " {y--no-assumptions} \t ignore user assumptions\n" \ " {y--assert-to-assume} \t convert user assertions to assumptions\n" +// clang-format off +#define PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options) \ + options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \ + options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \ + options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \ + options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("undefined-shift-check", !cmdline.isset("no-undefined-shift-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + (void) 0; +// clang-format on + // clang-format off #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ - options.set_option("bounds-check", !cmdline.isset("no-bounds-check")); \ - options.set_option("pointer-check", !cmdline.isset("no-pointer-check")); \ options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \ options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("div-by-zero-check", !cmdline.isset("no-div-by-zero-check")); \ options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \ - options.set_option("signed-overflow-check", !cmdline.isset("no-signed-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */ \ options.set_option("conversion-check", cmdline.isset("conversion-check")); \ - options.set_option("undefined-shift-check", !cmdline.isset("no-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("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("pointer-primitive-check", !cmdline.isset("no-pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ - options.set_option("retain-trivial-checks", \ - cmdline.isset("retain-trivial-checks")); \ options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \ options.set_option("assumptions", !cmdline.isset("no-assumptions")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("retain-trivial-checks", \ + cmdline.isset("retain-trivial-checks")); \ options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \ options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \ if(cmdline.isset("error-label")) \ - options.set_option("error-label", cmdline.get_values("error-label")); \ + options.set_option("error-label", cmdline.get_values("error-label")); \ (void)0 // clang-format on diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cab6a9d3a65..0065e512b43 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -109,7 +109,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options) options.set_option("depth", UINT32_MAX); } -void cbmc_parse_optionst::set_soundness_on_by_default(optionst &options) +void cbmc_parse_optionst::set_default_analysis_flags(optionst &options) { // Analysis flags on by default options.set_option("bounds-check", true); @@ -134,11 +134,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_options(options); parse_c_object_factory_options(cmdline, options); - // Enable flags that in combination provide analysis with no surprises - // (expected checks and no unsoundness by missing checks). - if (options.get_bool_option("standard-checks")) - set_soundness_on_by_default(options); - if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); @@ -327,7 +322,14 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) "self-loops-to-assumptions", !cmdline.isset("no-self-loops-to-assumptions")); - // all checks supported by goto_check + // Enable flags that in combination provide analysis with no surprises + // (expected checks and no unsoundness by missing checks). + if (!cmdline.isset("no-standard-checks") && options.get_bool_option("standard-checks")) + set_default_analysis_flags(options); + else + PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options); + + // all (non-default) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // generate unwinding assertions diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 433c06c84f0..c3fde199e70 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -34,7 +34,7 @@ class optionst; // clang-format off #define CBMC_OPTIONS \ OPT_BMC \ - "(standard-checks)" \ + "(no-standard-checks)" \ "(preprocess)(slice-by-trace):" \ OPT_FUNCTIONS \ "(no-simplify)(full-slice)" \ @@ -91,7 +91,7 @@ class cbmc_parse_optionst : public parse_options_baset /// This function can be called from clients that wish to emulate CBMC's /// default behaviour, for example unit tests. static void set_default_options(optionst &); - static void set_soundness_on_by_default(optionst &options); + static void set_default_analysis_flags(optionst &options); static bool process_goto_program(goto_modelt &, const optionst &, messaget &); From 5a1a2514f68dbe241c9c9b814f7355a4d53323ee Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 23 Nov 2023 15:44:01 +0000 Subject: [PATCH 3/8] Add reminders of places to invoke default argument setup after testing --- src/goto-analyzer/goto_analyzer_parse_options.cpp | 1 + src/goto-diff/goto_diff_parse_options.cpp | 1 + src/goto-instrument/goto_instrument_parse_options.cpp | 1 + src/libcprover-cpp/api_options.cpp | 1 + 4 files changed, 4 insertions(+) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index b64119b6b9e..1e2eae14644 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -67,6 +67,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); + // TODO: Will need to add the default one here. // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index b30a71df7d3..29c99432f2b 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -59,6 +59,7 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cover")) parse_cover_options(cmdline, options); + // TODO: May need to add default one here. // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 55721374ce6..97fd4847c77 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1025,6 +1025,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() else options.set_option("simplify", true); + // TODO: May need to add the default one here // all checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); diff --git a/src/libcprover-cpp/api_options.cpp b/src/libcprover-cpp/api_options.cpp index c4d1839ddec..6019487f2ac 100644 --- a/src/libcprover-cpp/api_options.cpp +++ b/src/libcprover-cpp/api_options.cpp @@ -17,6 +17,7 @@ static std::unique_ptr make_internal_default_options() { std::unique_ptr options = std::make_unique(); cmdlinet command_line; + // TODO: May need to add the default one here. PARSE_OPTIONS_GOTO_CHECK(command_line, (*options)); parse_solver_options(command_line, *options); options->set_option("built-in-assertions", true); From 3a09e6f46f6d9c61a5275bc388a7ac51b4227d5b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 23 Nov 2023 16:58:21 +0000 Subject: [PATCH 4/8] Adjust default flags in regression/cbmc tests. --- regression/cbmc/ACSL/operators.desc | 2 +- regression/cbmc/Address_of1/test.desc | 2 +- regression/cbmc/Anonymous_Struct1/test.desc | 2 +- regression/cbmc/Array_UF21/test.desc | 2 +- regression/cbmc/Array_operations1/full-slice.desc | 4 ++-- regression/cbmc/Array_operations1/test.desc | 2 +- regression/cbmc/Associativity1/test.desc | 2 +- regression/cbmc/BV_Arithmetic3/test.desc | 2 +- regression/cbmc/BV_Arithmetic4/test.desc | 2 +- regression/cbmc/Bitfields3/paths.desc | 2 +- regression/cbmc/Bitfields3/test.desc | 2 +- regression/cbmc/Bool/bool5-full-slice.desc | 2 +- regression/cbmc/Bool/bool5.desc | 2 +- regression/cbmc/Boolean_Guards1/test.desc | 2 +- regression/cbmc/Endianness5/test.desc | 2 +- regression/cbmc/Failed_Symbols1/test.desc | 2 +- regression/cbmc/Float-flags-no-simp1/test.desc | 2 +- regression/cbmc/Float13/test.desc | 2 +- regression/cbmc/Free1/test.desc | 2 +- regression/cbmc/Free3/test.desc | 2 +- regression/cbmc/Free4/test.desc | 2 +- regression/cbmc/Function1/test.desc | 2 +- regression/cbmc/Function5/test.desc | 2 +- regression/cbmc/Function_Pointer14/test.desc | 2 +- regression/cbmc/Function_Pointer16/test.desc | 2 +- regression/cbmc/Function_Pointer18/test.desc | 2 +- regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc | 2 +- regression/cbmc/Linking6/test.desc | 2 +- regression/cbmc/Linking7/member-name-mismatch.desc | 2 +- regression/cbmc/Linking7/test.desc | 2 +- regression/cbmc/Linking8/test.desc | 2 +- regression/cbmc/Local_out_of_scope1/test.desc | 2 +- regression/cbmc/Local_out_of_scope4/test.desc | 2 +- regression/cbmc/Malloc1/test.desc | 2 +- regression/cbmc/Malloc10/test.desc | 2 +- regression/cbmc/Malloc11/slice-formula.desc | 2 +- regression/cbmc/Malloc2/test.desc | 2 +- regression/cbmc/Malloc23/test.desc | 2 +- regression/cbmc/Malloc24/test.desc | 2 +- regression/cbmc/Malloc3/test.desc | 2 +- regression/cbmc/Malloc4/test.desc | 2 +- regression/cbmc/Malloc5/test.desc | 2 +- regression/cbmc/Malloc6/test.desc | 2 +- regression/cbmc/Malloc7/test.desc | 2 +- regression/cbmc/Malloc8/test.desc | 2 +- regression/cbmc/Malloc9/test.desc | 2 +- regression/cbmc/Multi_Dimensional_Array6/test.desc | 2 +- regression/cbmc/Pointer1/test.desc | 2 +- regression/cbmc/Pointer10/test.desc | 2 +- regression/cbmc/Pointer11/test.desc | 2 +- regression/cbmc/Pointer12/test.desc | 2 +- regression/cbmc/Pointer14/test.desc | 2 +- regression/cbmc/Pointer15/test.desc | 2 +- regression/cbmc/Pointer17/test.desc | 2 +- regression/cbmc/Pointer18/full-slice.desc | 2 +- regression/cbmc/Pointer18/test.desc | 2 +- regression/cbmc/Pointer20/test.desc | 2 +- regression/cbmc/Pointer21/test.desc | 2 +- regression/cbmc/Pointer23/test.desc | 2 +- regression/cbmc/Pointer24/test.desc | 2 +- regression/cbmc/Pointer28/test.desc | 2 +- regression/cbmc/Pointer3/test.desc | 2 +- regression/cbmc/Pointer30/test.desc | 2 +- regression/cbmc/Pointer31/test.desc | 2 +- regression/cbmc/Pointer4/test.desc | 2 +- regression/cbmc/Pointer6/test.desc | 2 +- regression/cbmc/Pointer7/test.desc | 2 +- regression/cbmc/Pointer8/test.desc | 2 +- regression/cbmc/Pointer9/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic1/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic10/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic11/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic2/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic3/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic4/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic5/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic6/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic7/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic8/test.desc | 2 +- regression/cbmc/Pointer_Arithmetic9/test.desc | 2 +- regression/cbmc/Pointer_Object_Type1/test.desc | 2 +- regression/cbmc/Pointer_array3/test.desc | 2 +- regression/cbmc/Pointer_byte_extract5/no-simplify.desc | 2 +- regression/cbmc/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc/Pointer_difference2/test.desc | 2 +- regression/cbmc/Recursion2/test.desc | 2 +- regression/cbmc/Sideeffects5/test.desc | 2 +- regression/cbmc/Sideeffects6/test.desc | 2 +- regression/cbmc/Sideeffects8/test.desc | 2 +- regression/cbmc/String1/test.desc | 2 +- regression/cbmc/String2/test.desc | 2 +- regression/cbmc/String3/test.desc | 2 +- regression/cbmc/String4/test.desc | 2 +- regression/cbmc/String5/test.desc | 2 +- regression/cbmc/String7/test.desc | 2 +- regression/cbmc/String8/test.desc | 2 +- regression/cbmc/String_Abstraction1/test.desc | 2 +- regression/cbmc/String_Abstraction10/test.desc | 2 +- regression/cbmc/String_Abstraction2/test.desc | 2 +- regression/cbmc/String_Abstraction23/test.desc | 2 +- regression/cbmc/String_Abstraction3/test.desc | 2 +- regression/cbmc/String_Abstraction4/test.desc | 2 +- regression/cbmc/String_Abstraction5/test.desc | 2 +- regression/cbmc/String_Abstraction6/test.desc | 2 +- regression/cbmc/String_Abstraction7/test.desc | 2 +- regression/cbmc/String_Abstraction8/test.desc | 2 +- regression/cbmc/String_Abstraction9/test.desc | 2 +- regression/cbmc/Struct_Pointer2/test.desc | 2 +- regression/cbmc/Undefined_Shift1/test.desc | 2 +- regression/cbmc/pointer-check-01/test.desc | 2 +- regression/cbmc/pointer-check-02/test.desc | 2 +- regression/cbmc/pointer-extra-checks/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- regression/cbmc/pointer-primitive-check-01/test.desc | 2 +- regression/cbmc/pointer-primitive-check-02/test.desc | 2 +- regression/cbmc/pointer-primitive-check-04/test.desc | 2 +- regression/cbmc/pragma_cprover1/test.desc | 2 +- regression/cbmc/pragma_cprover2/test.desc | 4 ++-- regression/cbmc/pragma_cprover3/test.desc | 2 +- regression/cbmc/pragma_cprover_enable1/test.desc | 2 +- regression/cbmc/pragma_cprover_enable2/test.desc | 2 +- regression/cbmc/pragma_cprover_enable_all/test.desc | 2 +- .../cbmc/pragma_cprover_enable_disable_global_on/test.desc | 2 +- regression/cbmc/r_w_ok10/test.desc | 2 +- regression/cbmc/return5/test.desc | 2 +- regression/cbmc/return9/test.desc | 2 +- regression/cbmc/set-property-inline1/test.desc | 2 +- .../short_circuit_implies/short-circuit-memory-checks.desc | 2 +- regression/cbmc/show_properties1/test.desc | 2 +- .../cbmc/simplify_singleton_interval_7690/negative_test.desc | 2 +- .../cbmc/simplify_singleton_interval_7690/positive_test.desc | 2 +- .../cbmc/simplify_singleton_interval_7690/test_smt2.desc | 2 +- regression/cbmc/struct12/test.desc | 2 +- regression/cbmc/struct6/test.desc | 2 +- regression/cbmc/struct7/test.desc | 2 +- regression/cbmc/switch8/program-only.desc | 2 +- regression/cbmc/switch8/test.desc | 2 +- regression/cbmc/switch9/test.desc | 2 +- regression/cbmc/unsigned___int128/test.desc | 2 +- regression/cbmc/void_pointer1/test.desc | 2 +- regression/cbmc/void_pointer2/test.desc | 2 +- regression/cbmc/void_pointer6/test.desc | 2 +- regression/cbmc/void_pointer7/test.desc | 2 +- 145 files changed, 147 insertions(+), 147 deletions(-) diff --git a/regression/cbmc/ACSL/operators.desc b/regression/cbmc/ACSL/operators.desc index 0f3f061b7a7..9d7051b2b97 100644 --- a/regression/cbmc/ACSL/operators.desc +++ b/regression/cbmc/ACSL/operators.desc @@ -1,6 +1,6 @@ CORE no-new-smt operators.c - +--no-signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Address_of1/test.desc b/regression/cbmc/Address_of1/test.desc index d891ef29be9..d4d93c6de01 100644 --- a/regression/cbmc/Address_of1/test.desc +++ b/regression/cbmc/Address_of1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---stop-on-fail +--stop-on-fail --no-pointer-check ^\[main\.assertion ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Anonymous_Struct1/test.desc b/regression/cbmc/Anonymous_Struct1/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Anonymous_Struct1/test.desc +++ b/regression/cbmc/Anonymous_Struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc index e9d3c4ebe15..8c2f51722b2 100644 --- a/regression/cbmc/Array_UF21/test.desc +++ b/regression/cbmc/Array_UF21/test.desc @@ -1,6 +1,6 @@ CORE main.c ---arrays-uf-always --bounds-check +--arrays-uf-always ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Array_operations1/full-slice.desc b/regression/cbmc/Array_operations1/full-slice.desc index 2fe6c114f6e..7fa8f83e6e0 100644 --- a/regression/cbmc/Array_operations1/full-slice.desc +++ b/regression/cbmc/Array_operations1/full-slice.desc @@ -10,9 +10,9 @@ main.c ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE -^\*\* 5 of 15 failed +^\*\* 5 of 19 failed ^VERIFICATION FAILED$ -- ^warning: ignoring -- -Verify the properties of various cprover array primitves +Verify the properties of various CPROVER array primitives. diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc index ba6bbd32daf..3bed4c0560a 100644 --- a/regression/cbmc/Array_operations1/test.desc +++ b/regression/cbmc/Array_operations1/test.desc @@ -10,7 +10,7 @@ main.c ^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE ^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE ^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE -^\*\* 5 of 15 failed +^\*\* 5 of 19 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/Associativity1/test.desc b/regression/cbmc/Associativity1/test.desc index 9efefbc7362..f6a6dcb1415 100644 --- a/regression/cbmc/Associativity1/test.desc +++ b/regression/cbmc/Associativity1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc index d2a7e3e7574..9c7dfb426dd 100644 --- a/regression/cbmc/BV_Arithmetic3/test.desc +++ b/regression/cbmc/BV_Arithmetic3/test.desc @@ -3,7 +3,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ -(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$) +(Starting CEGAR Loop|^Generated 68 VCC\(s\), 0 remaining after simplification$) ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc/BV_Arithmetic4/test.desc b/regression/cbmc/BV_Arithmetic4/test.desc index 23e981a3744..d5d60858ba8 100644 --- a/regression/cbmc/BV_Arithmetic4/test.desc +++ b/regression/cbmc/BV_Arithmetic4/test.desc @@ -1,6 +1,6 @@ CORE main.c - --unwind 32 + --unwind 32 --no-signed-overflow-check --no-undefined-shift-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc index 2b3f7623037..6ac421e404a 100644 --- a/regression/cbmc/Bitfields3/paths.desc +++ b/regression/cbmc/Bitfields3/paths.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check --bounds-check --paths lifo +--paths lifo ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc index 032c2879b43..1c039664a91 100644 --- a/regression/cbmc/Bitfields3/test.desc +++ b/regression/cbmc/Bitfields3/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Bool/bool5-full-slice.desc b/regression/cbmc/Bool/bool5-full-slice.desc index 6fc49d6b0cf..cff6a9ffa72 100644 --- a/regression/cbmc/Bool/bool5-full-slice.desc +++ b/regression/cbmc/Bool/bool5-full-slice.desc @@ -1,7 +1,7 @@ CORE bool5.c --full-slice -Generated 4 VCC\(s\), 0 remaining after simplification +Generated 10 VCC\(s\), 0 remaining after simplification ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Bool/bool5.desc b/regression/cbmc/Bool/bool5.desc index 273ab4b0ed7..a27559ad37a 100644 --- a/regression/cbmc/Bool/bool5.desc +++ b/regression/cbmc/Bool/bool5.desc @@ -1,7 +1,7 @@ CORE bool5.c -Generated 4 VCC\(s\), 0 remaining after simplification +Generated 10 VCC\(s\), 0 remaining after simplification ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Boolean_Guards1/test.desc b/regression/cbmc/Boolean_Guards1/test.desc index da239c1965b..f6a6dcb1415 100644 --- a/regression/cbmc/Boolean_Guards1/test.desc +++ b/regression/cbmc/Boolean_Guards1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---bounds-check --pointer-check +--no-signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Endianness5/test.desc b/regression/cbmc/Endianness5/test.desc index 4e90da351ba..9845e70d84b 100644 --- a/regression/cbmc/Endianness5/test.desc +++ b/regression/cbmc/Endianness5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---little-endian --pointer-check +--little-endian ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Failed_Symbols1/test.desc b/regression/cbmc/Failed_Symbols1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc/Failed_Symbols1/test.desc +++ b/regression/cbmc/Failed_Symbols1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Float-flags-no-simp1/test.desc b/regression/cbmc/Float-flags-no-simp1/test.desc index 74e429efb6d..7431ef153f6 100644 --- a/regression/cbmc/Float-flags-no-simp1/test.desc +++ b/regression/cbmc/Float-flags-no-simp1/test.desc @@ -1,6 +1,6 @@ CORE broken-cprover-smt-backend thorough-paths no-new-smt main.c ---floatbv --no-simplify +--floatbv --no-simplify --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Float13/test.desc b/regression/cbmc/Float13/test.desc index 9efefbc7362..e9506d33442 100644 --- a/regression/cbmc/Float13/test.desc +++ b/regression/cbmc/Float13/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-div-by-zero-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Free1/test.desc b/regression/cbmc/Free1/test.desc index 950f6791fef..6de79559914 100644 --- a/regression/cbmc/Free1/test.desc +++ b/regression/cbmc/Free1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Free3/test.desc b/regression/cbmc/Free3/test.desc index 950f6791fef..6de79559914 100644 --- a/regression/cbmc/Free3/test.desc +++ b/regression/cbmc/Free3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Free4/test.desc b/regression/cbmc/Free4/test.desc index 950f6791fef..6de79559914 100644 --- a/regression/cbmc/Free4/test.desc +++ b/regression/cbmc/Free4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Function1/test.desc b/regression/cbmc/Function1/test.desc index 9efefbc7362..f6a6dcb1415 100644 --- a/regression/cbmc/Function1/test.desc +++ b/regression/cbmc/Function1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Function5/test.desc b/regression/cbmc/Function5/test.desc index d877a4247fb..778e4a60a5a 100644 --- a/regression/cbmc/Function5/test.desc +++ b/regression/cbmc/Function5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^SIGNAL=0$ ^EXIT=10$ ^\[.*\] .* dereference failure: pointer outside object bounds in \*p: FAILURE$ diff --git a/regression/cbmc/Function_Pointer14/test.desc b/regression/cbmc/Function_Pointer14/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Function_Pointer14/test.desc +++ b/regression/cbmc/Function_Pointer14/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Function_Pointer16/test.desc b/regression/cbmc/Function_Pointer16/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Function_Pointer16/test.desc +++ b/regression/cbmc/Function_Pointer16/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc index 3cd78297904..7aacf515906 100644 --- a/regression/cbmc/Function_Pointer18/test.desc +++ b/regression/cbmc/Function_Pointer18/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS -\[main.pointer_dereference.1\] line 28 dereferenced function pointer must be f2: FAILURE$ +\[main.pointer_dereference.\d*\] line 28 dereferenced function pointer must be f2: FAILURE$ \[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS \[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc index 01bd38d3647..68ecc9e8916 100644 --- a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc +++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function foo --pointer-check +--function foo ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$ ^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$ ^EXIT=10$ diff --git a/regression/cbmc/Linking6/test.desc b/regression/cbmc/Linking6/test.desc index 67f1dd7303f..af20f90c655 100644 --- a/regression/cbmc/Linking6/test.desc +++ b/regression/cbmc/Linking6/test.desc @@ -1,6 +1,6 @@ CORE main.c -module.c --pointer-check +module.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc index 3ed8ac3b6e2..77efea6c1ef 100644 --- a/regression/cbmc/Linking7/member-name-mismatch.desc +++ b/regression/cbmc/Linking7/member-name-mismatch.desc @@ -6,6 +6,6 @@ module2.c ^VERIFICATION FAILED$ line 21 assertion \*g\.a == 42: SUCCESS line 22 assertion \*g\.c == 41: FAILURE -^\*\* 1 of 3 failed +^\*\* 1 of \d+ failed -- ^warning: ignoring diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc index 2917ed7e4f6..4678e189857 100644 --- a/regression/cbmc/Linking7/test.desc +++ b/regression/cbmc/Linking7/test.desc @@ -4,7 +4,7 @@ module.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 1 of 3 failed +^\*\* 1 of \d+ failed line 21 assertion \*g\.a == 42: SUCCESS line 22 assertion \*g\.b == 41: FAILURE -- diff --git a/regression/cbmc/Linking8/test.desc b/regression/cbmc/Linking8/test.desc index ebb8d9d1d71..2acb6544444 100644 --- a/regression/cbmc/Linking8/test.desc +++ b/regression/cbmc/Linking8/test.desc @@ -1,6 +1,6 @@ CORE b.c -a.c --pointer-check +a.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Local_out_of_scope1/test.desc b/regression/cbmc/Local_out_of_scope1/test.desc index 950f6791fef..6de79559914 100644 --- a/regression/cbmc/Local_out_of_scope1/test.desc +++ b/regression/cbmc/Local_out_of_scope1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Local_out_of_scope4/test.desc b/regression/cbmc/Local_out_of_scope4/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Local_out_of_scope4/test.desc +++ b/regression/cbmc/Local_out_of_scope4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc1/test.desc b/regression/cbmc/Malloc1/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc1/test.desc +++ b/regression/cbmc/Malloc1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc10/test.desc b/regression/cbmc/Malloc10/test.desc index 98ec2212e40..6e8c19959c9 100644 --- a/regression/cbmc/Malloc10/test.desc +++ b/regression/cbmc/Malloc10/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc11/slice-formula.desc b/regression/cbmc/Malloc11/slice-formula.desc index 5b5af79ac60..e60ca3550e7 100644 --- a/regression/cbmc/Malloc11/slice-formula.desc +++ b/regression/cbmc/Malloc11/slice-formula.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --slice-formula +--slice-formula ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc2/test.desc b/regression/cbmc/Malloc2/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc2/test.desc +++ b/regression/cbmc/Malloc2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 39d94af76fd..e1542884bee 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ pointer outside object bounds in \*p: FAILURE diff --git a/regression/cbmc/Malloc24/test.desc b/regression/cbmc/Malloc24/test.desc index cf64d363c65..bf39eb66071 100644 --- a/regression/cbmc/Malloc24/test.desc +++ b/regression/cbmc/Malloc24/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 4 --pointer-check --unwinding-assertions +--unwind 4 --unwinding-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc3/test.desc b/regression/cbmc/Malloc3/test.desc index 950f6791fef..6de79559914 100644 --- a/regression/cbmc/Malloc3/test.desc +++ b/regression/cbmc/Malloc3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Malloc4/test.desc b/regression/cbmc/Malloc4/test.desc index ac6b317a781..d11741ada5b 100644 --- a/regression/cbmc/Malloc4/test.desc +++ b/regression/cbmc/Malloc4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Malloc5/test.desc b/regression/cbmc/Malloc5/test.desc index 72b27267062..d1233272a46 100644 --- a/regression/cbmc/Malloc5/test.desc +++ b/regression/cbmc/Malloc5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Malloc6/test.desc b/regression/cbmc/Malloc6/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc6/test.desc +++ b/regression/cbmc/Malloc6/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc7/test.desc b/regression/cbmc/Malloc7/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc7/test.desc +++ b/regression/cbmc/Malloc7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc8/test.desc b/regression/cbmc/Malloc8/test.desc index 95528fabef5..facc8bd6eda 100644 --- a/regression/cbmc/Malloc8/test.desc +++ b/regression/cbmc/Malloc8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Malloc9/test.desc b/regression/cbmc/Malloc9/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc9/test.desc +++ b/regression/cbmc/Malloc9/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index 6694cf6e8b7..69ac2b33451 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -5,6 +5,6 @@ main.c ^SIGNAL=0$ ^\[main\.assertion\.1\] .*: SUCCESS$ ^\[main\.assertion\.2\] .*: FAILURE$ -^\*\* 1 of 2 failed +^\*\* 3 of 8 failed -- ^warning: ignoring diff --git a/regression/cbmc/Pointer1/test.desc b/regression/cbmc/Pointer1/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer1/test.desc +++ b/regression/cbmc/Pointer1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer10/test.desc b/regression/cbmc/Pointer10/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer10/test.desc +++ b/regression/cbmc/Pointer10/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer11/test.desc b/regression/cbmc/Pointer11/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer11/test.desc +++ b/regression/cbmc/Pointer11/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer12/test.desc b/regression/cbmc/Pointer12/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer12/test.desc +++ b/regression/cbmc/Pointer12/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer14/test.desc b/regression/cbmc/Pointer14/test.desc index 350a589e4a6..e2d2d714649 100644 --- a/regression/cbmc/Pointer14/test.desc +++ b/regression/cbmc/Pointer14/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer15/test.desc b/regression/cbmc/Pointer15/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer15/test.desc +++ b/regression/cbmc/Pointer15/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer17/test.desc b/regression/cbmc/Pointer17/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer17/test.desc +++ b/regression/cbmc/Pointer17/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer18/full-slice.desc b/regression/cbmc/Pointer18/full-slice.desc index 37c7526ffee..84c609faf08 100644 --- a/regression/cbmc/Pointer18/full-slice.desc +++ b/regression/cbmc/Pointer18/full-slice.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 1 --no-unwinding-assertions --pointer-check --full-slice +--unwind 1 --no-unwinding-assertions --full-slice ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer18/test.desc b/regression/cbmc/Pointer18/test.desc index 0b21ec028ac..4d988589f85 100644 --- a/regression/cbmc/Pointer18/test.desc +++ b/regression/cbmc/Pointer18/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 1 --no-unwinding-assertions --pointer-check +--unwind 1 --no-unwinding-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer20/test.desc b/regression/cbmc/Pointer20/test.desc index a0af87d2c09..17695a197ac 100644 --- a/regression/cbmc/Pointer20/test.desc +++ b/regression/cbmc/Pointer20/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer21/test.desc b/regression/cbmc/Pointer21/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer21/test.desc +++ b/regression/cbmc/Pointer21/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer23/test.desc b/regression/cbmc/Pointer23/test.desc index a0af87d2c09..17695a197ac 100644 --- a/regression/cbmc/Pointer23/test.desc +++ b/regression/cbmc/Pointer23/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer24/test.desc b/regression/cbmc/Pointer24/test.desc index d9a7678b126..1c039664a91 100644 --- a/regression/cbmc/Pointer24/test.desc +++ b/regression/cbmc/Pointer24/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer28/test.desc b/regression/cbmc/Pointer28/test.desc index 09aaafc1c87..366f3e536c7 100644 --- a/regression/cbmc/Pointer28/test.desc +++ b/regression/cbmc/Pointer28/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check --little-endian +--little-endian ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer3/test.desc b/regression/cbmc/Pointer3/test.desc index a0af87d2c09..17695a197ac 100644 --- a/regression/cbmc/Pointer3/test.desc +++ b/regression/cbmc/Pointer3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer30/test.desc b/regression/cbmc/Pointer30/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer30/test.desc +++ b/regression/cbmc/Pointer30/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer31/test.desc b/regression/cbmc/Pointer31/test.desc index a0af87d2c09..17695a197ac 100644 --- a/regression/cbmc/Pointer31/test.desc +++ b/regression/cbmc/Pointer31/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer4/test.desc b/regression/cbmc/Pointer4/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer4/test.desc +++ b/regression/cbmc/Pointer4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer6/test.desc b/regression/cbmc/Pointer6/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer6/test.desc +++ b/regression/cbmc/Pointer6/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer7/test.desc b/regression/cbmc/Pointer7/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer7/test.desc +++ b/regression/cbmc/Pointer7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer8/test.desc b/regression/cbmc/Pointer8/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer8/test.desc +++ b/regression/cbmc/Pointer8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer9/test.desc b/regression/cbmc/Pointer9/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer9/test.desc +++ b/regression/cbmc/Pointer9/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic1/test.desc b/regression/cbmc/Pointer_Arithmetic1/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic1/test.desc +++ b/regression/cbmc/Pointer_Arithmetic1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic10/test.desc b/regression/cbmc/Pointer_Arithmetic10/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic10/test.desc +++ b/regression/cbmc/Pointer_Arithmetic10/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc index f5e039ba3ed..9845e70d84b 100644 --- a/regression/cbmc/Pointer_Arithmetic11/test.desc +++ b/regression/cbmc/Pointer_Arithmetic11/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --little-endian +--little-endian ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic2/test.desc b/regression/cbmc/Pointer_Arithmetic2/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic2/test.desc +++ b/regression/cbmc/Pointer_Arithmetic2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic3/test.desc b/regression/cbmc/Pointer_Arithmetic3/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic3/test.desc +++ b/regression/cbmc/Pointer_Arithmetic3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic4/test.desc b/regression/cbmc/Pointer_Arithmetic4/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic4/test.desc +++ b/regression/cbmc/Pointer_Arithmetic4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic5/test.desc b/regression/cbmc/Pointer_Arithmetic5/test.desc index f9c919bbdc2..3387a15b315 100644 --- a/regression/cbmc/Pointer_Arithmetic5/test.desc +++ b/regression/cbmc/Pointer_Arithmetic5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check --function f +--function f ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer_Arithmetic6/test.desc b/regression/cbmc/Pointer_Arithmetic6/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic6/test.desc +++ b/regression/cbmc/Pointer_Arithmetic6/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic7/test.desc b/regression/cbmc/Pointer_Arithmetic7/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic7/test.desc +++ b/regression/cbmc/Pointer_Arithmetic7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Arithmetic8/test.desc b/regression/cbmc/Pointer_Arithmetic8/test.desc index 4b9176a942e..6de79559914 100644 --- a/regression/cbmc/Pointer_Arithmetic8/test.desc +++ b/regression/cbmc/Pointer_Arithmetic8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer_Arithmetic9/test.desc b/regression/cbmc/Pointer_Arithmetic9/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic9/test.desc +++ b/regression/cbmc/Pointer_Arithmetic9/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_Object_Type1/test.desc b/regression/cbmc/Pointer_Object_Type1/test.desc index d3aaf765740..17695a197ac 100644 --- a/regression/cbmc/Pointer_Object_Type1/test.desc +++ b/regression/cbmc/Pointer_Object_Type1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^SIGNAL=0$ ^EXIT=10$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer_array3/test.desc b/regression/cbmc/Pointer_array3/test.desc index 33c89987cc7..5984f379484 100644 --- a/regression/cbmc/Pointer_array3/test.desc +++ b/regression/cbmc/Pointer_array3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --no-assertions +--no-assertions ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index a8cdc81121f..13f1bafbdd8 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -1,6 +1,6 @@ CORE broken-cprover-smt-backend no-new-smt main.i ---bounds-check --32 --no-simplify +--32 --no-simplify ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 474026934fa..3215b675014 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -1,6 +1,6 @@ CORE main.i ---bounds-check --32 +--32 ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE diff --git a/regression/cbmc/Pointer_difference2/test.desc b/regression/cbmc/Pointer_difference2/test.desc index 36d9e01f3cf..7db4ff3ffd7 100644 --- a/regression/cbmc/Pointer_difference2/test.desc +++ b/regression/cbmc/Pointer_difference2/test.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend no-new-smt main.c ---pointer-check + ^\[main.assertion.1\] line 6 correct: SUCCESS ^\[main.pointer.1\] line 8 same object violation in array - other_array: FAILURE$ ^\[main.assertion.2\] line 11 undefined behavior: FAILURE$ diff --git a/regression/cbmc/Recursion2/test.desc b/regression/cbmc/Recursion2/test.desc index 4a9104162ed..e21095fda9d 100644 --- a/regression/cbmc/Recursion2/test.desc +++ b/regression/cbmc/Recursion2/test.desc @@ -1,6 +1,6 @@ CORE main.c - --unwind 11 +--unwind 11 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Sideeffects5/test.desc b/regression/cbmc/Sideeffects5/test.desc index e69488b2e66..33900ad2b78 100644 --- a/regression/cbmc/Sideeffects5/test.desc +++ b/regression/cbmc/Sideeffects5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---div-by-zero-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Sideeffects6/test.desc b/regression/cbmc/Sideeffects6/test.desc index e69488b2e66..33900ad2b78 100644 --- a/regression/cbmc/Sideeffects6/test.desc +++ b/regression/cbmc/Sideeffects6/test.desc @@ -1,6 +1,6 @@ CORE main.c ---div-by-zero-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/Sideeffects8/test.desc b/regression/cbmc/Sideeffects8/test.desc index 565f30cc839..5e7633e5a19 100644 --- a/regression/cbmc/Sideeffects8/test.desc +++ b/regression/cbmc/Sideeffects8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/String1/test.desc b/regression/cbmc/String1/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/String1/test.desc +++ b/regression/cbmc/String1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String2/test.desc b/regression/cbmc/String2/test.desc index 4b9176a942e..6de79559914 100644 --- a/regression/cbmc/String2/test.desc +++ b/regression/cbmc/String2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/String3/test.desc b/regression/cbmc/String3/test.desc index e19d0a66341..e5f0568a0eb 100644 --- a/regression/cbmc/String3/test.desc +++ b/regression/cbmc/String3/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---pointer-check --bounds-check + ^EXIT=10$ ^SIGNAL=0$ ^Counterexample:$ diff --git a/regression/cbmc/String4/test.desc b/regression/cbmc/String4/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/String4/test.desc +++ b/regression/cbmc/String4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String5/test.desc b/regression/cbmc/String5/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/String5/test.desc +++ b/regression/cbmc/String5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String7/test.desc b/regression/cbmc/String7/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/String7/test.desc +++ b/regression/cbmc/String7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String8/test.desc b/regression/cbmc/String8/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/String8/test.desc +++ b/regression/cbmc/String8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction1/test.desc b/regression/cbmc/String_Abstraction1/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction1/test.desc +++ b/regression/cbmc/String_Abstraction1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction10/test.desc b/regression/cbmc/String_Abstraction10/test.desc index 72eb0a670e6..d449253e7f0 100644 --- a/regression/cbmc/String_Abstraction10/test.desc +++ b/regression/cbmc/String_Abstraction10/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction2/test.desc b/regression/cbmc/String_Abstraction2/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction2/test.desc +++ b/regression/cbmc/String_Abstraction2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction23/test.desc b/regression/cbmc/String_Abstraction23/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction23/test.desc +++ b/regression/cbmc/String_Abstraction23/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction3/test.desc b/regression/cbmc/String_Abstraction3/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction3/test.desc +++ b/regression/cbmc/String_Abstraction3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction4/test.desc b/regression/cbmc/String_Abstraction4/test.desc index 4beaf5352c1..ca468cf5a61 100644 --- a/regression/cbmc/String_Abstraction4/test.desc +++ b/regression/cbmc/String_Abstraction4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/String_Abstraction5/test.desc b/regression/cbmc/String_Abstraction5/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction5/test.desc +++ b/regression/cbmc/String_Abstraction5/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction6/test.desc b/regression/cbmc/String_Abstraction6/test.desc index a8058d6d1e4..e6f36bad003 100644 --- a/regression/cbmc/String_Abstraction6/test.desc +++ b/regression/cbmc/String_Abstraction6/test.desc @@ -1,6 +1,6 @@ KNOWNBUG main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction7/test.desc b/regression/cbmc/String_Abstraction7/test.desc index 4d28a11df24..500d141fdec 100644 --- a/regression/cbmc/String_Abstraction7/test.desc +++ b/regression/cbmc/String_Abstraction7/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction8/test.desc b/regression/cbmc/String_Abstraction8/test.desc index c9b7d9f6ff4..327468f4725 100644 --- a/regression/cbmc/String_Abstraction8/test.desc +++ b/regression/cbmc/String_Abstraction8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --unwind 5 --pointer-check --bounds-check +--string-abstraction --unwind 5 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction9/test.desc b/regression/cbmc/String_Abstraction9/test.desc index e6fb3bba609..f3145b289ad 100644 --- a/regression/cbmc/String_Abstraction9/test.desc +++ b/regression/cbmc/String_Abstraction9/test.desc @@ -1,6 +1,6 @@ CORE main.c ---string-abstraction --pointer-check --bounds-check +--string-abstraction ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Struct_Pointer2/test.desc b/regression/cbmc/Struct_Pointer2/test.desc index 39c491ba8bb..9efefbc7362 100644 --- a/regression/cbmc/Struct_Pointer2/test.desc +++ b/regression/cbmc/Struct_Pointer2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index 06417908cee..fdc14ee5bb3 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/regression/cbmc/Undefined_Shift1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---undefined-shift-check + ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 4 shift operand is negative in .*: SUCCESS$ diff --git a/regression/cbmc/pointer-check-01/test.desc b/regression/cbmc/pointer-check-01/test.desc index f86851a0aa1..de728102aaa 100644 --- a/regression/cbmc/pointer-check-01/test.desc +++ b/regression/cbmc/pointer-check-01/test.desc @@ -1,6 +1,6 @@ CORE test.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-check-02/test.desc b/regression/cbmc/pointer-check-02/test.desc index 2e0645ee56a..3620f08a75b 100644 --- a/regression/cbmc/pointer-check-02/test.desc +++ b/regression/cbmc/pointer-check-02/test.desc @@ -1,6 +1,6 @@ CORE test.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index b793e876bf8..03bece93ba2 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/regression/cbmc/pointer-extra-checks/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main.pointer_dereference.1\] .* dereference failure: pointer NULL in \*p: FAILURE$ diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc index 7b82cc87646..e92915867f1 100644 --- a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc index 716670ff6f7..23245bb4bae 100644 --- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc index 7b82cc87646..e92915867f1 100644 --- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc +++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc @@ -1,6 +1,6 @@ CORE main.c ---function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check +--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index fb52df0c4de..ec4382d528b 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/regression/cbmc/pointer-primitive-check-01/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^EXIT=10$ ^SIGNAL=0$ \[main.pointer_primitives.\d+\] line \d+ pointer invalid in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): FAILURE diff --git a/regression/cbmc/pointer-primitive-check-02/test.desc b/regression/cbmc/pointer-primitive-check-02/test.desc index 315e2d255c7..2a8b2dfc804 100644 --- a/regression/cbmc/pointer-primitive-check-02/test.desc +++ b/regression/cbmc/pointer-primitive-check-02/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc index 3c9f2d5f074..ebd94b82416 100644 --- a/regression/cbmc/pointer-primitive-check-04/test.desc +++ b/regression/cbmc/pointer-primitive-check-04/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^EXIT=10$ ^SIGNAL=0$ \[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(p, .*1\): FAILURE diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 487a7c80d7b..e9aebd82921 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---signed-overflow-check --bounds-check + line 14 array 'y' upper bound in y\[(\(signed long( long)? int\))?1\]: FAILURE$ ^\*\* 1 of 1 failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc index fc1f888dfcf..5ea4e565aeb 100644 --- a/regression/cbmc/pragma_cprover2/test.desc +++ b/regression/cbmc/pragma_cprover2/test.desc @@ -1,9 +1,9 @@ CORE main.c ---signed-overflow-check + ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$ ^\[main.overflow\.2\] line 22 arithmetic overflow on signed \+ in x \+ n: FAILURE$ -^\*\* 2 of 2 failed +^\*\* 2 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover3/test.desc b/regression/cbmc/pragma_cprover3/test.desc index c7e1faaa966..32bad9c99cf 100644 --- a/regression/cbmc/pragma_cprover3/test.desc +++ b/regression/cbmc/pragma_cprover3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^main.c function main$ ^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ diff --git a/regression/cbmc/pragma_cprover_enable1/test.desc b/regression/cbmc/pragma_cprover_enable1/test.desc index 8113775430e..2e62973ed17 100644 --- a/regression/cbmc/pragma_cprover_enable1/test.desc +++ b/regression/cbmc/pragma_cprover_enable1/test.desc @@ -3,7 +3,7 @@ main.c ^\[main\.array_bounds\.1\] line \d+ array 'y' upper bound.*FAILURE$ ^\[main\.overflow\.1\] line \d+ arithmetic overflow on signed.*FAILURE$ -^\*\* 2 of 2 failed +^\*\* 2 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover_enable2/test.desc b/regression/cbmc/pragma_cprover_enable2/test.desc index 9ddbded4bb7..22b756e21c8 100644 --- a/regression/cbmc/pragma_cprover_enable2/test.desc +++ b/regression/cbmc/pragma_cprover_enable2/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ ^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ ^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$ -^\*\* 5 of 5 failed +^\*\* 5 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc index da404977532..2b59ea8ab11 100644 --- a/regression/cbmc/pragma_cprover_enable_all/test.desc +++ b/regression/cbmc/pragma_cprover_enable_all/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check +--object-bits 8 --enum-range-check --unsigned-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --nan-check ^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc index 9e72ed21ec6..05a374a7ff8 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^main.c function main$ ^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ diff --git a/regression/cbmc/r_w_ok10/test.desc b/regression/cbmc/r_w_ok10/test.desc index 54479c1b6d3..7fe3f0ce2d4 100644 --- a/regression/cbmc/r_w_ok10/test.desc +++ b/regression/cbmc/r_w_ok10/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-primitive-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main.pointer_primitives.\d+\] line 7 pointer invalid in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$ diff --git a/regression/cbmc/return5/test.desc b/regression/cbmc/return5/test.desc index 7c84befca17..df2241a3a99 100644 --- a/regression/cbmc/return5/test.desc +++ b/regression/cbmc/return5/test.desc @@ -1,6 +1,6 @@ CORE main.c - --unwind 2 +--unwind 2 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/return9/test.desc b/regression/cbmc/return9/test.desc index 25ff2f70a34..14c62697987 100644 --- a/regression/cbmc/return9/test.desc +++ b/regression/cbmc/return9/test.desc @@ -1,6 +1,6 @@ CORE tcas_v23_523.c ---bounds-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/set-property-inline1/test.desc b/regression/cbmc/set-property-inline1/test.desc index de76ddc5e98..7c739b4c4f7 100644 --- a/regression/cbmc/set-property-inline1/test.desc +++ b/regression/cbmc/set-property-inline1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---property inc.overflow.1 --property inc.overflow.2 --slice-formula --signed-overflow-check --conversion-check +--property inc.overflow.1 --property inc.overflow.2 --slice-formula --conversion-check ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED diff --git a/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc b/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc index 1b37eefb313..d2869403138 100644 --- a/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc +++ b/regression/cbmc/short_circuit_implies/short-circuit-memory-checks.desc @@ -1,6 +1,6 @@ CORE short-circuit-memory-checks.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ line 11 dereference failure: pointer NULL in \*c: SUCCESS diff --git a/regression/cbmc/show_properties1/test.desc b/regression/cbmc/show_properties1/test.desc index 96b4816a1fb..58455c49f0e 100644 --- a/regression/cbmc/show_properties1/test.desc +++ b/regression/cbmc/show_properties1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --show-properties +--show-properties ^EXIT=0$ ^SIGNAL=0$ ^Property foo.pointer_dereference.1:$ diff --git a/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc b/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc index c49d9b15bdb..4825105bf3e 100644 --- a/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc +++ b/regression/cbmc/simplify_singleton_interval_7690/negative_test.desc @@ -1,6 +1,6 @@ CORE ---trace singleton_interval_simp_neg.c +--trace ^VERIFICATION FAILED$ ^\[main\.assertion\.1\] line \d expected failure: paths where x is unbounded explored: FAILURE$ ^\[main\.assertion\.2\] line \d+ expected failure: paths where 0 \<= x \<= 15 explored: FAILURE$ diff --git a/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc b/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc index 651633ec466..ac1e5eb265f 100644 --- a/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc +++ b/regression/cbmc/simplify_singleton_interval_7690/positive_test.desc @@ -1,6 +1,6 @@ CORE ---trace singleton_interval_simp.c +--trace ^VERIFICATION FAILED$ ^\[main\.assertion\.1\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ ^\[main\.assertion\.2\] line \d+ expected failure: only paths where x == 15 explored: FAILURE$ diff --git a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc index c7b20b1fa7a..eb0dc3a26cc 100644 --- a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc +++ b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc @@ -1,6 +1,6 @@ CORE smt-backend singleton_interval_in_assume_7690.c ---pointer-check + ^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed( long( long)?)? int\)stk-\>top\]: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/struct12/test.desc b/regression/cbmc/struct12/test.desc index d678193e09e..baa5be87a7f 100644 --- a/regression/cbmc/struct12/test.desc +++ b/regression/cbmc/struct12/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc index da239c1965b..9efefbc7362 100644 --- a/regression/cbmc/struct6/test.desc +++ b/regression/cbmc/struct6/test.desc @@ -1,6 +1,6 @@ CORE main.c ---bounds-check --pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc index 96c9b4bcd7b..9efefbc7362 100644 --- a/regression/cbmc/struct7/test.desc +++ b/regression/cbmc/struct7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/switch8/program-only.desc b/regression/cbmc/switch8/program-only.desc index 15885c2d7e5..4c387ea1733 100644 --- a/regression/cbmc/switch8/program-only.desc +++ b/regression/cbmc/switch8/program-only.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --program-only +--program-only ^EXIT=0$ ^SIGNAL=0$ a!0@1#2 == 0$ diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc index 62e8b9730ae..f054d2889bc 100644 --- a/regression/cbmc/switch8/test.desc +++ b/regression/cbmc/switch8/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.1\] line 11 assertion 0: SUCCESS$ diff --git a/regression/cbmc/switch9/test.desc b/regression/cbmc/switch9/test.desc index 8438cf07aac..388e216cca0 100644 --- a/regression/cbmc/switch9/test.desc +++ b/regression/cbmc/switch9/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check --malloc-may-fail --malloc-fail-null +--malloc-may-fail --malloc-fail-null activate-multi-line-match ^\[main.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*p: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/unsigned___int128/test.desc b/regression/cbmc/unsigned___int128/test.desc index 67b0294bc90..2671302be7c 100644 --- a/regression/cbmc/unsigned___int128/test.desc +++ b/regression/cbmc/unsigned___int128/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unsigned-overflow-check --signed-overflow-check --function reduce +--unsigned-overflow-check --function reduce ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/void_pointer1/test.desc b/regression/cbmc/void_pointer1/test.desc index d5e386bad9a..83b8819429a 100644 --- a/regression/cbmc/void_pointer1/test.desc +++ b/regression/cbmc/void_pointer1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc index 6daabc695da..6ab9ab2fc56 100644 --- a/regression/cbmc/void_pointer2/test.desc +++ b/regression/cbmc/void_pointer2/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c ---pointer-check --no-simplify --unwind 3 +--no-simplify --unwind 3 ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/void_pointer6/test.desc b/regression/cbmc/void_pointer6/test.desc index 503df2ca2a0..16b577369e5 100644 --- a/regression/cbmc/void_pointer6/test.desc +++ b/regression/cbmc/void_pointer6/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/void_pointer7/test.desc b/regression/cbmc/void_pointer7/test.desc index 3db12932134..c3f30ba1925 100644 --- a/regression/cbmc/void_pointer7/test.desc +++ b/regression/cbmc/void_pointer7/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ From 47631b86372a17d4a578e5ef47230f642639966c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 23 Nov 2023 16:59:40 +0000 Subject: [PATCH 5/8] Change flags to no- variant in goto_check --- src/ansi-c/goto_check_c.h | 10 +++++----- src/cbmc/cbmc_parse_options.cpp | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h index 85c921cd6b4..5e2a2dacbf5 100644 --- a/src/ansi-c/goto_check_c.h +++ b/src/ansi-c/goto_check_c.h @@ -38,12 +38,12 @@ void goto_check_c( message_handlert &message_handler); #define OPT_GOTO_CHECK \ - "(no-bounds-check)(pointer-check)(memory-leak-check)(memory-cleanup-check)" \ - "(div-by-zero-check)(enum-range-check)" \ - "(signed-overflow-check)(unsigned-overflow-check)" \ - "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ + "(no-bounds-check)(no-pointer-check)(memory-leak-check)(memory-cleanup-check)" \ + "(no-div-by-zero-check)(enum-range-check)" \ + "(no-signed-overflow-check)(unsigned-overflow-check)" \ + "(pointer-overflow-check)(conversion-check)(no-undefined-shift-check)" \ "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ - "(pointer-primitive-check)" \ + "(no-pointer-primitive-check)" \ "(retain-trivial-checks)" \ "(error-label):" \ "(no-assertions)(no-assumptions)" \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 0065e512b43..616daaa9e69 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -326,8 +326,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // (expected checks and no unsoundness by missing checks). if (!cmdline.isset("no-standard-checks") && options.get_bool_option("standard-checks")) set_default_analysis_flags(options); - else - PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options); + + PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options); // all (non-default) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); From 1256695995882ac523b1fa65ee9d092166aff5ae Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 29 Nov 2023 11:19:24 +0000 Subject: [PATCH 6/8] Override defaults flags only if default flags have been set --- src/cbmc/cbmc_parse_options.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 616daaa9e69..3c0003a8d2b 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -325,10 +325,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) // Enable flags that in combination provide analysis with no surprises // (expected checks and no unsoundness by missing checks). if (!cmdline.isset("no-standard-checks") && options.get_bool_option("standard-checks")) + { set_default_analysis_flags(options); - - PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options); - + PARSE_OPTIONS_GOTO_CHECK_DEFAULTS_OVERRIDE(cmdline, options); + } + // all (non-default) checks supported by goto_check PARSE_OPTIONS_GOTO_CHECK(cmdline, options); From f7a9d37c1c1bb8fc0576f70cb82b008e692338f1 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 29 Nov 2023 11:19:42 +0000 Subject: [PATCH 7/8] More tests adjusted --- regression/cbmc/Float-div2/test.desc | 2 +- regression/cbmc/Float-div3/test.desc | 2 +- regression/cbmc/Float-flags-simp1/test.desc | 2 +- regression/cbmc/Malloc11/test.desc | 2 +- regression/cbmc/Pointer29/test.desc | 2 +- regression/cbmc/Pointer_byte_extract2/test.desc | 2 +- .../cbmc/Pointer_byte_extract5/no-simplify.desc | 2 +- regression/cbmc/Pointer_comparison3/test.desc | 2 +- .../cbmc/Pointer_difference1/no-simplify.desc | 2 +- regression/cbmc/Pointer_difference1/test.desc | 2 +- regression/cbmc/Pointer_difference2/test.desc | 2 +- regression/cbmc/Quantifiers-assertion/test.desc | 2 +- regression/cbmc/Quantifiers-assignment/test.desc | 2 +- regression/cbmc/Quantifiers-copy/test.desc | 2 +- regression/cbmc/Quantifiers-if/test.desc | 2 +- .../cbmc/Quantifiers-initialisation/test.desc | 2 +- .../cbmc/Quantifiers-initialisation2/test.desc | 2 +- .../cbmc/Quantifiers-not-exists/fixed.desc | 2 +- regression/cbmc/Quantifiers-not/test.desc | 2 +- .../Quantifiers-two-dimension-array/fixed.desc | 2 +- .../Quantifiers-two-dimension-array/test.desc | 2 +- regression/cbmc/String_Abstraction11/test.desc | 2 +- regression/cbmc/String_Abstraction15/test.desc | 2 +- regression/cbmc/String_Abstraction19/test.desc | 2 +- regression/cbmc/Unbounded_Array5/test.desc | 2 +- regression/cbmc/Undefined_Shift1/test.desc | 2 +- regression/cbmc/__builtin_clz-01/big-endian.desc | 2 +- regression/cbmc/__builtin_clz-01/test.desc | 2 +- regression/cbmc/__builtin_ctz-01/big-endian.desc | 2 +- regression/cbmc/__builtin_ctz-01/test.desc | 2 +- regression/cbmc/__builtin_ffs-01/big-endian.desc | 2 +- regression/cbmc/__builtin_ffs-01/test.desc | 2 +- .../cbmc/address_space_size_limit3/test.desc | 2 +- regression/cbmc/argc-and-argv/argc1.desc | 2 +- regression/cbmc/argc-and-argv/argv1.desc | 2 +- regression/cbmc/array-bug-6230/test.desc | 2 +- .../array-cell-sensitivity1/test_execution.desc | 2 +- .../array-cell-sensitivity2/test_execution.desc | 2 +- .../array-cell-sensitivity4/test_execution.desc | 2 +- .../array-cell-sensitivity5/test_execution.desc | 2 +- .../array-cell-sensitivity6/test_execution.desc | 2 +- .../array-cell-sensitivity9/test_execution.desc | 2 +- .../cbmc/array-function-parameters/test.desc | 2 +- regression/cbmc/array_constraints1/test.desc | 4 ++-- regression/cbmc/atomic_X_fetch-1/test.desc | 2 +- regression/cbmc/atomic_fetch_X-1/test.desc | 2 +- .../cbmc/aws-byte-buf-regression/test.desc | 2 +- regression/cbmc/bounds_check1/test.desc | 2 +- regression/cbmc/bounds_check2/test.desc | 2 +- regression/cbmc/byte_update11/test.desc | 2 +- .../test-no-failed-assertions.desc | 2 +- .../cbmc/cover-failed-assertions/test.desc | 2 +- regression/cbmc/coverage_report2/test.desc | 2 +- .../cbmc/destructors/compound_literal.desc | 2 +- regression/cbmc/dynamic_size1/stack_object.desc | 2 +- regression/cbmc/dynamic_size1/test.desc | 2 +- regression/cbmc/empty_compound_type1/test.desc | 2 +- regression/cbmc/empty_compound_type2/test.desc | 2 +- .../cbmc/equality_through_array6/test.desc | 2 +- .../exported.symex.ready.goto | Bin 0 -> 7889 bytes .../fault_localization-stop_on_fail1/test.desc | 2 +- regression/cbmc/field-sensitivity14/test.desc | 2 +- regression/cbmc/fmod1/test.desc | 2 +- regression/cbmc/function_option1/test.desc | 2 +- .../cbmc/gcc_builtin_sub_overflow/simplify.desc | 2 +- regression/cbmc/gcc_vector1/test.desc | 2 +- regression/cbmc/graphml_witness2/test.desc | 2 +- regression/cbmc/guard1/test.desc | 2 +- regression/cbmc/havoc_object1/full-slice.desc | 2 +- regression/cbmc/havoc_object1/test.desc | 2 +- regression/cbmc/if1/test.desc | 2 +- regression/cbmc/link_json_symtabs/test.desc | 2 +- regression/cbmc/locations1/test.desc | 2 +- regression/cbmc/member1/test.desc | 2 +- regression/cbmc/memory_allocation1/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 4 ++-- regression/cbmc/memset3/test.desc | 2 +- regression/cbmc/mm_io1/test.desc | 2 +- regression/cbmc/multiple-goto-traces/test.desc | 2 +- regression/cbmc/null7/test.desc | 2 +- .../cbmc/overflow/leftshift_overflow-c89.desc | 4 ++-- .../leftshift_overflow-c99-full-slice.desc | 4 ++-- .../cbmc/overflow/leftshift_overflow-c99.desc | 4 ++-- regression/cbmc/overflow/mod_overflow.desc | 2 +- .../cbmc/overflow/signed_addition_overflow1.desc | 2 +- .../cbmc/overflow/signed_addition_overflow2.desc | 2 +- .../cbmc/overflow/signed_addition_overflow3.desc | 2 +- .../cbmc/overflow/signed_addition_overflow4.desc | 2 +- .../cbmc/overflow/signed_multiplication1.desc | 2 +- .../cbmc/overflow/signed_subtraction1.desc | 2 +- .../cbmc/overflow/unary_minus_overflow.desc | 2 +- regression/cbmc/path-per-path-vccs/test.desc | 2 +- .../cbmc/pointer-predicates/at_bounds1.desc | 2 +- regression/cbmc/points-to-sets/test_json.desc | 2 +- regression/cbmc/pragma_cprover_enable2/test.desc | 4 +++- regression/cbmc/pragma_cprover_enable3/test.desc | 2 +- .../test.desc | 2 +- regression/cbmc/r_w_ok1/test.desc | 2 +- regression/cbmc/r_w_ok10/test.desc | 2 +- regression/cbmc/runtime-profiling/test.desc | 2 +- regression/cbmc/scanf1/big-endian.desc | 2 +- regression/cbmc/scanf1/test.desc | 2 +- regression/cbmc/simplify-union/test.desc | 2 +- regression/cbmc/sync_X_and_fetch-1/test.desc | 2 +- regression/cbmc/sync_fetch_and_X-1/test.desc | 2 +- regression/cbmc/sync_lock_release-1/test.desc | 2 +- regression/cbmc/uniform_array1/test.desc | 2 +- regression/cbmc/union12/test.desc | 4 ++-- regression/cbmc/union17/test.desc | 2 +- regression/cbmc/unwind_counters4/test.desc | 2 +- regression/cbmc/void_pointer3/test.desc | 2 +- 111 files changed, 118 insertions(+), 116 deletions(-) create mode 100644 regression/cbmc/export-symex-ready-goto/exported.symex.ready.goto diff --git a/regression/cbmc/Float-div2/test.desc b/regression/cbmc/Float-div2/test.desc index 9e28fc5f807..8afef949891 100644 --- a/regression/cbmc/Float-div2/test.desc +++ b/regression/cbmc/Float-div2/test.desc @@ -1,6 +1,6 @@ CORE broken-z3-smt-backend no-new-smt main.c ---floatbv +--floatbv --no-built-in-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc index 9e28fc5f807..8afef949891 100644 --- a/regression/cbmc/Float-div3/test.desc +++ b/regression/cbmc/Float-div3/test.desc @@ -1,6 +1,6 @@ CORE broken-z3-smt-backend no-new-smt main.c ---floatbv +--floatbv --no-built-in-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Float-flags-simp1/test.desc b/regression/cbmc/Float-flags-simp1/test.desc index ccfe3848438..f400518065f 100644 --- a/regression/cbmc/Float-flags-simp1/test.desc +++ b/regression/cbmc/Float-flags-simp1/test.desc @@ -1,6 +1,6 @@ CORE broken-cprover-smt-backend no-new-smt main.c ---floatbv +--floatbv --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Malloc11/test.desc b/regression/cbmc/Malloc11/test.desc index 7561cd38b9b..9c96469df12 100644 --- a/regression/cbmc/Malloc11/test.desc +++ b/regression/cbmc/Malloc11/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer29/test.desc b/regression/cbmc/Pointer29/test.desc index 9efefbc7362..73e23b3765b 100644 --- a/regression/cbmc/Pointer29/test.desc +++ b/regression/cbmc/Pointer29/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-pointer-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc index eb98d4f78ba..c89ed785b59 100644 --- a/regression/cbmc/Pointer_byte_extract2/test.desc +++ b/regression/cbmc/Pointer_byte_extract2/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] .*: FAILURE$ -^\*\* 1 of 2 failed +^\*\* 2 of 4 failed -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index 13f1bafbdd8..26f5df4cdf1 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed +\*\* 1 of \d+ failed -- ^warning: ignoring -- diff --git a/regression/cbmc/Pointer_comparison3/test.desc b/regression/cbmc/Pointer_comparison3/test.desc index 4076451d3f7..a2e9b218a8c 100644 --- a/regression/cbmc/Pointer_comparison3/test.desc +++ b/regression/cbmc/Pointer_comparison3/test.desc @@ -3,7 +3,7 @@ main.c ^\[main.assertion.3\] line 21 always false for different objects: FAILURE$ ^\[main.assertion.4\] line 23 always false for different objects: FAILURE$ -^\*\* 2 of 7 failed +^\*\* 11 of 59 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer_difference1/no-simplify.desc b/regression/cbmc/Pointer_difference1/no-simplify.desc index 2d4a398e23a..1093c705750 100644 --- a/regression/cbmc/Pointer_difference1/no-simplify.desc +++ b/regression/cbmc/Pointer_difference1/no-simplify.desc @@ -1,6 +1,6 @@ CORE main.c ---no-simplify +--no-simplify --no-standard-checks VERIFICATION SUCCESSFUL ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Pointer_difference1/test.desc b/regression/cbmc/Pointer_difference1/test.desc index 466da18b2b5..1909295d022 100644 --- a/regression/cbmc/Pointer_difference1/test.desc +++ b/regression/cbmc/Pointer_difference1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/Pointer_difference2/test.desc b/regression/cbmc/Pointer_difference2/test.desc index 7db4ff3ffd7..9d993bd4dd6 100644 --- a/regression/cbmc/Pointer_difference2/test.desc +++ b/regression/cbmc/Pointer_difference2/test.desc @@ -9,7 +9,7 @@ main.c ^\[main.pointer_arithmetic.\d+\] line 26 pointer relation: pointer outside object bounds in p: FAILURE$ ^\[main.assertion.8\] line 28 end plus 2 is nondet: FAILURE$ ^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$ -^\*\* 7 of \d+ failed +^\*\* 9 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc index 17a23b4628e..b0258159753 100644 --- a/regression/cbmc/Quantifiers-assertion/test.desc +++ b/regression/cbmc/Quantifiers-assertion/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.assertion.4\] .* NotExists-Forall: failed: FAILURE$ ^\[main.assertion.5\] .* NotForall-Forall: successful: SUCCESS$ ^\[main.assertion.6\] .* NotForall-NotForall: successful: SUCCESS$ -^\*\* 3 of 6 failed +^\*\* 3 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc index 2c0b0b3ae32..c7c725c2405 100644 --- a/regression/cbmc/Quantifiers-assignment/test.desc +++ b/regression/cbmc/Quantifiers-assignment/test.desc @@ -6,7 +6,7 @@ main.c ^\[main.assertion.2\] .* assertion y: FAILURE$ ^\[main.assertion.3\] .* assertion z1: SUCCESS$ ^\[main.assertion.4\] .* assertion z2: SUCCESS$ -^\*\* 1 of 4 failed +^\*\* 1 of 20 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc index ad846a8f439..8733c27e61e 100644 --- a/regression/cbmc/Quantifiers-copy/test.desc +++ b/regression/cbmc/Quantifiers-copy/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] .* assertion b\[.*\] == 2: SUCCESS$ ^\[main.assertion.4\] .* assertion b\[.*\] == 3: SUCCESS$ ^\[main.assertion.5\] .* assertion b\[.*\] == 4: SUCCESS$ -^\*\* 0 of 5 failed +^\*\* 0 of 9 failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc index d61553a444f..49b42b06acc 100644 --- a/regression/cbmc/Quantifiers-if/test.desc +++ b/regression/cbmc/Quantifiers-if/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] .* success 1: SUCCESS$ ^\[main.assertion.4\] .* failure 3: FAILURE$ ^\[main.assertion.5\] .* success 2: SUCCESS$ -^\*\* 3 of 5 failed +^\*\* 3 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc index 672fa68090d..c9ae3fccbbb 100644 --- a/regression/cbmc/Quantifiers-initialisation/test.desc +++ b/regression/cbmc/Quantifiers-initialisation/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] .* assertion a\[.*\] == 3: SUCCESS$ ^\[main.assertion.4\] .* assertion a\[.*\] == 4: SUCCESS$ ^\[main.assertion.5\] .* assertion a\[.*\] == 5: SUCCESS$ -^\*\* 0 of 5 failed +^\*\* 0 of \d+ failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc index 82af7c648f3..4dd895be373 100644 --- a/regression/cbmc/Quantifiers-initialisation2/test.desc +++ b/regression/cbmc/Quantifiers-initialisation2/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] .* assertion a\[.*\] > a\[.*\]: FAILURE$ ^\[main.assertion.4\] .* forall c\[\]: SUCCESS$ ^\[main.assertion.5\] .* assertion c\[.*\] >= c\[.*\]: SUCCESS$ -^\*\* 1 of 5 failed +^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.desc b/regression/cbmc/Quantifiers-not-exists/fixed.desc index c0c0c8aaa2b..6a614b091d3 100644 --- a/regression/cbmc/Quantifiers-not-exists/fixed.desc +++ b/regression/cbmc/Quantifiers-not-exists/fixed.desc @@ -8,7 +8,7 @@ fixed.c ^\[main.assertion.8\] line 36 assertion .*: SUCCESS$ ^\[main.assertion.9\] line 38 assertion .*: SUCCESS$ ^\[main.assertion.10\] line 39 assertion .*: SUCCESS$ -^\*\* 4 of 10 failed +^\*\* 4 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc index f930deb9f8a..e3757edc8a1 100644 --- a/regression/cbmc/Quantifiers-not/test.desc +++ b/regression/cbmc/Quantifiers-not/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] .* failure 1: FAILURE$ ^\[main.assertion.4\] .* success 3: SUCCESS$ ^\[main.assertion.5\] .* failure 2: FAILURE$ -^\*\* 2 of 5 failed +^\*\* 2 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc b/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc index a39cee20077..a046794fb66 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc @@ -7,7 +7,7 @@ fixed.c ^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$ ^\[main.assertion.5\] line 18 assertion .*: SUCCESS$ -^\*\* 0 of 5 failed +^\*\* 0 of \d+ failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 5b8451664ce..875b7b3d0e1 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$ ^\[main.assertion.5\] line 16 assertion .*: FAILURE$ -^\*\* 1 of 5 failed +^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/String_Abstraction11/test.desc b/regression/cbmc/String_Abstraction11/test.desc index e21815b93e7..14aaf2bc0ba 100644 --- a/regression/cbmc/String_Abstraction11/test.desc +++ b/regression/cbmc/String_Abstraction11/test.desc @@ -1,6 +1,6 @@ CORE anon-retval.c ---string-abstraction +--string-abstraction --no-pointer-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction15/test.desc b/regression/cbmc/String_Abstraction15/test.desc index d7fa5b8d070..2911f71a220 100644 --- a/regression/cbmc/String_Abstraction15/test.desc +++ b/regression/cbmc/String_Abstraction15/test.desc @@ -1,6 +1,6 @@ CORE pass-in.c ---string-abstraction +--string-abstraction --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/String_Abstraction19/test.desc b/regression/cbmc/String_Abstraction19/test.desc index 456949ab85b..788f304b972 100644 --- a/regression/cbmc/String_Abstraction19/test.desc +++ b/regression/cbmc/String_Abstraction19/test.desc @@ -1,6 +1,6 @@ CORE structs.c ---string-abstraction +--string-abstraction --no-pointer-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Unbounded_Array5/test.desc b/regression/cbmc/Unbounded_Array5/test.desc index 9c96469df12..9b782e2bb19 100644 --- a/regression/cbmc/Unbounded_Array5/test.desc +++ b/regression/cbmc/Unbounded_Array5/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index fdc14ee5bb3..5fe4951916b 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/regression/cbmc/Undefined_Shift1/test.desc @@ -9,7 +9,7 @@ main.c ^\[.*\] line 15 shift distance is negative in .*: FAILURE$ ^\[.*\] line 15 shift distance too large in .*: SUCCESS$ ^\[.*\] line 20 shift operand is negative in .*: FAILURE$ -^\*\* 3 of 6 failed +^\*\* 4 of 9 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/__builtin_clz-01/big-endian.desc b/regression/cbmc/__builtin_clz-01/big-endian.desc index 8fce3084303..10628c7cb4c 100644 --- a/regression/cbmc/__builtin_clz-01/big-endian.desc +++ b/regression/cbmc/__builtin_clz-01/big-endian.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---bounds-check --big-endian +--big-endian ^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$ ^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/__builtin_clz-01/test.desc b/regression/cbmc/__builtin_clz-01/test.desc index 335b9f6beca..e6b6f54a4e0 100644 --- a/regression/cbmc/__builtin_clz-01/test.desc +++ b/regression/cbmc/__builtin_clz-01/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---bounds-check + ^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$ ^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/__builtin_ctz-01/big-endian.desc b/regression/cbmc/__builtin_ctz-01/big-endian.desc index 3251ca19026..efe145a3671 100644 --- a/regression/cbmc/__builtin_ctz-01/big-endian.desc +++ b/regression/cbmc/__builtin_ctz-01/big-endian.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---bounds-check --big-endian +--big-endian ^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$ ^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$ ^\*\* 1 of \d+ failed diff --git a/regression/cbmc/__builtin_ctz-01/test.desc b/regression/cbmc/__builtin_ctz-01/test.desc index 7b8ccbf8e26..c1ef9001580 100644 --- a/regression/cbmc/__builtin_ctz-01/test.desc +++ b/regression/cbmc/__builtin_ctz-01/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---bounds-check + ^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$ ^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$ ^\*\* 1 of \d+ failed diff --git a/regression/cbmc/__builtin_ffs-01/big-endian.desc b/regression/cbmc/__builtin_ffs-01/big-endian.desc index 1e0a706ecec..bdf75a8ae10 100644 --- a/regression/cbmc/__builtin_ffs-01/big-endian.desc +++ b/regression/cbmc/__builtin_ffs-01/big-endian.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check --bounds-check --big-endian +--big-endian ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/__builtin_ffs-01/test.desc b/regression/cbmc/__builtin_ffs-01/test.desc index 032c2879b43..1c039664a91 100644 --- a/regression/cbmc/__builtin_ffs-01/test.desc +++ b/regression/cbmc/__builtin_ffs-01/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check --bounds-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc index 8aaae24a492..1c6ab14d1cf 100644 --- a/regression/cbmc/address_space_size_limit3/test.desc +++ b/regression/cbmc/address_space_size_limit3/test.desc @@ -1,6 +1,6 @@ CORE thorough-smt-backend no-new-smt main.i ---32 --little-endian --object-bits 26 --pointer-check +--32 --little-endian --object-bits 26 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/argc-and-argv/argc1.desc b/regression/cbmc/argc-and-argv/argc1.desc index 5f6348ffbe0..10b513412bf 100644 --- a/regression/cbmc/argc-and-argv/argc1.desc +++ b/regression/cbmc/argc-and-argv/argc1.desc @@ -1,6 +1,6 @@ CORE argc1.c ---bounds-check --pointer-check --unwind 0 +--unwind 0 ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line .* dereference failure: pointer outside object bounds in argv\[.*n\]: FAILURE$ diff --git a/regression/cbmc/argc-and-argv/argv1.desc b/regression/cbmc/argc-and-argv/argv1.desc index 1f379687b2b..47303fff42a 100644 --- a/regression/cbmc/argc-and-argv/argv1.desc +++ b/regression/cbmc/argc-and-argv/argv1.desc @@ -1,6 +1,6 @@ CORE argv1.c ---bounds-check --pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-bug-6230/test.desc b/regression/cbmc/array-bug-6230/test.desc index e7f5fdc04e1..34d33a342a4 100644 --- a/regression/cbmc/array-bug-6230/test.desc +++ b/regression/cbmc/array-bug-6230/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---malloc-may-fail --malloc-fail-null --pointer-check +--malloc-may-fail --malloc-fail-null ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/array-cell-sensitivity1/test_execution.desc b/regression/cbmc/array-cell-sensitivity1/test_execution.desc index 9280dcb19be..edf471b2124 100644 --- a/regression/cbmc/array-cell-sensitivity1/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity1/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-bounds-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-cell-sensitivity2/test_execution.desc b/regression/cbmc/array-cell-sensitivity2/test_execution.desc index 9280dcb19be..edf471b2124 100644 --- a/regression/cbmc/array-cell-sensitivity2/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity2/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-bounds-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-cell-sensitivity4/test_execution.desc b/regression/cbmc/array-cell-sensitivity4/test_execution.desc index 9280dcb19be..edf471b2124 100644 --- a/regression/cbmc/array-cell-sensitivity4/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity4/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-bounds-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-cell-sensitivity5/test_execution.desc b/regression/cbmc/array-cell-sensitivity5/test_execution.desc index 9280dcb19be..3490296625f 100644 --- a/regression/cbmc/array-cell-sensitivity5/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity5/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-cell-sensitivity6/test_execution.desc b/regression/cbmc/array-cell-sensitivity6/test_execution.desc index 9280dcb19be..3490296625f 100644 --- a/regression/cbmc/array-cell-sensitivity6/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity6/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-pointer-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-cell-sensitivity9/test_execution.desc b/regression/cbmc/array-cell-sensitivity9/test_execution.desc index 9280dcb19be..edf471b2124 100644 --- a/regression/cbmc/array-cell-sensitivity9/test_execution.desc +++ b/regression/cbmc/array-cell-sensitivity9/test_execution.desc @@ -1,6 +1,6 @@ CORE test.c - +--no-bounds-check ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc index bcc19893964..35ae04f966f 100644 --- a/regression/cbmc/array-function-parameters/test.desc +++ b/regression/cbmc/array-function-parameters/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt test.c ---function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check +--function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 ^EXIT=10$ ^SIGNAL=0$ \[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 32573032d3b..a8b1e839570 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -1,9 +1,9 @@ CORE no-new-smt main.c ---unwind 2 --pointer-check +--unwind 2 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 14 +^\*\* 4 of \d+ -- ^warning: ignoring diff --git a/regression/cbmc/atomic_X_fetch-1/test.desc b/regression/cbmc/atomic_X_fetch-1/test.desc index 27a28993ba5..1a10ff50301 100644 --- a/regression/cbmc/atomic_X_fetch-1/test.desc +++ b/regression/cbmc/atomic_X_fetch-1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/atomic_fetch_X-1/test.desc b/regression/cbmc/atomic_fetch_X-1/test.desc index 854a0a8ec12..1666360e744 100644 --- a/regression/cbmc/atomic_fetch_X-1/test.desc +++ b/regression/cbmc/atomic_fetch_X-1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only no-new-smt main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/aws-byte-buf-regression/test.desc b/regression/cbmc/aws-byte-buf-regression/test.desc index 87997b956fc..1d99a5bb8bd 100644 --- a/regression/cbmc/aws-byte-buf-regression/test.desc +++ b/regression/cbmc/aws-byte-buf-regression/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c ---pointer-check + VERIFICATION SUCCESSFUL ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc index 2b746cacc8e..00327ebb729 100644 --- a/regression/cbmc/bounds_check1/test.desc +++ b/regression/cbmc/bounds_check1/test.desc @@ -1,6 +1,6 @@ CORE thorough-smt-backend no-new-smt main.c ---bounds-check --pointer-check + ^EXIT=10$ ^SIGNAL=0$ \[\(.*\)i2\]: FAILURE diff --git a/regression/cbmc/bounds_check2/test.desc b/regression/cbmc/bounds_check2/test.desc index 2af7f866590..86b25cb3b31 100644 --- a/regression/cbmc/bounds_check2/test.desc +++ b/regression/cbmc/bounds_check2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---bounds-check --retain-trivial-checks +--retain-trivial-checks ^Generated \d+ VCC\(s\), 0 remaining after simplification$ ^\[main.array_bounds.1\] line 4 array 'A' (lower|upper) bound in A\[(\(signed (long (long )?)?int\))?1\]: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/byte_update11/test.desc b/regression/cbmc/byte_update11/test.desc index 9845e70d84b..59eb032535e 100644 --- a/regression/cbmc/byte_update11/test.desc +++ b/regression/cbmc/byte_update11/test.desc @@ -1,6 +1,6 @@ CORE main.c ---little-endian +--little-endian --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc index 0544dcdb715..2bdd86121c3 100644 --- a/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc +++ b/regression/cbmc/cover-failed-assertions/test-no-failed-assertions.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---cover location --pointer-check --malloc-may-fail --malloc-fail-null +--cover location --malloc-may-fail --malloc-fail-null \[main\.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED \[main\.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): FAILED \[main\.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED diff --git a/regression/cbmc/cover-failed-assertions/test.desc b/regression/cbmc/cover-failed-assertions/test.desc index 2b07b32fe2d..9b156333768 100644 --- a/regression/cbmc/cover-failed-assertions/test.desc +++ b/regression/cbmc/cover-failed-assertions/test.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure test.c ---cover location --cover-failed-assertions --pointer-check --malloc-may-fail --malloc-fail-null +--cover location --cover-failed-assertions --malloc-may-fail --malloc-fail-null \[main.coverage\.4\] file test\.c line \d+ function main block 4 \(lines test\.c:main:17,18\): SATISFIED \[main.coverage\.3\] file test\.c line \d+ function main block 3 \(lines test\.c:main:15\): SATISFIED \[main.coverage\.2\] file test\.c line \d+ function main block 2 \(lines test\.c:main:5,6,12,14\): SATISFIED diff --git a/regression/cbmc/coverage_report2/test.desc b/regression/cbmc/coverage_report2/test.desc index 825addd41c6..d41d800907e 100644 --- a/regression/cbmc/coverage_report2/test.desc +++ b/regression/cbmc/coverage_report2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---symex-coverage-report - --unwind 1 +--symex-coverage-report - --unwind 1 --no-standard-checks --no-unwinding-assertions ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/destructors/compound_literal.desc b/regression/cbmc/destructors/compound_literal.desc index f99cd3c3724..aa615705d7d 100644 --- a/regression/cbmc/destructors/compound_literal.desc +++ b/regression/cbmc/destructors/compound_literal.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 10 --show-goto-functions +--unwind 10 --show-goto-functions --no-standard-checks activate-multi-line-match (?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION ^EXIT=0$ diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc index 242e2c1d4c0..45ea1243134 100644 --- a/regression/cbmc/dynamic_size1/stack_object.desc +++ b/regression/cbmc/dynamic_size1/stack_object.desc @@ -1,6 +1,6 @@ CORE stack_object.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/dynamic_size1/test.desc b/regression/cbmc/dynamic_size1/test.desc index d110065a9cf..1fe4842c85f 100644 --- a/regression/cbmc/dynamic_size1/test.desc +++ b/regression/cbmc/dynamic_size1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/empty_compound_type1/test.desc b/regression/cbmc/empty_compound_type1/test.desc index 88df5a048c4..3c2578cdbef 100644 --- a/regression/cbmc/empty_compound_type1/test.desc +++ b/regression/cbmc/empty_compound_type1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/empty_compound_type2/test.desc b/regression/cbmc/empty_compound_type2/test.desc index 43b571fbd05..71835eef7cb 100644 --- a/regression/cbmc/empty_compound_type2/test.desc +++ b/regression/cbmc/empty_compound_type2/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/equality_through_array6/test.desc b/regression/cbmc/equality_through_array6/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc/equality_through_array6/test.desc +++ b/regression/cbmc/equality_through_array6/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/export-symex-ready-goto/exported.symex.ready.goto b/regression/cbmc/export-symex-ready-goto/exported.symex.ready.goto new file mode 100644 index 0000000000000000000000000000000000000000..3a78b92d0095cf82ad92a2d07cdb47a3ea8d59c3 GIT binary patch literal 7889 zcmZ`;3wRXOy+7w{vNO3-7caD!5-AYd-dl+fLd9}1H!4`YwNtNC`_Q)A&F*ZnWgqG8 zCV;oO0)n6mZw<$sNKz{0 z#4gX&{|th$f|+-6dA6WzQQ&&u_cumbArsmPt9RKl;~P?!5@K5lK0po5_u-|S6f_Gb zoyZsuZ$6*^^lt#VNCEYD*|_@CK=XV+5G)o}5_v%L6wv3)T%sZE#Ohm^)y~HzV);ha zqbQJdEKnH@=f^iW?Be@Hv@w!}62ahHA9f@gZA|2$Yjf5K(}TxhuI3O7ws*H7lk>>i z6?rJ$lu4xXPL|m{O^DP3LR^fnxdht&`+jN9E2Gf2cd1n#Z%#*L2=!XUQ;|fvXohy) z`$OZZVR(d9t&TutSNDB>P8m^;7!k=fv}gf}a*%$rKD`W2&MxzjGwFpdC;^EH2^kE| zDJz(d`ss?WlDrR*U%Jt#84Agc1^aW@_t2Ibn>hN=cJVzzl68}*pfg~BpXRNFmsOe zXZC=p+5;Uya-Uq3lQDubf;71NA13fcwwmX3WV&vxz3@ zVuFEEEZFym$&SE2_|yMu^^t5gGM?Fetk4w{AXe`|&lxq~S>8*D6|GF9W6n6GeHHQR z4PIA1QZ#)sgEFG*Z^d$nI~_LoTDJsPB~?~kOC;IsupuuPUk7(qU2hM))+!->R$a|% zLB@Vvsm_MIVpQXq*P~+G>j1ECTXejN3htCfb7XFGByCS!J-Scb`8zd@&lf zZoB#BFzV=?PBsGu`{2KQCL3~X+`f)VA{89CUAdF=#d(nyPJiKNS@e1s#F^X$PBcE#v4k)F8r{ zIJ0jaAmfGE-=57?VugL-VAaFMvF|`K1ja2d8dp(BfQwc4zfT*fNHmkf;|gAxR6$e9 z>{}IW4cyohKbxFHG0tw>+nucdQZVT_gjzBk;X>5dHhW{sGo$ zS>{dM4eX+`KFjzDKOoP-GG}3#A4<#It}JuM8%8y?kFJ*a(Okg)cp0~UGQbYc=2nSi zg>JX%e!A3%WK*)RuHdAcR*K!er#oe+Qi1m#sIv#^MB;Wm)ZtnkuGNVy0KXX2aj;Iy zMRoX@uIdyUEFjN7oik9UHeO*jU@KCxQR$ReWmMCgP}Ip6p^dw{6Vyq^5|MNoaRBVy z5O+7kt^HYrJw{kfM?wa#!ptlDeA+y?kPxDI3xR?`XO{aX8ph6X<(t9lM^I4(@f|1HCX2HxUqhOwbjZPWt{uQD& zTVdyvCV8bv^Q%TR4LGhQEjx^1s+>{Lsb%@C-RUFw#4^qGNypV`D|FgQCL3E}k5h~= z?NQ$-^H_Ms8o#+a@En?%4|g+gHxuri754ur++Qf%fQQ@SI^h=`-Qh~1ixzUl?f`rT z!M9e}|F7WhQt&-K3;wQ6-NEar#Rc93;7tJTGl47Ei5$3a?S_ z27~8KH7j5OIghuDEiS!>_q9UzYSDkmHybr*gD$&HJ`l6SuQ;>s_0)PGuZIC1hN_)>Iv+{%Q9m|=_qE&bn~B#Y z)45fPV?o|YVUA&s@Soy0;!8Vxdg4uFF8qkOnN zL0Bd2WZ1ddLi70B#!zbb#boT{^T~{~PO@07z5!|hpX%d~NaK_gNz&v3K9BJTI(suo zNv(*a3oRrjn2azm>-JasTmF;c>>Q5b)IwW-2N56V9isLcW}P=SCv1O~ct3~TwiSDxZxvUNIQ9!#1dItKeV|$Ei~OVm+ZY&>tf6JF!2Z&vY@{I-VXxp}LRl=4i=cdssHZ&3RYe<}=opNq%&L8rkA`A6 z6cO-i5Nf$L#tMF()Oej9SCaP@a>Pp?IA|3T;0>7oXhN4DhL>^#?`nR4=--qJZy___ zP;WeIetO1fO8>Hu83m#?m zS_r$2Hm%2|4blr6l@~h5AQ)MCU`yQ!kb1sYu6#kfYd7(YJky+44pA=J%&)7*p>_=9 z3!e3bT^QLw!~a=XC)gIU$5sk7RJd(?lTp((nyE}|2j3mi7(1cDE{bp35!&r;vI zc|Im|@J5v&M?r93q1deoMX^F`#jb)m52DPY3b7Z_u#Yr`H}(@aO5|`i`0KnTw4bl_ zaqChcaKnJ(K4n$GTnpf})Fb{1;P*7}0S)YBl@Is;U(+2h&KhpzSp(oT06s|8JEYC< zKJPGU>DQE9{ijCdI7eaziwmH&;m`}lsg?T&S|-63o#nC+0H z9k%;BN%Db4{0HA))c8k)PJWyuq4gz!4v4~h4}!x3g#>bGYi6eOu}?((0}rGjiLUw*~vd4VQ76x;539eBZWB&VLpK{=iGf( z`FTFgCydJOPY2aGpDgwSLH#Ukg(eCW)RV*-W2l@e&vO-uZTxN#Q(elQEXfC2p(&dD z9YI~iVFKzLPhX>gop?p=0&hK z?%XG~_%-t%xh|N`wg7tz1@W(eeZR(jKx6+#EH|qCF;}N%5*h;^5Zk+BA?FBaR2)E& zE8D?lJJ?JWWvEe?%A2HPfoWoK*^jt8}+21#pn`evWvfeYvIIJLL&;bz)XFgq~> zbzL&i2FjGhLt_|G;XUA#k{1_V-oOyNC)ov)e#0lL#EE^$~&N0<&X^0OgJd zW`STf5u~lwIbyO;(^Oh0%c5YXM^3u1;B+LREolfS49d5bC)(JCwUlK2?IjtXeZ zB~?}kL@fBCIPD94#TlV~8lisLU_)zPhC<7yh;v@Y_h4Pd9&7YlpxUAG51fx?h1gOBKSAyPKEn-y$w0m%X&;S!f#Ap_`t2~gRaYR1xJ^E;Ppdg@{r=h zE;zGT54#Kc4x)IPv8KB#u|!K%{rD=nesx!8xU1?8sw&gsWaG)qSeK&BrNAM{LFsa0 zRk_AQJnvG>bSa9wo3e=%PNXePk%qC0kCP_`T6G_amv}yl+jQJ7;9m$II;3fQp^ct= z(r*I{{YwAO9T$2}@FPty!umoqlad|aps@NhWvO6eT8Jhw;;}DVm%48fF?LEUl%I93 z#2TpZW#URX+Dhk17S_bFW-L`RbPw`2ClHwwJhEIkd`%9_mJGaOA#fa%Z;rCg$EDLo-h6ddOQ%g literal 0 HcmV?d00001 diff --git a/regression/cbmc/fault_localization-stop_on_fail1/test.desc b/regression/cbmc/fault_localization-stop_on_fail1/test.desc index 9358227a214..98ead3d5e2b 100644 --- a/regression/cbmc/fault_localization-stop_on_fail1/test.desc +++ b/regression/cbmc/fault_localization-stop_on_fail1/test.desc @@ -1,6 +1,6 @@ CORE paths-lifo-expected-failure broken-smt-backend no-new-smt main.c ---localize-faults --stop-on-fail +--localize-faults --stop-on-fail --no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.[12]\]: diff --git a/regression/cbmc/field-sensitivity14/test.desc b/regression/cbmc/field-sensitivity14/test.desc index d1748c78147..44eaf013d8f 100644 --- a/regression/cbmc/field-sensitivity14/test.desc +++ b/regression/cbmc/field-sensitivity14/test.desc @@ -1,7 +1,7 @@ CORE main.c -^Generated \d+ VCC\(s\), 0 remaining after simplification$ +^Generated \d+ VCC\(s\), \d remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/fmod1/test.desc b/regression/cbmc/fmod1/test.desc index 75ed3d2f77b..a685bfcb952 100644 --- a/regression/cbmc/fmod1/test.desc +++ b/regression/cbmc/fmod1/test.desc @@ -1,6 +1,6 @@ CORE broken-z3-smt-backend broken-smt-backend no-new-smt main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/function_option1/test.desc b/regression/cbmc/function_option1/test.desc index 521d7365c2f..d9eccf04205 100644 --- a/regression/cbmc/function_option1/test.desc +++ b/regression/cbmc/function_option1/test.desc @@ -1,6 +1,6 @@ CORE main.c - --function f +--function f --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc b/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc index 7a3c9680812..554a1ff19cd 100644 --- a/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc +++ b/regression/cbmc/gcc_builtin_sub_overflow/simplify.desc @@ -1,7 +1,7 @@ CORE simplify.c -^Generated 1 VCC\(s\), 0 remaining after simplification$ +^Generated 2 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/gcc_vector1/test.desc b/regression/cbmc/gcc_vector1/test.desc index 1c039664a91..a23743ed017 100644 --- a/regression/cbmc/gcc_vector1/test.desc +++ b/regression/cbmc/gcc_vector1/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/graphml_witness2/test.desc b/regression/cbmc/graphml_witness2/test.desc index b31243fbb28..f315f4facd2 100644 --- a/regression/cbmc/graphml_witness2/test.desc +++ b/regression/cbmc/graphml_witness2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---graphml-witness - --unwindset main.0:1 --unwinding-assertions --stack-trace +--no-standard-checks --graphml-witness - --unwindset main.0:1 --unwinding-assertions --stack-trace ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/guard1/test.desc b/regression/cbmc/guard1/test.desc index a6acc8553dc..4447dbc8203 100644 --- a/regression/cbmc/guard1/test.desc +++ b/regression/cbmc/guard1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---depth 19 +--depth 19 --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/havoc_object1/full-slice.desc b/regression/cbmc/havoc_object1/full-slice.desc index fe3706bdab4..fc0fabbcc93 100644 --- a/regression/cbmc/havoc_object1/full-slice.desc +++ b/regression/cbmc/havoc_object1/full-slice.desc @@ -4,5 +4,5 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 6 of 8 failed.*$ +^\*\* 6 of \d+ failed.*$ -- diff --git a/regression/cbmc/havoc_object1/test.desc b/regression/cbmc/havoc_object1/test.desc index abe30d88695..4a7c0222d44 100644 --- a/regression/cbmc/havoc_object1/test.desc +++ b/regression/cbmc/havoc_object1/test.desc @@ -4,5 +4,5 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 6 of 8 failed.*$ +^\*\* 6 of \d+ failed.*$ -- diff --git a/regression/cbmc/if1/test.desc b/regression/cbmc/if1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc/if1/test.desc +++ b/regression/cbmc/if1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/link_json_symtabs/test.desc b/regression/cbmc/link_json_symtabs/test.desc index c6f6ebe9068..82ec3792ca4 100644 --- a/regression/cbmc/link_json_symtabs/test.desc +++ b/regression/cbmc/link_json_symtabs/test.desc @@ -1,6 +1,6 @@ CORE one.json_symtab -two.json_symtab +two.json_symtab --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ \[1\] file two.adb line [0-9]+ assertion: SUCCESS diff --git a/regression/cbmc/locations1/test.desc b/regression/cbmc/locations1/test.desc index 12c44d464cd..9efefbc7362 100644 --- a/regression/cbmc/locations1/test.desc +++ b/regression/cbmc/locations1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---signed-overflow-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/member1/test.desc b/regression/cbmc/member1/test.desc index 22feeb5e857..0a54bc65651 100644 --- a/regression/cbmc/member1/test.desc +++ b/regression/cbmc/member1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc index 8f8e0f557a1..b475124244b 100644 --- a/regression/cbmc/memory_allocation1/test.desc +++ b/regression/cbmc/memory_allocation1/test.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$ diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index 879dc7a01f2..c008c1b6ed8 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -1,11 +1,11 @@ CORE main.c ---bounds-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$ ^\[main\.array_bounds\.3\] line 38 array.buffer (dynamic object )?upper bound in buffers\[(\(signed long (long )?int\))?0\]->buffer\[(\(signed long (long )?int\))?100\]: FAILURE$ -^\*\* 1 of 3 failed +^\*\* 1 of \d failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc index be58134bdcb..0887788eb0f 100644 --- a/regression/cbmc/memset3/test.desc +++ b/regression/cbmc/memset3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/mm_io1/test.desc b/regression/cbmc/mm_io1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc/mm_io1/test.desc +++ b/regression/cbmc/mm_io1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc index 96a326299a7..c5f294e4e53 100644 --- a/regression/cbmc/multiple-goto-traces/test.desc +++ b/regression/cbmc/multiple-goto-traces/test.desc @@ -1,6 +1,6 @@ CORE main.c ---trace +--trace --no-standard-checks activate-multi-line-match ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/null7/test.desc b/regression/cbmc/null7/test.desc index 45989540170..a29ca8bf58c 100644 --- a/regression/cbmc/null7/test.desc +++ b/regression/cbmc/null7/test.desc @@ -1,6 +1,6 @@ CORE main.c ---pointer-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/overflow/leftshift_overflow-c89.desc b/regression/cbmc/overflow/leftshift_overflow-c89.desc index 78ccc75aa8a..532a67e328d 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c89.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c89.desc @@ -1,6 +1,6 @@ CORE leftshift_overflow.c ---signed-overflow-check --c89 +--c89 ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$ @@ -8,7 +8,7 @@ leftshift_overflow.c ^\[.*\] line 17 arithmetic overflow on signed shl in .*: SUCCESS$ ^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$ ^\[.*\] line 30 arithmetic overflow on signed shl in .*: SUCCESS$ -^\*\* 2 of 6 failed +^\*\* 6 of \d+ failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc index 4059cdb1c85..9dd5cf440ce 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c99-full-slice.desc @@ -1,6 +1,6 @@ CORE leftshift_overflow.c ---signed-overflow-check --c99 --full-slice +--c99 --full-slice ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$ @@ -9,7 +9,7 @@ leftshift_overflow.c ^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$ ^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$ ^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$ -^\*\* 4 of 7 failed +^\*\* 8 of \d+ failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/overflow/leftshift_overflow-c99.desc b/regression/cbmc/overflow/leftshift_overflow-c99.desc index 5104954ed84..0efd7f5cad5 100644 --- a/regression/cbmc/overflow/leftshift_overflow-c99.desc +++ b/regression/cbmc/overflow/leftshift_overflow-c99.desc @@ -1,6 +1,6 @@ CORE leftshift_overflow.c ---signed-overflow-check --c99 +--c99 ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 8 arithmetic overflow on signed shl in .*: FAILURE$ @@ -9,7 +9,7 @@ leftshift_overflow.c ^\[.*\] line 20 arithmetic overflow on signed shl in .*: FAILURE$ ^\[.*\] line 26 arithmetic overflow on signed shl in .*: FAILURE$ ^\[.*\] line 30 arithmetic overflow on signed shl in .*: FAILURE$ -^\*\* 4 of 7 failed +^\*\* 8 of \d+ failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/overflow/mod_overflow.desc b/regression/cbmc/overflow/mod_overflow.desc index fd1ab486ff6..ab6f6c87a34 100644 --- a/regression/cbmc/overflow/mod_overflow.desc +++ b/regression/cbmc/overflow/mod_overflow.desc @@ -1,6 +1,6 @@ CORE mod_overflow.c ---signed-overflow-check + ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 9 result of signed mod is not representable in .*: FAILURE$ diff --git a/regression/cbmc/overflow/signed_addition_overflow1.desc b/regression/cbmc/overflow/signed_addition_overflow1.desc index 0db00fffad6..c913fc57d27 100644 --- a/regression/cbmc/overflow/signed_addition_overflow1.desc +++ b/regression/cbmc/overflow/signed_addition_overflow1.desc @@ -1,6 +1,6 @@ CORE signed_addition_overflow1.c ---signed-overflow-check + ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$ diff --git a/regression/cbmc/overflow/signed_addition_overflow2.desc b/regression/cbmc/overflow/signed_addition_overflow2.desc index 2e02a2230df..e10762406fd 100644 --- a/regression/cbmc/overflow/signed_addition_overflow2.desc +++ b/regression/cbmc/overflow/signed_addition_overflow2.desc @@ -1,6 +1,6 @@ CORE signed_addition_overflow2.c ---signed-overflow-check + ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$ diff --git a/regression/cbmc/overflow/signed_addition_overflow3.desc b/regression/cbmc/overflow/signed_addition_overflow3.desc index 9710d0ad847..e4bf6c9b0af 100644 --- a/regression/cbmc/overflow/signed_addition_overflow3.desc +++ b/regression/cbmc/overflow/signed_addition_overflow3.desc @@ -1,6 +1,6 @@ CORE signed_addition_overflow3.c ---signed-overflow-check --conversion-check +--conversion-check ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS diff --git a/regression/cbmc/overflow/signed_addition_overflow4.desc b/regression/cbmc/overflow/signed_addition_overflow4.desc index b532dbb788e..640e84ca06b 100644 --- a/regression/cbmc/overflow/signed_addition_overflow4.desc +++ b/regression/cbmc/overflow/signed_addition_overflow4.desc @@ -1,6 +1,6 @@ CORE signed_addition_overflow4.c ---signed-overflow-check --conversion-check +--conversion-check ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS diff --git a/regression/cbmc/overflow/signed_multiplication1.desc b/regression/cbmc/overflow/signed_multiplication1.desc index 3e243e13501..d2f1b2b01a5 100644 --- a/regression/cbmc/overflow/signed_multiplication1.desc +++ b/regression/cbmc/overflow/signed_multiplication1.desc @@ -1,6 +1,6 @@ CORE signed_multiplication1.c ---signed-overflow-check + ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/overflow/signed_subtraction1.desc b/regression/cbmc/overflow/signed_subtraction1.desc index fad1fa02144..acf808e8605 100644 --- a/regression/cbmc/overflow/signed_subtraction1.desc +++ b/regression/cbmc/overflow/signed_subtraction1.desc @@ -1,6 +1,6 @@ CORE signed_subtraction1.c ---signed-overflow-check +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/overflow/unary_minus_overflow.desc b/regression/cbmc/overflow/unary_minus_overflow.desc index 2766431e519..ce362b53e2c 100644 --- a/regression/cbmc/overflow/unary_minus_overflow.desc +++ b/regression/cbmc/overflow/unary_minus_overflow.desc @@ -1,6 +1,6 @@ CORE unary_minus_overflow.c ---signed-overflow-check --unsigned-overflow-check +--unsigned-overflow-check ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line .* arithmetic overflow on signed unary minus in -x: FAILURE$ diff --git a/regression/cbmc/path-per-path-vccs/test.desc b/regression/cbmc/path-per-path-vccs/test.desc index d399e5b2ddb..e45f14e00d1 100644 --- a/regression/cbmc/path-per-path-vccs/test.desc +++ b/regression/cbmc/path-per-path-vccs/test.desc @@ -1,6 +1,6 @@ CORE main.c ---paths lifo --unwind 1 --pointer-check +--paths lifo --unwind 1 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/pointer-predicates/at_bounds1.desc b/regression/cbmc/pointer-predicates/at_bounds1.desc index c2251b5db67..ced7be46573 100644 --- a/regression/cbmc/pointer-predicates/at_bounds1.desc +++ b/regression/cbmc/pointer-predicates/at_bounds1.desc @@ -1,6 +1,6 @@ CORE at_bounds1.c ---pointer-primitive-check --malloc-fail-null +--malloc-fail-null ^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$ ^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ diff --git a/regression/cbmc/points-to-sets/test_json.desc b/regression/cbmc/points-to-sets/test_json.desc index 3ee78b26f91..a7dec447a70 100644 --- a/regression/cbmc/points-to-sets/test_json.desc +++ b/regression/cbmc/points-to-sets/test_json.desc @@ -1,6 +1,6 @@ CORE main.c ---show-points-to-sets --json-ui +--show-points-to-sets --json-ui --no-standard-checks activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover_enable2/test.desc b/regression/cbmc/pragma_cprover_enable2/test.desc index 22b756e21c8..1b9ed534579 100644 --- a/regression/cbmc/pragma_cprover_enable2/test.desc +++ b/regression/cbmc/pragma_cprover_enable2/test.desc @@ -6,7 +6,9 @@ main.c ^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ ^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$ ^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$ -^\*\* 5 of \d+ failed +^\[main\.overflow\.6\] line 20 arithmetic overflow on signed \+ in n \+ n: FAILURE$ +^\[main\.overflow\.7\] line 21 arithmetic overflow on signed \+ in x \+ n: FAILURE$ +^\*\* 7 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/pragma_cprover_enable3/test.desc b/regression/cbmc/pragma_cprover_enable3/test.desc index 951dc2c266d..07f11389886 100644 --- a/regression/cbmc/pragma_cprover_enable3/test.desc +++ b/regression/cbmc/pragma_cprover_enable3/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-pointer-primitive-check ^main.c function main$ ^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ diff --git a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc index c9e8430a6b4..ea415d9e0fd 100644 --- a/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc +++ b/regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc @@ -1,6 +1,6 @@ CORE main.c - +-no-pointer-primitive-check ^main.c function main$ ^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$ diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index 6a461a6a137..1f292619f59 100644 --- a/regression/cbmc/r_w_ok1/test.desc +++ b/regression/cbmc/r_w_ok1/test.desc @@ -2,7 +2,7 @@ CORE main.c __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$ -^\*\* 2 of 12 failed +^\*\* 2 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/cbmc/r_w_ok10/test.desc b/regression/cbmc/r_w_ok10/test.desc index 7fe3f0ce2d4..6a98ceba1be 100644 --- a/regression/cbmc/r_w_ok10/test.desc +++ b/regression/cbmc/r_w_ok10/test.desc @@ -11,7 +11,7 @@ main.c ^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 34 dead object in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main.pointer_primitives.\d+\] line 40 deallocated dynamic object in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$ -^\*\* 8 of \d+ failed +^\*\* 9 of \d+ failed -- ^warning: ignoring -- diff --git a/regression/cbmc/runtime-profiling/test.desc b/regression/cbmc/runtime-profiling/test.desc index a7d3a1198a1..a6a504aa5b0 100644 --- a/regression/cbmc/runtime-profiling/test.desc +++ b/regression/cbmc/runtime-profiling/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^Runtime Symex:.*$ diff --git a/regression/cbmc/scanf1/big-endian.desc b/regression/cbmc/scanf1/big-endian.desc index 6528bb49ec8..11e3ce88ee9 100644 --- a/regression/cbmc/scanf1/big-endian.desc +++ b/regression/cbmc/scanf1/big-endian.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.i ---big-endian +--big-endian --no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^\*\* 8 of 8 failed diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc index 1f30ec816fe..301cf05ee22 100644 --- a/regression/cbmc/scanf1/test.desc +++ b/regression/cbmc/scanf1/test.desc @@ -1,6 +1,6 @@ CORE no-new-smt main.i ---little-endian +--little-endian --no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^\*\* 8 of 8 failed diff --git a/regression/cbmc/simplify-union/test.desc b/regression/cbmc/simplify-union/test.desc index de8c67be832..0ee536b695f 100644 --- a/regression/cbmc/simplify-union/test.desc +++ b/regression/cbmc/simplify-union/test.desc @@ -1,7 +1,7 @@ CORE main.c -^Generated 1 VCC\(s\), 0 remaining after simplification$ +^Generated 13 VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/sync_X_and_fetch-1/test.desc b/regression/cbmc/sync_X_and_fetch-1/test.desc index 27a28993ba5..1a10ff50301 100644 --- a/regression/cbmc/sync_X_and_fetch-1/test.desc +++ b/regression/cbmc/sync_X_and_fetch-1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/sync_fetch_and_X-1/test.desc b/regression/cbmc/sync_fetch_and_X-1/test.desc index 27a28993ba5..1a10ff50301 100644 --- a/regression/cbmc/sync_fetch_and_X-1/test.desc +++ b/regression/cbmc/sync_fetch_and_X-1/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc/sync_lock_release-1/test.desc b/regression/cbmc/sync_lock_release-1/test.desc index c985459baff..2b28e64db54 100644 --- a/regression/cbmc/sync_lock_release-1/test.desc +++ b/regression/cbmc/sync_lock_release-1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/uniform_array1/test.desc b/regression/cbmc/uniform_array1/test.desc index 1b1641fd47a..43f2d55e8aa 100644 --- a/regression/cbmc/uniform_array1/test.desc +++ b/regression/cbmc/uniform_array1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc index 171e794113a..22f5df0f5c1 100644 --- a/regression/cbmc/union12/test.desc +++ b/regression/cbmc/union12/test.desc @@ -1,10 +1,10 @@ CORE broken-smt-backend main.c ---pointer-check + ^EXIT=10$ ^SIGNAL=0$ ^\[main\.assertion\.2\] line 20 should fail: FAILURE$ -^\*\* 1 of 15 failed +^\*\* 1 of \d+ failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/union17/test.desc b/regression/cbmc/union17/test.desc index f3599e3b335..ca199761d93 100644 --- a/regression/cbmc/union17/test.desc +++ b/regression/cbmc/union17/test.desc @@ -1,6 +1,6 @@ CORE broken-smt-backend no-new-smt main.c ---no-simplify +--no-simplify --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/unwind_counters4/test.desc b/regression/cbmc/unwind_counters4/test.desc index f60b11caa10..0e0bdbdf656 100644 --- a/regression/cbmc/unwind_counters4/test.desc +++ b/regression/cbmc/unwind_counters4/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\** 2 of 2 failed +^\** 4 of 4 failed -- -- Loop unwinding must terminate despite the existence of multiple loop entry diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc index 83b8819429a..32c632099f9 100644 --- a/regression/cbmc/void_pointer3/test.desc +++ b/regression/cbmc/void_pointer3/test.desc @@ -1,6 +1,6 @@ CORE gcc-only main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ From be8e6a1760bc5f0e19d74734ec96c0d7821b8fcf Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 30 Nov 2023 15:16:43 +0000 Subject: [PATCH 8/8] Adjust flags for cbmc-shadow-memory/ regression tests --- regression/cbmc-shadow-memory/char1/test.desc | 2 +- regression/cbmc-shadow-memory/constchar-pointers1/test.desc | 2 +- regression/cbmc-shadow-memory/errno1/test.desc | 2 +- regression/cbmc-shadow-memory/linked-list1/test.desc | 2 +- regression/cbmc-shadow-memory/maybe-null1/test.desc | 2 +- regression/cbmc-shadow-memory/pointer-checks1/test.desc | 2 +- regression/cbmc-shadow-memory/pointer-checks2/test.desc | 2 +- regression/cbmc-shadow-memory/static1/test.desc | 2 +- regression/cbmc-shadow-memory/strdup1/main.c | 3 +++ regression/cbmc-shadow-memory/strdup1/test.desc | 2 +- 10 files changed, 12 insertions(+), 9 deletions(-) diff --git a/regression/cbmc-shadow-memory/char1/test.desc b/regression/cbmc-shadow-memory/char1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc-shadow-memory/char1/test.desc +++ b/regression/cbmc-shadow-memory/char1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc index e21095fda9d..eb2b6c78ddb 100644 --- a/regression/cbmc-shadow-memory/constchar-pointers1/test.desc +++ b/regression/cbmc-shadow-memory/constchar-pointers1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 11 +--unwind 11 --no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/errno1/test.desc b/regression/cbmc-shadow-memory/errno1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc-shadow-memory/errno1/test.desc +++ b/regression/cbmc-shadow-memory/errno1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/linked-list1/test.desc b/regression/cbmc-shadow-memory/linked-list1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc-shadow-memory/linked-list1/test.desc +++ b/regression/cbmc-shadow-memory/linked-list1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/maybe-null1/test.desc b/regression/cbmc-shadow-memory/maybe-null1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc-shadow-memory/maybe-null1/test.desc +++ b/regression/cbmc-shadow-memory/maybe-null1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/pointer-checks1/test.desc b/regression/cbmc-shadow-memory/pointer-checks1/test.desc index 984313a2d59..e527a51fe46 100644 --- a/regression/cbmc-shadow-memory/pointer-checks1/test.desc +++ b/regression/cbmc-shadow-memory/pointer-checks1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---verbosity 10 --pointer-check +--verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-shadow-memory/pointer-checks2/test.desc b/regression/cbmc-shadow-memory/pointer-checks2/test.desc index 1cb021a32b9..46231fc3ef0 100644 --- a/regression/cbmc-shadow-memory/pointer-checks2/test.desc +++ b/regression/cbmc-shadow-memory/pointer-checks2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---verbosity 10 --pointer-check +--verbosity 10 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-shadow-memory/static1/test.desc b/regression/cbmc-shadow-memory/static1/test.desc index 9efefbc7362..8002a63813a 100644 --- a/regression/cbmc-shadow-memory/static1/test.desc +++ b/regression/cbmc-shadow-memory/static1/test.desc @@ -1,6 +1,6 @@ CORE main.c - +--no-standard-checks ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-shadow-memory/strdup1/main.c b/regression/cbmc-shadow-memory/strdup1/main.c index b937b83bc97..fd23e37436c 100644 --- a/regression/cbmc-shadow-memory/strdup1/main.c +++ b/regression/cbmc-shadow-memory/strdup1/main.c @@ -8,6 +8,9 @@ int main() __CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0); char *s = (char *)malloc(3 * sizeof(char)); + // Terminate string so that `strdup` will not call `strlen` + // on a string without a null-terminator. + s[2] = '\0'; assert(__CPROVER_get_field(&s[0], "field1") == 0); assert(__CPROVER_get_field(&s[1], "field1") == 0); diff --git a/regression/cbmc-shadow-memory/strdup1/test.desc b/regression/cbmc-shadow-memory/strdup1/test.desc index 831280dc5ef..fee020638a8 100644 --- a/regression/cbmc-shadow-memory/strdup1/test.desc +++ b/regression/cbmc-shadow-memory/strdup1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwind 4 +--unwind 4 --no-standard-checks --no-built-in-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$