Merge pull request #7082 from remi-delmas-3000/function-pointer-obeys-contract-exprt-improvements

CONTRACTS: Convenience updates for `function_pointer_obeys_contract_exprt`

Author: remi-delmas-3000

src/ansi-c/c_expr.h

@@ -364,12 +364,22 @@ class function_pointer_obeys_contract_exprt : public exprt
     return op0();
   }
 
-  const exprt &contract() const
+  const symbol_exprt &contract_symbol_expr() const
+  {
+    return to_symbol_expr(op1().operands().at(0));
+  }
+
+  symbol_exprt &contract_symbol_expr()
+  {
+    return to_symbol_expr(op1().operands().at(0));
+  }
+
+  const exprt &address_of_contract() const
   {
     return op1();
   }
 
-  exprt &contract()
+  exprt &address_of_contract()
   {
     return op1();
   }

src/ansi-c/c_typecheck_code.cpp

@@ -1040,14 +1040,14 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
   }
 
   // second parameter must be the address of a function symbol
-  auto &contract = obeys_expr.contract();
-  typecheck_expr(contract);
+  auto &address_of_contract = obeys_expr.address_of_contract();
+  typecheck_expr(address_of_contract);
 
   if(
-    contract.id() != ID_address_of ||
-    to_address_of_expr(contract).object().id() != ID_symbol ||
-    contract.type().id() != ID_pointer ||
-    to_pointer_type(contract.type()).subtype().id() != ID_code)
+    address_of_contract.id() != ID_address_of ||
+    to_address_of_expr(address_of_contract).object().id() != ID_symbol ||
+    address_of_contract.type().id() != ID_pointer ||
+    to_pointer_type(address_of_contract.type()).subtype().id() != ID_code)
   {
     error().source_location = expr.source_location();
     error() << "the second parameter of the requires_contract/ensures_contract "
@@ -1056,7 +1056,7 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract(
     throw 0;
   }
 
-  if(function_pointer.type() != contract.type())
+  if(function_pointer.type() != address_of_contract.type())
   {
     error().source_location = expr.source_location();
     error() << "the first and second parameter of the "

src/goto-instrument/contracts/contracts.cpp

@@ -1428,10 +1428,10 @@ void code_contractst::assert_function_pointer_obeys_contract(
   comment << "Assert function pointer '"
           << from_expr_using_mode(ns, mode, expr.function_pointer())
           << "' obeys contract '"
-          << from_expr_using_mode(ns, mode, expr.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.contract()});
+    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);
@@ -1448,10 +1448,10 @@ void code_contractst::assume_function_pointer_obeys_contract(
   comment << "Assume function pointer '"
           << from_expr_using_mode(ns, mode, expr.function_pointer())
           << "' obeys contract '"
-          << from_expr_using_mode(ns, mode, expr.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.contract(), loc));
+    expr.function_pointer(), expr.address_of_contract(), loc));
 }
 
 void code_contractst::add_contract_check(