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

@@ -17,7 +17,6 @@ Date: February 2016
 
 #include <analyses/local_may_alias.h>
 
-#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/remove_skip.h>
 
 #include <util/arith_tools.h>
@@ -155,15 +154,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);
@@ -335,10 +325,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);
@@ -364,10 +354,10 @@ bool code_contractst::apply_function_contract(
   if(ensures.is_not_nil())
   {
     goto_programt assumption;
-    convert_to_goto(
+    converter.goto_convert(
       code_assumet(ensures),
-      symbol_table.lookup_ref(function).mode,
-      assumption);
+      assumption,
+      symbol_table.lookup_ref(function).mode);
     auto lines_to_iterate = assumption.instructions.size();
     goto_program.insert_before_swap(target, assumption);
     std::advance(target, lines_to_iterate);
@@ -858,8 +848,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);
   }
 
@@ -874,8 +864,8 @@ void code_contractst::add_contract_check(
   if(ensures.is_not_nil())
   {
     goto_programt assertion;
-    convert_to_goto(
-      code_assertt(ensures_cond), function_symbol.mode, assertion);
+    converter.goto_convert(
+      code_assertt(ensures_cond), assertion, function_symbol.mode);
     check.destructive_append(assertion);
   }
 

src/goto-instrument/code_contracts.h

@@ -18,6 +18,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>
 
@@ -35,8 +36,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())
+
   {
   }
 
@@ -94,20 +96,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 &);