diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 9416192f053..474026934fa 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 \d+ failed -- ^warning: ignoring -- diff --git a/regression/cbmc/Undefined_Shift1/test.desc b/regression/cbmc/Undefined_Shift1/test.desc index 5ed811bd59e..06417908cee 100644 --- a/regression/cbmc/Undefined_Shift1/test.desc +++ b/regression/cbmc/Undefined_Shift1/test.desc @@ -4,11 +4,12 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[.*\] line 4 shift operand is negative in .*: SUCCESS$ +^\[.*\] line 5 shift operand is negative in .*: SUCCESS$ ^\[.*\] line 7 shift distance too large in .*: FAILURE$ ^\[.*\] 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 5 failed +^\*\* 3 of 6 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/bounds_check2/main.c b/regression/cbmc/bounds_check2/main.c new file mode 100644 index 00000000000..b9acd4c01fb --- /dev/null +++ b/regression/cbmc/bounds_check2/main.c @@ -0,0 +1,5 @@ +int main() +{ + int A[2]; + int x = A[1]; +} diff --git a/regression/cbmc/bounds_check2/test.desc b/regression/cbmc/bounds_check2/test.desc new file mode 100644 index 00000000000..ca9d85d6fd5 --- /dev/null +++ b/regression/cbmc/bounds_check2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--bounds-check --retain-trivial-checks +^Generated \d+ VCC\(s\), 0 remaining after simplification$ +^\[main.array_bounds.1\] line 4 array 'A' lower bound in A\[\(signed (long (long )?)?int\)1\]: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^Generated 0 VCC\(s\), 0 remaining after simplification$ diff --git a/regression/cbmc/pointer-overflow3/no-simplify.desc b/regression/cbmc/pointer-overflow3/no-simplify.desc new file mode 100644 index 00000000000..7a98821d501 --- /dev/null +++ b/regression/cbmc/pointer-overflow3/no-simplify.desc @@ -0,0 +1,16 @@ +CORE broken-smt-backend +main.c +--pointer-overflow-check --no-simplify +^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE +^\*\* 4 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +Invariant check failed +-- +Uses --no-simplify to avoid removing repeated ASSERT FALSE statements. diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc index 7a98821d501..429f07b4f66 100644 --- a/regression/cbmc/pointer-overflow3/test.desc +++ b/regression/cbmc/pointer-overflow3/test.desc @@ -1,6 +1,6 @@ -CORE broken-smt-backend +CORE main.c ---pointer-overflow-check --no-simplify +--pointer-overflow-check ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE @@ -12,5 +12,3 @@ main.c -- ^warning: ignoring Invariant check failed --- -Uses --no-simplify to avoid removing repeated ASSERT FALSE statements. diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 55169428900..e4e16f371c4 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -70,7 +70,7 @@ class goto_checkt _options.get_bool_option("float-overflow-check"); enable_simplify=_options.get_bool_option("simplify"); enable_nan_check=_options.get_bool_option("nan-check"); - retain_trivial=_options.get_bool_option("retain-trivial"); + retain_trivial = _options.get_bool_option("retain-trivial-checks"); enable_assert_to_assume=_options.get_bool_option("assert-to-assume"); enable_assertions=_options.get_bool_option("assertions"); enable_built_in_assertions=_options.get_bool_option("built-in-assertions"); @@ -242,7 +242,7 @@ class goto_checkt const guardt &guard); goto_programt new_code; - typedef std::set assertionst; + typedef std::set> assertionst; assertionst assertions; /// Remove all assertions containing the symbol in \p lhs as well as all @@ -333,8 +333,12 @@ void goto_checkt::invalidate(const exprt &lhs) for(auto it = assertions.begin(); it != assertions.end();) { - if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference)) + if( + has_symbol(it->second, find_symbols_set) || + has_subexpr(it->second, ID_dereference)) + { it = assertions.erase(it); + } else ++it; } @@ -1545,7 +1549,7 @@ void goto_checkt::add_guarded_property( ? std::move(simplified_expr) : implies_exprt{guard.as_expr(), std::move(simplified_expr)}; - if(assertions.insert(guarded_expr).second) + if(assertions.insert(std::make_pair(src_expr, guarded_expr)).second) { auto t = new_code.add( enable_assert_to_assume ? goto_programt::make_assumption( diff --git a/src/analyses/goto_check.h b/src/analyses/goto_check.h index ad47e6827d7..fe5b0099983 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)" \ + "(retain-trivial-checks)" // clang-format off #define HELP_GOTO_CHECK \ @@ -54,9 +55,10 @@ void goto_check( " --undefined-shift-check check shift greater than bit-width\n" \ " --float-overflow-check check floating-point for +/-Inf\n" \ " --nan-check check floating-point for NaN\n" \ - " --no-built-in-assertions ignore assertions in built-in library\n" \ " --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) */ \ + " --no-built-in-assertions ignore assertions in built-in library\n" \ + " --retain-trivial-checks include checks that are trivially true\n" \ #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \ options.set_option("bounds-check", cmdline.isset("bounds-check")); \ @@ -72,7 +74,10 @@ 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("retain-trivial-checks", \ + cmdline.isset("retain-trivial-checks")); \ + (void)0 // clang-format on #endif // CPROVER_ANALYSES_GOTO_CHECK_H