Improves description of code_contractst methods

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

src/goto-instrument/contracts/contracts.h

@@ -185,17 +185,24 @@ class code_contractst
     const exprt &lhs,
     std::vector<exprt> &aliasable_references);
 
+  /// Apply loop contracts, whenever available, to all loops in `function`.
+  /// Loop invariants, loop variants, and loop assigns clauses.
   void apply_loop_contract(
     const irep_idt &function,
     goto_functionst::goto_functiont &goto_function);
 
   /// \brief Does the named function have a contract?
   bool has_contract(const irep_idt);
 
+  /// Replaces function calls with assertions based on requires clauses,
+  /// non-deterministic assignments for the write set, and assumptions
+  /// based on ensures clauses.
   bool apply_function_contract(
     goto_programt &goto_program,
     goto_programt::targett target);
 
+  /// Instruments `wrapper_function` adding assumptions based on requires
+  /// clauses and assertions based on ensures clauses.
   void add_contract_check(
     const irep_idt &wrapper_function,
     const irep_idt &mangled_function,