From 8152d87da5ded1f9f0426211a52cf516fdafb864 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 30 Jun 2020 10:43:09 +0100 Subject: [PATCH 1/5] Add new --overly-large-allocation-check option to goto_check() The option adds an assertion to check that not more memory is allocated with __CPROVER_allocate() than cbmc can address. Since the primitive is used by the models of malloc(), etc., this also guarantees that those function don't allocate more memory than can be addressed. --- src/analyses/goto_check.cpp | 41 +++++++++++++++++++++++++++++++++++++ src/analyses/goto_check.h | 11 +++++++--- 2 files changed, 49 insertions(+), 3 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index aaf277a904f..1af83471c5f 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -75,6 +75,8 @@ class goto_checkt error_labels=_options.get_list_option("error-label"); enable_pointer_primitive_check = _options.get_bool_option("pointer-primitive-check"); + enable_overly_large_allocation_check = + _options.get_bool_option("overly-large-allocation-check"); } typedef goto_functionst::goto_functiont goto_functiont; @@ -195,6 +197,10 @@ class goto_checkt /// \param guard: the condition under which the operation happens void pointer_primitive_check(const exprt &expr, const guardt &guard); + void overly_large_allocation_check( + const side_effect_exprt &expr, + const guardt &guard); + /// Returns true if the given expression is a pointer primitive such as /// __CPROVER_r_ok() /// @@ -256,6 +262,7 @@ class goto_checkt bool enable_built_in_assertions; bool enable_assumptions; bool enable_pointer_primitive_check; + bool enable_overly_large_allocation_check; typedef optionst::value_listt error_labelst; error_labelst error_labels; @@ -1229,6 +1236,29 @@ void goto_checkt::pointer_primitive_check( guard); } +void goto_checkt::overly_large_allocation_check( + const side_effect_exprt &expr, + const guardt &guard) +{ + if(!enable_overly_large_allocation_check) + return; + + const exprt size_expr = expr.operands().front(); + + binary_relation_exprt bre( + size_expr, + ID_le, + ns.lookup(CPROVER_PREFIX "max_malloc_size").symbol_expr()); + + add_guarded_property( + bre, + "more memory allocated than can be addressed by cbmc", + "allocate", + expr.source_location(), + expr, + guard); +} + bool goto_checkt::is_pointer_primitive(const exprt &expr) { // we don't need to include the __CPROVER_same_object primitive here as it @@ -1812,6 +1842,15 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard) { pointer_primitive_check(expr, guard); } + else if(expr.id() == ID_side_effect) + { + const auto &side_effect_expr = to_side_effect_expr(expr); + + if(side_effect_expr.get_statement() == ID_allocate) + { + overly_large_allocation_check(side_effect_expr, guard); + } + } } void goto_checkt::check(const exprt &expr) @@ -1934,6 +1973,8 @@ void goto_checkt::goto_check( flag_resetter.set_flag(enable_nan_check, false); else if(d.first == "disable:pointer-primitive-check") flag_resetter.set_flag(enable_pointer_primitive_check, false); + else if(d.first == "disable:overly-large-allocation-check") + flag_resetter.set_flag(enable_overly_large_allocation_check, false); } new_code.clear(); diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index ad47e6827d7..7f6f6295246 100644 --- a/src/analyses/goto_check.h +++ b/src/analyses/goto_check.h @@ -39,7 +39,8 @@ void goto_check( "overflow-check)" \ "(pointer-overflow-check)(conversion-check)(undefined-shift-check)" \ "(float-overflow-check)(nan-check)(no-built-in-assertions)" \ - "(pointer-primitive-check)" + "(pointer-primitive-check)" \ + "(overly-large-allocation-check)" // clang-format off #define HELP_GOTO_CHECK \ @@ -56,7 +57,10 @@ void goto_check( " --nan-check check floating-point for NaN\n" \ " --no-built-in-assertions ignore assertions in built-in library\n" \ " --enum-range-check checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \ - " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ + " --pointer-primitive-check checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */ \ + << help_entry( \ + "--overly-large-allocation-check", \ + "checks that no individual allocation exceeds CBMC's address space limit") #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ @@ -72,7 +76,8 @@ void goto_check( 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("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \ + options.set_option("overly-large-allocation-check", cmdline.isset("overly-large-allocation-check")) /* NOLINT(whitespace/line_length) */ // clang-format on #endif // CPROVER_ANALYSES_GOTO_CHECK_H From 0ee13c99010f78d6e1a04e04e30f8f0becfc9e1e Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 30 Jun 2020 12:17:45 +0100 Subject: [PATCH 2/5] Adapt usages of the HELP_GOTO_CHECK macro Adapt the help messages of all the tools to work with the macro HELP_GOTO_CHECK which is now using help_entry() for the entry for --overly-large-allocation-check --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- src/goto-diff/goto_diff_parse_options.cpp | 2 +- src/goto-instrument/goto_instrument_parse_options.cpp | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b547bd66214..b0bde272b6b 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1067,7 +1067,7 @@ void cbmc_parse_optionst::help() HELP_SHOW_GOTO_FUNCTIONS "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK + << HELP_GOTO_CHECK << " --no-assertions ignore user assertions\n" " --no-assumptions ignore user assumptions\n" " --error-label label check that label is unreachable\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 972134614e2..6b23cd7154a 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -916,7 +916,7 @@ void goto_analyzer_parse_optionst::help() HELP_SHOW_PROPERTIES "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK + << HELP_GOTO_CHECK << "\n" "Other options:\n" HELP_VALIDATE diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 2753ec1d1ba..956de88a243 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -407,7 +407,7 @@ void goto_diff_parse_optionst::help() " --compact-output output dependencies in compact mode\n" "\n" "Program instrumentation options:\n" - HELP_GOTO_CHECK + << HELP_GOTO_CHECK << " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) "Other options:\n" " --version show version and exit\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 9a3d00a69b4..5139cbf3d0d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1792,7 +1792,7 @@ void goto_instrument_parse_optionst::help() "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" - HELP_GOTO_CHECK + << HELP_GOTO_CHECK << " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*) " --error-label label check that label is unreachable\n" " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*) From c466524897b3db302391eb9dbdae2946e3634456 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 30 Jun 2020 11:31:58 +0100 Subject: [PATCH 3/5] Simplify malloc models for allocation failures --- src/ansi-c/ansi_c_internal_additions.cpp | 12 ++---- src/ansi-c/library/stdlib.c | 50 +++++------------------- src/cbmc/cbmc_parse_options.cpp | 11 +++--- src/cbmc/cbmc_parse_options.h | 4 +- src/util/config.cpp | 17 ++++---- src/util/config.h | 11 +----- 6 files changed, 34 insertions(+), 71 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index cc6e04020ec..8d7f95d4122 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -186,17 +186,13 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" "const void *" CPROVER_PREFIX "alloca_object = 0;\n" - "int " CPROVER_PREFIX "malloc_failure_mode="+ - std::to_string(config.ansi_c.malloc_failure_mode)+";\n" - "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+ - std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n" - "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+ - std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n" CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ integer2string(max_malloc_size(config.ansi_c.pointer_width, config .bv_encoding.object_bits))+";\n" - CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " + - std::to_string(config.ansi_c.malloc_may_fail) + ";\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_may_fail = " + + std::to_string(config.ansi_c.allocate_may_fail) + ";\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_size_null = " + + std::to_string(config.ansi_c.allocate_size_null) + ";\n" // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 2bf24fdc654..afd010d9c8e 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -75,29 +75,14 @@ __CPROVER_HIDE:; __CPROVER_size_t alloc_size = nmemb * size; #pragma CPROVER check pop - if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null) + if(__CPROVER_allocate_size_null && alloc_size > __CPROVER_max_malloc_size) { - __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); - if( - alloc_size > __CPROVER_max_malloc_size || - (__CPROVER_malloc_may_fail && should_malloc_fail)) - { - return (void *)0; - } + return (void *)0; } - else if( - __CPROVER_malloc_failure_mode == - __CPROVER_malloc_failure_mode_assert_then_assume) + + if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool()) { - __CPROVER_assert( - alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded"); - __CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size); - - __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); - __CPROVER_assert( - !__CPROVER_malloc_may_fail || !should_malloc_fail, - "max allocation may fail"); - __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail); + return (void *)0; } void *malloc_res; @@ -141,29 +126,14 @@ inline void *malloc(__CPROVER_size_t malloc_size) // but we only do so if `--malloc-may-fail` is set __CPROVER_HIDE:; - if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null) + if(__CPROVER_allocate_size_null && malloc_size > __CPROVER_max_malloc_size) { - __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); - if( - malloc_size > __CPROVER_max_malloc_size || - (__CPROVER_malloc_may_fail && should_malloc_fail)) - { - return (void *)0; - } + return (void *)0; } - else if( - __CPROVER_malloc_failure_mode == - __CPROVER_malloc_failure_mode_assert_then_assume) + + if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool()) { - __CPROVER_assert( - malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded"); - __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size); - - __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); - __CPROVER_assert( - !__CPROVER_malloc_may_fail || !should_malloc_fail, - "max allocation may fail"); - __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail); + return (void *)0; } void *malloc_res; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b0bde272b6b..63edc5010dc 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1073,11 +1073,12 @@ void cbmc_parse_optionst::help() " --error-label label check that label is unreachable\n" " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) - // NOLINTNEXTLINE(whitespace/line_length) - " --malloc-fail-assert set malloc failure mode to assert-then-assume\n" - " --malloc-fail-null set malloc failure mode to return null\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --malloc-may-fail allow malloc calls to return a null pointer\n" + << help_entry( + "--overly-large-allocation-returns-null", + "memory allocation functions return null when more memory is allocated than can be addressed by cbmc") // NOLINT(*) + << help_entry( + "--allocation-may-fail", + "allow memory allocation functions to return null") << HELP_REACHABILITY_SLICER HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index d5cc76e332e..c3c782c8108 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -51,8 +51,8 @@ class optionst; "(object-bits):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ - "(malloc-fail-assert)(malloc-fail-null)" \ - "(malloc-may-fail)" \ + "(overly-large-allocation-returns-null)" \ + "(allocation-may-fail)" \ OPT_XML_INTERFACE \ OPT_JSON_INTERFACE \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ diff --git a/src/util/config.cpp b/src/util/config.cpp index 889b48b984e..158cb8535aa 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1093,17 +1093,20 @@ bool configt::set(const cmdlinet &cmdline) bv_encoding.is_object_bits_default = false; } - if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null")) + if( + cmdline.isset("overly-large-allocation-check") && + cmdline.isset("overly-large-allocation-returns-null")) { throw invalid_command_line_argument_exceptiont{ - "at most one malloc failure mode is acceptable", "--malloc-fail-null"}; + "only one of " + "--overly-large-allocation-check/--overly-large-allocation-returns-null " + "can be given at a time", + "--overly-large-allocation-check/--overly-large-allocation-returns-null"}; } - if(cmdline.isset("malloc-fail-null")) - ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null; - if(cmdline.isset("malloc-fail-assert")) - ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; - ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail"); + ansi_c.allocate_may_fail = cmdline.isset("allocation-may-fail"); + ansi_c.allocate_size_null = + cmdline.isset("overly-large-allocation-returns-null"); return false; } diff --git a/src/util/config.h b/src/util/config.h index 19290cd3dbb..d76ac9728e2 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -129,16 +129,9 @@ class configt libt lib; bool string_abstraction; - bool malloc_may_fail = false; - enum malloc_failure_modet - { - malloc_failure_mode_none = 0, - malloc_failure_mode_return_null = 1, - malloc_failure_mode_assert_then_assume = 2 - }; - - malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none; + bool allocate_may_fail = false; + bool allocate_size_null = false; static const std::size_t default_object_bits=8; } ansi_c; From 610483bb041d783531466eb3a2d42238ff017ea1 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 30 Jun 2020 16:16:12 +0100 Subject: [PATCH 4/5] Adapt existing regression tests for new command line options Adapt the malloc failure regression tests to use the new options --overly-large-allocation-check, --overly-large-allocation-returns-null, and --allocate-may-fail --- regression/cbmc/malloc-may-fail/test.desc | 2 +- regression/cbmc/malloc-too-large/largest_representable.desc | 4 ++-- regression/cbmc/malloc-too-large/max_size.desc | 4 ++-- regression/cbmc/malloc-too-large/one_byte_too_large.desc | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/cbmc/malloc-may-fail/test.desc b/regression/cbmc/malloc-may-fail/test.desc index fb64c203397..3bf5c4775ea 100644 --- a/regression/cbmc/malloc-may-fail/test.desc +++ b/regression/cbmc/malloc-may-fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---malloc-may-fail --malloc-fail-null +--allocation-may-fail ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$ diff --git a/regression/cbmc/malloc-too-large/largest_representable.desc b/regression/cbmc/malloc-too-large/largest_representable.desc index d6f9fd63d14..cba42ddc08d 100644 --- a/regression/cbmc/malloc-too-large/largest_representable.desc +++ b/regression/cbmc/malloc-too-large/largest_representable.desc @@ -1,9 +1,9 @@ CORE largest_representable.c ---malloc-fail-assert +--overly-large-allocation-check ^EXIT=0$ ^SIGNAL=0$ -^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$ +^\[malloc.allocate.\d+\] line \d+ .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/max_size.desc b/regression/cbmc/malloc-too-large/max_size.desc index 783470072e3..16115a96590 100644 --- a/regression/cbmc/malloc-too-large/max_size.desc +++ b/regression/cbmc/malloc-too-large/max_size.desc @@ -1,9 +1,9 @@ CORE max_size.c ---malloc-fail-assert +--overly-large-allocation-check ^EXIT=10$ ^SIGNAL=0$ -^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: FAILURE$ +^\[malloc.allocate.\d+\] line \d+ .*: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.desc b/regression/cbmc/malloc-too-large/one_byte_too_large.desc index dbec5e98957..c5b21cbb04e 100644 --- a/regression/cbmc/malloc-too-large/one_byte_too_large.desc +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.desc @@ -1,6 +1,6 @@ CORE one_byte_too_large.c ---malloc-fail-null +--overly-large-allocation-returns-null ^EXIT=10$ ^SIGNAL=0$ ^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$ From 02172ccba15d7bf349926738412867722b2d16ca Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 30 Jun 2020 16:17:12 +0100 Subject: [PATCH 5/5] Adapt unrelated regression tests Due to the changes to the malloc models, less assertions are now generated by default. Thus, adapt the regexes ` of failed` in the test.desc files --- regression/cbmc/Pointer_byte_extract5/no-simplify.desc | 2 +- regression/cbmc/Pointer_byte_extract5/test.desc | 2 +- regression/cbmc/array_constraints1/test.desc | 2 +- regression/cbmc/pointer-overflow1/test.desc | 2 +- regression/cbmc/r_w_ok1/test.desc | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index a0cd2a4ed2e..2c13864d894 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 16 failed +\*\* 1 of 14 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 9416192f053..cdef75df344 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 14 failed +\*\* 1 of 12 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 9d4f5476bc3..8040e5651bf 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 16 +^\*\* 2 of 14 -- ^warning: ignoring diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index c0f0033f690..2055355d938 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/regression/cbmc/pointer-overflow1/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS ^VERIFICATION FAILED$ -^\*\* 8 of 13 failed +^\*\* 8 of 11 failed -- ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE ^warning: ignoring diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index 6a461a6a137..e50051dc10b 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 10 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$