Removes unused methods from contracts module

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

src/goto-instrument/contracts/contracts.cpp

@@ -666,19 +666,6 @@ goto_functionst &code_contractst::get_goto_functions()
   return goto_functions;
 }
 
-exprt code_contractst::create_alias_expression(
-  const exprt &lhs,
-  std::vector<exprt> &aliasable_references)
-{
-  exprt::operandst operands;
-  operands.reserve(aliasable_references.size());
-  for(auto aliasable : aliasable_references)
-  {
-    operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type())));
-  }
-  return disjunction(operands);
-}
-
 void code_contractst::instrument_assign_statement(
   goto_programt::instructionst::iterator &instruction_iterator,
   goto_programt &program,

src/goto-instrument/contracts/contracts.h

@@ -174,13 +174,6 @@ class code_contractst
     goto_programt &,
     assigns_clauset &);
 
-  /// Creates a boolean expression which is true when there exists an expression
-  /// in aliasable_references with the same pointer object and pointer offset as
-  /// the address of lhs.
-  exprt create_alias_expression(
-    const exprt &lhs,
-    std::vector<exprt> &aliasable_references);
-
   /// Apply loop contracts, whenever available, to all loops in `function`.
   /// Loop invariants, loop variants, and loop assigns clauses.
   void apply_loop_contract(