Merge pull request #7328 from remi-delmas-3000/drop-pointer-contrat-support

CONTRACTS: Drop function pointer contract support

Author: tautschnig

regression/contracts/function-pointer-contracts-enforce/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --enforce-contract foo --restrict-function-pointer foo.function_pointer_call.1/contract --replace-call-with-contract contract --replace-call-with-contract bar
-^EXIT=0$
+^file main.c line 23: require_contracts or ensures_contract clauses are not supported$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that we can require that a function pointer satisfies some named

regression/contracts/function-pointer-contracts-replace/test.desc

@@ -1,12 +1,9 @@
 CORE
 main.c
 --replace-call-with-contract foo
-^\[foo.precondition.\d+] line 19 Assert function pointer 'infun' obeys contract 'contract': SUCCESS$
-^\[main.assertion.\d+].* assertion outfun1 == contract: SUCCESS$
-^\[main.assertion.\d+].* assertion outfun2 == contract: SUCCESS$
-^EXIT=0$
+^file main.c line 19 function foo: require_contracts or ensures_contract clauses are not supported$
+^EXIT=6$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that, when replacing a call by its contract,

src/goto-instrument/contracts/contracts.cpp

@@ -1204,36 +1204,19 @@ void code_contractst::assert_function_pointer_obeys_contract(
   const irep_idt &mode,
   goto_programt &dest)
 {
-  source_locationt loc(expr.source_location());
-  loc.set_property_class(property_class);
-  std::stringstream comment;
-  comment << "Assert function pointer '"
-          << from_expr_using_mode(ns, mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(ns, mode, expr.address_of_contract()) << "'";
-  loc.set_comment(comment.str());
-  code_assertt assert_expr(
-    equal_exprt{expr.function_pointer(), expr.address_of_contract()});
-  assert_expr.add_source_location() = loc;
-  goto_programt instructions;
-  converter.goto_convert(assert_expr, instructions, mode);
-  dest.destructive_append(instructions);
+  throw invalid_source_file_exceptiont(
+    "require_contracts or ensures_contract clauses are not supported",
+    expr.source_location());
 }
 
 void code_contractst::assume_function_pointer_obeys_contract(
   const function_pointer_obeys_contract_exprt &expr,
   const irep_idt &mode,
   goto_programt &dest)
 {
-  source_locationt loc(expr.source_location());
-  std::stringstream comment;
-  comment << "Assume function pointer '"
-          << from_expr_using_mode(ns, mode, expr.function_pointer())
-          << "' obeys contract '"
-          << from_expr_using_mode(ns, mode, expr.address_of_contract()) << "'";
-  loc.set_comment(comment.str());
-  dest.add(goto_programt::make_assignment(
-    expr.function_pointer(), expr.address_of_contract(), loc));
+  throw invalid_source_file_exceptiont(
+    "require_contracts or ensures_contract clauses are not supported",
+    expr.source_location());
 }
 
 void code_contractst::add_contract_check(