Doxygen the comments describing the abstract domain interface.

Author: martin

src/analyses/ai_domain.h

@@ -27,7 +27,7 @@ class ai_baset;
 class ai_domain_baset
 {
 protected:
-  // The constructor is expected to produce 'false' or 'bottom'
+  /// The constructor is expected to produce 'false' or 'bottom'
   ai_domain_baset()
   {
   }
@@ -39,20 +39,20 @@ class ai_domain_baset
 
   typedef goto_programt::const_targett locationt;
 
-  // how function calls are treated:
-  // a) there is an edge from each call site to the function head
-  // b) there is an edge from the last instruction (END_FUNCTION)
-  //    of the function to the instruction _following_ the call site
-  //    (this also needs to set the LHS, if applicable)
-  //
-  // "this" is the domain before the instruction "from"
-  // "from" is the instruction to be interpretted
-  // "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
-  //
-  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
-  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
-  // PRECONDITION(are_comparable(from,to) ||
-  //              (from->is_function_call() || from->is_end_function())
+  /// how function calls are treated:
+  /// a) there is an edge from each call site to the function head
+  /// b) there is an edge from the last instruction (END_FUNCTION)
+  ///    of the function to the instruction _following_ the call site
+  ///    (this also needs to set the LHS, if applicable)
+  ///
+  /// "this" is the domain before the instruction "from"
+  /// "from" is the instruction to be interpretted
+  /// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
+  ///
+  /// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  /// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
+  /// PRECONDITION(are_comparable(from,to) ||
+  ///              (from->is_function_call() || from->is_end_function())
 
   virtual void transform(
     locationt from,
@@ -69,47 +69,47 @@ class ai_domain_baset
 
   virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
 
-  // no states
+  /// no states
   virtual void make_bottom() = 0;
 
-  // all states -- the analysis doesn't use this,
-  // and domains may refuse to implement it.
+  /// all states -- the analysis doesn't use this,
+  /// and domains may refuse to implement it.
   virtual void make_top() = 0;
 
-  // a reasonable entry-point state
+  /// a reasonable entry-point state
   virtual void make_entry() = 0;
 
   virtual bool is_bottom() const = 0;
 
   virtual bool is_top() const = 0;
 
-  // also add
-  //
-  //   bool merge(const T &b, locationt from, locationt to);
-  //
-  // This computes the join between "this" and "b".
-  // Return true if "this" has changed.
-  // In the usual case, "b" is the updated state after "from"
-  // and "this" is the state before "to".
-  //
-  // PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
-  // PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
-
-  // This method allows an expression to be simplified / evaluated using the
-  // current state.  It is used to evaluate assertions and in program
-  // simplification
-
-  // return true if unchanged
+  /// also add
+  ///
+  ///   bool merge(const T &b, locationt from, locationt to);
+  ///
+  /// This computes the join between "this" and "b".
+  /// Return true if "this" has changed.
+  /// In the usual case, "b" is the updated state after "from"
+  /// and "this" is the state before "to".
+  ///
+  /// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
+  /// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
+
+  /// This method allows an expression to be simplified / evaluated using the
+  /// current state.  It is used to evaluate assertions and in program
+  /// simplification
+
+  /// return true if unchanged
   virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
   {
     return true;
   }
 
-  // Simplifies the expression but keeps it as an l-value
+  /// Simplifies the expression but keeps it as an l-value
   virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
 
-  // Gives a Boolean condition that is true for all values represented by the
-  // domain.  This allows domains to be converted into program invariants.
+  /// Gives a Boolean condition that is true for all values represented by the
+  /// domain.  This allows domains to be converted into program invariants.
   virtual exprt to_predicate(void) const
   {
     if(is_bottom())