diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 6976ec2df0a..5bb4428f231 100644 --- a/regression/contracts/assigns_enforce_address_of/test.desc +++ b/regression/contracts/assigns_enforce_address_of/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc index 3a80f654b3b..b9ee423738e 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc index 3a80f654b3b..b9ee423738e 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_function_calls/main.c b/regression/contracts/assigns_enforce_function_calls/main.c index dffa10e0575..c4ce468f413 100644 --- a/regression/contracts/assigns_enforce_function_calls/main.c +++ b/regression/contracts/assigns_enforce_function_calls/main.c @@ -13,5 +13,4 @@ int main() { int x; foo(&x); - baz(&x); } diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index 3f29cee23a7..b3b4c031205 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: expecting void return type for function 'bar' called in assigns clause$ ^CONVERSION ERROR$ -- -- -Check that function call expressions are rejected in assigns clauses. +Check that non-void function call expressions are rejected in assigns clauses. diff --git a/regression/contracts/assigns_enforce_function_calls_ignored/main.c b/regression/contracts/assigns_enforce_function_calls_ignored/main.c new file mode 100644 index 00000000000..01faaaa4d0b --- /dev/null +++ b/regression/contracts/assigns_enforce_function_calls_ignored/main.c @@ -0,0 +1,17 @@ +void bar(int *x) +{ + if(x) + __CPROVER_typed_target(x); +} + +int foo(int *x) __CPROVER_assigns(bar(x)) +{ + *x = 0; + return 0; +} + +int main() +{ + int x; + foo(&x); +} diff --git a/regression/contracts/assigns_enforce_function_calls_ignored/test.desc b/regression/contracts/assigns_enforce_function_calls_ignored/test.desc new file mode 100644 index 00000000000..2b8cf826108 --- /dev/null +++ b/regression/contracts/assigns_enforce_function_calls_ignored/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract foo +^call to function 'bar' in assigns clause not supported yet$ +^EXIT=(127|134)$ +^SIGNAL=0$ +-- +-- +Check that void function call expressions in assigns clauses make +instrumentation fail. diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index d1f35051245..78c33a0aa62 100644 --- a/regression/contracts/assigns_enforce_literal/test.desc +++ b/regression/contracts/assigns_enforce_literal/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index 77d004e7e30..6449125a7fd 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index 77d004e7e30..6449125a7fd 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc index d994c951202..92a3ee83d44 100644 --- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc +++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc index c2afad9b49d..2788121bb93 100644 --- a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc +++ b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^main.c.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 8365e4216a0..3981a71e647 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -995,34 +995,34 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) else if(can_cast_expr(target)) { const auto &funcall = to_side_effect_expr_function_call(target); - if(can_cast_expr(funcall.function())) + if(!can_cast_expr(funcall.function())) { - const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); - if( - ident == CPROVER_PREFIX "assignable" || - ident == CPROVER_PREFIX "object_whole" || - ident == CPROVER_PREFIX "object_upto" || - ident == CPROVER_PREFIX "object_from") - { - for(const auto &argument : funcall.arguments()) - throw_on_side_effects(argument); - return; - } + throw invalid_source_file_exceptiont( + "function pointer calls not allowed in assigns clauses", + target.source_location()); } - else + + if(target.type().id() != ID_empty) { throw invalid_source_file_exceptiont( - "function pointer calls not allowed in assigns clauses", + "expecting void return type for function '" + + id2string(to_symbol_expr(funcall.function()).get_identifier()) + + "' called in assigns clause", target.source_location()); } + + for(const auto &argument : funcall.arguments()) + throw_on_side_effects(argument); + } + else + { + // if we reach this point the target did not pass the checks + throw invalid_source_file_exceptiont( + "assigns clause target must be a non-void lvalue, a call " + "to " CPROVER_PREFIX + "POINTER_OBJECT or a call to a function returning void", + target.source_location()); } - // if we reach this point the target did not pass the checks - throw invalid_source_file_exceptiont( - "assigns clause target must be a non-void lvalue or a call to one " - "of " CPROVER_PREFIX "POINTER_OBJECT, " CPROVER_PREFIX - "assignable, " CPROVER_PREFIX "object_whole, " CPROVER_PREFIX - "object_upto, " CPROVER_PREFIX "object_from", - target.source_location()); } void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 2d61047d28d..2fc087e3a59 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -487,6 +487,15 @@ car_exprt instrument_spec_assignst::create_car_expr( if(can_cast_expr(funcall.function())) { const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + + PRECONDITION_WITH_DIAGNOSTICS( + ident == CPROVER_PREFIX "object_from" || + ident == CPROVER_PREFIX "object_upto" || + ident == CPROVER_PREFIX "object_whole" || + ident == CPROVER_PREFIX "assignable", + "call to function '" + id2string(ident) + + "' in assigns clause not supported yet"); + if(ident == CPROVER_PREFIX "object_from") { const auto &ptr = funcall.arguments().at(0); @@ -558,12 +567,6 @@ car_exprt instrument_spec_assignst::create_car_expr( is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN : car_havoc_methodt::HAVOC_SLICE}; } - else - { - log.error().source_location = target.source_location(); - log.error() << "call to " << ident - << " in assigns clauses not supported in this version"; - } } } else if(is_assignable(target))