Format

Author: ArenBabikian

src/goto-instrument/code_contracts.cpp

@@ -98,7 +98,10 @@ void code_contractst::check_apply_invariants(
     return;
 
   // Add quantified variables in contracts to the symbol map
-  //TODO improve the structure below
+  // TODO improve the structure below wrt the replace_symbolt object
+  //   In the current implementation, the add_quantified_variable
+  //   function requires a replace_symbolt object as input, which is
+  //   irrelevant in the context of loop contracts.
   replace_symbolt replace;
   code_contractst::add_quantified_variable(invariant, replace, mode);
 

src/goto-instrument/code_contracts.h

@@ -18,9 +18,9 @@ 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>
-#include <goto-programs/goto_convert_class.h>
 
 #include <goto-instrument/loop_utils.h>
 
@@ -185,12 +185,12 @@ class code_contractst
     irep_idt mode);
 
   void check_apply_invariants(
-  goto_functionst::goto_functiont &goto_function,
-  goto_convertt &converter,
-  const local_may_aliast &local_may_alias,
-  const goto_programt::targett loop_head,
-  const loopt &loop,
-  const irep_idt &mode);
+    goto_functionst::goto_functiont &goto_function,
+    goto_convertt &converter,
+    const local_may_aliast &local_may_alias,
+    const goto_programt::targett loop_head,
+    const loopt &loop,
+    const irep_idt &mode);
 };
 
 #define FLAG_REPLACE_CALL "replace-call-with-contract"