diff --git a/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c new file mode 100644 index 00000000000..0d03e24fb56 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.c @@ -0,0 +1,10 @@ +#ifndef __GNUC__ +_Bool __builtin_add_overflow(); +#endif + +int main() +{ + unsigned a, b, c; + if(__builtin_add_overflow(a, b, &c)) + return 0; +} diff --git a/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc new file mode 100644 index 00000000000..d601d8b4c24 --- /dev/null +++ b/regression/cbmc/gcc_builtin_add_overflow/conversion-check.desc @@ -0,0 +1,10 @@ +CORE +conversion-check.c +--conversion-check --unsigned-overflow-check --signed-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^Generated [1-9]\d* VCC\(s\) +-- +Zero VCCs should be generated. diff --git a/regression/cbmc/pragma_cprover4/main.c b/regression/cbmc/pragma_cprover4/main.c new file mode 100644 index 00000000000..193dfd9d986 --- /dev/null +++ b/regression/cbmc/pragma_cprover4/main.c @@ -0,0 +1,22 @@ +#include + +int nondet_int(); + +void main() +{ + int a = nondet_int(); + int b = nondet_int(); + int c = a + +#pragma CPROVER check disable "signed-overflow" + (a + b); +#pragma CPROVER check pop + +#pragma CPROVER check disable "signed-overflow" + for(int i = 0; i < 10; ++i) + { + int temp = a + b; +#pragma CPROVER check pop + int foo = temp + a; + assert(foo > 2); + } +} diff --git a/regression/cbmc/pragma_cprover4/test.desc b/regression/cbmc/pragma_cprover4/test.desc new file mode 100644 index 00000000000..45d63b42913 --- /dev/null +++ b/regression/cbmc/pragma_cprover4/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--signed-overflow-check +^\[main.overflow.1\] line 9 arithmetic overflow on signed \+ in a \+ a \+ b: FAILURE$ +^\[main.overflow.2\] line 19 arithmetic overflow on signed \+ in temp \+ a: FAILURE$ +^\[main.assertion.1\] line 20 assertion foo > 2: FAILURE$ +^\*\* 3 of 3 failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +No assertions other than the above three are expected. diff --git a/regression/contracts/simplify-overflow/main.c b/regression/contracts/simplify-overflow/main.c new file mode 100644 index 00000000000..4929b9e9c56 --- /dev/null +++ b/regression/contracts/simplify-overflow/main.c @@ -0,0 +1,9 @@ +int main() +{ + char buf[10]; + __CPROVER_size_t max = 9; + __CPROVER_size_t start = 1; + + __CPROVER_assert( + __CPROVER_r_ok(buf + start, max - start), "array is readable"); +} diff --git a/regression/contracts/simplify-overflow/test.desc b/regression/contracts/simplify-overflow/test.desc new file mode 100644 index 00000000000..fe21afc0216 --- /dev/null +++ b/regression/contracts/simplify-overflow/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--nan-check _ --signed-overflow-check --unsigned-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test doesn't actually use contracts, but rather demonstrates the workflow +of having goto-instrument expand __CPROVER_r_ok (but really doing nothing else) +before CBMC when may add (overflow) checks. Doing so must not result in failing +assertions that would not have failed on the original input. diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp index d07bbbd7b34..fbb1bf5c9e8 100644 --- a/src/analyses/goto_check_c.cpp +++ b/src/analyses/goto_check_c.cpp @@ -1895,6 +1895,33 @@ void goto_check_ct::check_rec_arithmetic_op( void goto_check_ct::check_rec(const exprt &expr, const guardt &guard) { + flag_overridet resetter(expr.source_location()); + const auto &pragmas = expr.source_location().get_pragmas(); + for(const auto &d : pragmas) + { + // match named-check related pragmas + auto matched = match_named_check(d.first); + if(matched.has_value()) + { + auto named_check = matched.value(); + auto name = named_check.first; + auto status = named_check.second; + bool *flag = name_to_flag.find(name)->second; + switch(status) + { + case check_statust::ENABLE: + resetter.set_flag(*flag, true, name); + break; + case check_statust::DISABLE: + resetter.set_flag(*flag, false, name); + break; + case check_statust::CHECKED: + resetter.disable_flag(*flag, name); + break; + } + } + } + if(expr.id() == ID_exists || expr.id() == ID_forall) { // the scoped variables may be used in the assertion @@ -2020,6 +2047,10 @@ optionalt goto_check_ct::rw_ok_check(exprt expr) exprt c = conjunction(conjuncts); if(enable_simplify) simplify(c, ns); + + // this is a logic expression, C language checks no longer apply + add_all_disable_named_check_pragmas(c.add_source_location()); + return c; } else if(modified) diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp index 5e90ccbf56a..ad88cb68841 100644 --- a/src/ansi-c/ansi_c_parser.cpp +++ b/src/ansi-c/ansi_c_parser.cpp @@ -203,6 +203,9 @@ void ansi_c_parsert::pragma_cprover_add_check( bool ansi_c_parsert::pragma_cprover_clash(const irep_idt &name, bool enabled) { + if(pragma_cprover_stack.empty()) + return false; + auto top = pragma_cprover_stack.back(); auto found = top.find(name); return found != top.end() && found->second != enabled; diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 2a5785b1eb9..e88ea5c692a 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -656,9 +656,12 @@ void goto_convertt::remove_overflow( if(result.type().id() == ID_pointer) { result_type = to_pointer_type(result.type()).base_type(); - code_assignt result_assignment{dereference_exprt{result}, - typecast_exprt{operation, *result_type}, - expr.source_location()}; + source_locationt source_location_annotated = expr.source_location(); + source_location_annotated.add_pragma("disable:conversion-check"); + code_assignt result_assignment{ + dereference_exprt{result}, + typecast_exprt{operation, *result_type}, + source_location_annotated}; convert_assign(result_assignment, dest, mode); } else