minor improvements to assigns clause checking

Author: SaswatPadhi

src/goto-instrument/contracts/contracts.cpp

@@ -178,8 +178,7 @@ void code_contractst::check_apply_loop_contracts(
   }
   else
   {
-    for(const auto &target : assigns.operands())
-      modifies.insert(target);
+    modifies.insert(assigns.operands().cbegin(), assigns.operands().cend());
 
     // Create snapshots of write set CARs.
     // This must be done before havocing the write set.
@@ -264,13 +263,8 @@ void code_contractst::check_apply_loop_contracts(
   // Copy the loop_head as we would increment the iterator while instrumenting.
   if(assigns.is_not_nil())
   {
-    auto copy_loop_head = loop_head;
     check_frame_conditions(
-      function_name,
-      goto_function.body,
-      copy_loop_head,
-      loop_end,
-      loop_assigns);
+      function_name, goto_function.body, loop_head, loop_end, loop_assigns);
   }
 
   // Generate: assignments to store the multidimensional decreases clause's
@@ -649,8 +643,7 @@ bool code_contractst::apply_function_contract(
 
     // Havoc all targets in the write set
     modifiest modifies;
-    for(const auto &target : targets.operands())
-      modifies.insert(target);
+    modifies.insert(targets.operands().cbegin(), targets.operands().cend());
 
     goto_programt assigns_havoc;
     havoc_assigns_targetst havoc_gen(modifies, ns);
@@ -1000,7 +993,7 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
 void code_contractst::check_frame_conditions(
   const irep_idt &function,
   goto_programt &body,
-  goto_programt::targett &instruction_it,
+  goto_programt::targett instruction_it,
   const goto_programt::targett &instruction_end,
   assigns_clauset &assigns)
 {

src/goto-instrument/contracts/contracts.h

@@ -131,7 +131,7 @@ class code_contractst
   void check_frame_conditions(
     const irep_idt &,
     goto_programt &,
-    goto_programt::targett &,
+    goto_programt::targett,
     const goto_programt::targett &,
     assigns_clauset &);