Minor refactor and cleanup on code contracts

We can maintain a `protected` `goto_convertt` field in our class, which would be reusable, rather than trying to instantiate an object for each codet -> goto_programt transformation.

Author: SaswatPadhi

src/goto-instrument/code_contracts.cpp

@@ -158,15 +158,6 @@ static void check_apply_invariants(
     loop_end->set_condition(boolean_negate(loop_end->get_condition()));
 }
 
-void code_contractst::convert_to_goto(
-  const codet &code,
-  const irep_idt &mode,
-  goto_programt &program)
-{
-  goto_convertt converter(symbol_table, log.get_message_handler());
-  converter.goto_convert(code, program, mode);
-}
-
 bool code_contractst::has_contract(const irep_idt fun_name)
 {
   const symbolt &function_symbol = ns.lookup(fun_name);
@@ -322,7 +313,7 @@ code_contractst::create_ensures_instruction(
 
   // Create instructions corresponding to the ensures clause
   goto_programt ensures_program;
-  convert_to_goto(expression, mode, ensures_program);
+  converter.goto_convert(expression, ensures_program, mode);
 
   // return a pair containing:
   // 1. instructions corresponding to the ensures clause
@@ -424,10 +415,10 @@ bool code_contractst::apply_function_contract(
   if(requires.is_not_nil())
   {
     goto_programt assertion;
-    convert_to_goto(
+    converter.goto_convert(
       code_assertt(requires),
-      symbol_table.lookup_ref(function).mode,
-      assertion);
+      assertion,
+      symbol_table.lookup_ref(function).mode);
     auto lines_to_iterate = assertion.instructions.size();
     goto_program.insert_before_swap(target, assertion);
     std::advance(target, lines_to_iterate);
@@ -966,8 +957,8 @@ void code_contractst::add_contract_check(
     replace(requires_cond);
 
     goto_programt assumption;
-    convert_to_goto(
-      code_assumet(requires_cond), function_symbol.mode, assumption);
+    converter.goto_convert(
+      code_assumet(requires_cond), assumption, function_symbol.mode);
     check.destructive_append(assumption);
   }
 

src/goto-instrument/code_contracts.h

@@ -19,6 +19,7 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
@@ -36,8 +37,9 @@ class code_contractst
     : ns(goto_model.symbol_table),
       symbol_table(goto_model.symbol_table),
       goto_functions(goto_model.goto_functions),
-      temporary_counter(0),
-      log(log)
+      log(log),
+      converter(symbol_table, log.get_message_handler())
+
   {
   }
 
@@ -95,20 +97,14 @@ class code_contractst
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 
-  unsigned temporary_counter;
   messaget &log;
+  goto_convertt converter;
 
   std::unordered_set<irep_idt> summarized;
 
   /// \brief Enforce contract of a single function
   bool enforce_contract(const std::string &);
 
-  /// \brief Create goto instructions based on code and add them to program.
-  void convert_to_goto(
-    const codet &code,
-    const irep_idt &mode,
-    goto_programt &program);
-
   /// Insert assertion statements into the goto program to ensure that
   /// assigned memory is within the assignable memory frame.
   bool add_pointer_checks(const std::string &);