Cleans up comments in code_contracts

This commit adds some documentation to code-contracts, as well as
fixing up small errors or confusing wording in existing comments.

Author: klaas

src/goto-instrument/code_contracts.cpp

@@ -56,23 +56,56 @@ class code_contractst
 
   void code_contracts(goto_functionst::goto_functiont &goto_function);
 
+  /// Applies (but does not check) a function contract.
+  /// This will assume that the contract holds, and then use that assumption
+  /// to remove the function call located at target.
+  /// \param goto_program The goto program containing the target callsite.
+  /// \param value_sets A value_setst object containing information about
+  ///   aliasing in the goto program being analyzed
+  /// \param target An iterator pointing to the function call to be removed.
   void apply_contract(
     goto_programt &goto_program,
     value_setst &value_sets,
     goto_programt::targett target);
 
+  /// Applies (but does not check) a loop invariant.
+  /// This will assume that the loop invariant is indeed an invariant, and then
+  /// use that assumption to remove the loop.
+  /// \param goto_function The goto function containing the target loop.
+  /// \param value_sets A value_setst object containing information about
+  ///   aliasing in the goto program being analyzed
+  /// \param loop_head An iterator pointing to the first instruction of the
+  ///   target loop.
+  /// \param loop The loop being removed.
   void apply_invariant(
     goto_functionst::goto_functiont &goto_function,
     value_setst &value_sets,
     const goto_programt::targett loop_head,
     const loopt &loop);
 
+  /// Checks (but does not apply) a function contract.
+  /// This will build a code snippet to be inserted at dest which will check
+  //    that the function contract is satisfied.
+  /// \param function_id The id of the function being checked.
+  /// \param goto_function The goto_function object for the function
+  ///   being checked.
+  /// \param dest An iterator pointing to the place to insert checking code.
   void check_contract(
     const irep_idt &function_id,
     goto_functionst::goto_functiont &goto_function,
     goto_programt &dest);
 
-  void check_apply_invariant(
+  /// Checks and applies a loop invariant
+  /// This will replace the loop with a code snippet (based on the loop) which
+  ///   will check that the loop invariant is indeed ian invariant, and then
+  ///   use that invariant in what follows.
+  /// \param goto_function The goto function containing the target loop.
+  /// \param value_sets A value_setst object containing information about
+  ///   aliasing in the goto program being analyzed
+  /// \param loop_head An iterator pointing to the first instruction of the
+  ///   target loop.
+  /// \param loop The loop being removed.
+ void check_apply_invariant(
     goto_functionst::goto_functiont &goto_function,
     value_setst &value_sets,
     const goto_programt::targett loop_head,
@@ -298,7 +331,7 @@ void code_contractst::apply_invariant(
     inst->make_skip();
   }
 
-  // Now havoc at the loop head. Use insert_swap to
+  // Now havoc at the loop head. Use insert_before_swap to
   // preserve jumps to loop head.
   goto_function.body.insert_before_swap(loop_head, havoc_code);
 
@@ -324,13 +357,15 @@ void code_contractst::check_contract(
     return;
   }
 
-  // build:
-  // if(nondet)
+  // We build the following checking code:
+  // if(nondet) goto end
   //   decl ret
   //   decl parameter1 ...
   //   assume(requires)  [optional]
   //   ret = function(parameter1, ...)
   //   assert(ensures)
+  // end:
+  //   skip
 
   // build skip so that if(nondet) can refer to it
   goto_programt tmp_skip;
@@ -482,7 +517,7 @@ void code_contractst::check_apply_invariant(
     a->source_location.set_comment("Loop invariant violated before entry");
   }
 
-  // havoc variables being written to
+  // havoc variables that can be modified by the loop
   build_havoc_code(loop_head, modifies, havoc_code);
 
   // assume the invariant
@@ -517,7 +552,7 @@ void code_contractst::check_apply_invariant(
     loop_end->guard.make_not();
   }
 
-  // Now havoc at the loop head. Use insert_swap to
+  // Now havoc at the loop head. Use insert_before_swap to
   // preserve jumps to loop head.
   goto_function.body.insert_before_swap(loop_head, havoc_code);
 }

src/goto-instrument/code_contracts.h

@@ -19,4 +19,16 @@ class goto_modelt;
 void apply_code_contracts(goto_modelt &);
 void check_code_contracts(goto_modelt &);
 
+// clang-format off
+#define HELP_APPLY_CODE_CONTRACTS \
+  " --apply-code-contracts       Assume (without checking) that the contracts used in code hold\n" \
+  "                              This will use __CPROVER_requires, __CPROVER_ensures,\n" \
+  "                              and __CPROVER_loop_invariant as assumptions in order to avoid\n" \
+  "                              checking code that is assumed to satisfy a specification.\n"
+#define HELP_CHECK_CODE_CONTRACTS \
+  " --check-code-contracts       Assume (with checking) that the contracts used in code hold.\n" \
+  "                              This differs from --apply-code-contracts in that in addition to\n" \
+  "                              assuming specifications, it checks that they are correct.\n"
+// clang-format on
+
 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1580,6 +1580,8 @@ void goto_instrument_parse_optionst::help()
     " --undefined-function-is-assume-false\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "                              convert each call to an undefined function to assume(false)\n"
+    HELP_APPLY_CODE_CONTRACTS
+    HELP_CHECK_CODE_CONTRACTS
     HELP_REPLACE_FUNCTION_BODY
     "\n"
     "Loop transformations:\n"