Merge pull request #7089 from qinheping/manual-loop-invariant-synthesizer

CONTRACTS: Documenting semantic of loop invariant synthesizers

Author: martin-cs

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

@@ -21,8 +21,10 @@ Author: Qinheping Hu
 class messaget;
 
 /// Enumerative loop invariant synthesizers.
-/// It handles `goto_model` containing only checks instrumented by
+/// It is designed for `goto_model` containing only checks instrumented by
 /// `goto-instrument` with the `--pointer-check` flag.
+/// When other checks present, it will just enumerate candidates and check
+/// if they are valid.
 class enumerative_loop_invariant_synthesizert
   : public loop_invariant_synthesizer_baset
 {
@@ -34,6 +36,8 @@ class enumerative_loop_invariant_synthesizert
   {
   }
 
+  /// This synthesizer guarantees that, with the synthesized loop invariants,
+  /// all checks in the annotated GOTO program pass.
   invariant_mapt synthesize_all() override;
   exprt synthesize(loop_idt loop_id) override;
 

src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h

@@ -38,12 +38,13 @@ class loop_invariant_synthesizer_baset
   }
   virtual ~loop_invariant_synthesizer_baset() = default;
 
-  /// Synthesize loop invariants with which all checks in `goto_model`
-  /// succeed. The result is a map from `loop_idt` ids of loops to `exprt`
-  /// the goto-expression representation of synthesized invariants.
+  /// Synthesize loop invariants that are inductive in the given GOTO program.
+  ///
+  /// The result is a map from `loop_idt` ids of loops to `exprt`
+  /// the GOTO-expression representation of synthesized invariants.
   virtual invariant_mapt synthesize_all() = 0;
 
-  /// Synthesize loop invariant for a specified loop in the `goto_model`
+  /// Synthesize loop invariant for a specified loop in the `goto_model`.
   virtual exprt synthesize(loop_idt) = 0;
 
 protected: