Fix issues and warnings raised by doxygen

Author: martin

src/analyses/variable-sensitivity/abstract_enviroment.cpp

@@ -343,10 +343,6 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory(
 
 bool abstract_environmentt::merge(const abstract_environmentt &env)
 {
-  // Use the sharing_map's "iterative over all differences" functionality
-  // This should give a significant performance boost
-  // We can strip down to just the things that are in both
-
   // for each entry in the incoming environment we need to either add it
   // if it is new, or merge with the existing key if it is not present
 

src/analyses/variable-sensitivity/abstract_enviroment.h

@@ -132,6 +132,7 @@ class abstract_environmentt
   /// \param top: does the type of the object start as top
   /// \param bottom: does the type of the object start as bottom in
   ///                the two-value domain
+  /// \param ns: the current variable namespace
   ///
   /// \return The abstract object that has been created
   virtual abstract_object_pointert abstract_object_factory(
@@ -143,7 +144,8 @@ class abstract_environmentt
   /// For converting constants in the program
   ///
   /// \param type: the type of the object whose state should be tracked
-  /// \param expr: the starting value of the symbol
+  /// \param e: the starting value of the symbol
+  /// \param ns: the current variable namespace
   ///
   /// \return The abstract object that has been created
   ///
@@ -169,8 +171,6 @@ class abstract_environmentt
   ///
   /// \param havoc_string: diagnostic string to track down havoc causing.
   ///
-  /// \return None
-  ///
   /// Set the domain to top
   virtual void havoc(const std::string &havoc_string);
 
@@ -235,16 +235,18 @@ class abstract_environmentt
   ///             the two-value domain
   /// \param bottom: does the type of the object start as bottom in
   ///                the two-value domain
-  /// \param expr: the starting value of the symbol if top and bottom
-  ///              are both false
+  /// \param e: the starting value of the symbol if top and bottom
+  ///           are both false
+  /// \param environment: the current environment (normally *this)
+  /// \param ns: the current variable namespace
   ///
   /// \return The abstract object that has been created
   abstract_object_pointert abstract_object_factory(
     const typet &type,
     bool top,
     bool bottom,
     const exprt &e,
-    const abstract_environmentt &eviroment,
+    const abstract_environmentt &environment,
     const namespacet &ns) const;
 };
 

src/analyses/variable-sensitivity/abstract_object.h

@@ -149,6 +149,11 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   ///
   /// \param expr: the expression to evaluate and find the result of it.
   ///              This will be the symbol referred to be op0()
+  /// \param operands: an abstract_object (pointer) that represent
+  ///                  the possible values of each operand
+  /// \param environment: the abstract environment in which the
+  ///                     expression is being evaluated
+  /// \param ns: the current variable namespace
   ///
   /// \return Returns the abstract_object representing the result of
   ///         this expression to the maximum precision available.
@@ -266,6 +271,7 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   ///             the sensitivity of the output and is the object compared
   ///             against to choose whether this merge changed anything
   /// \param op2: the second abstract object to merge
+  /// \param out_modifications: reference to a flag indicating modification
   ///
   /// \return The merged abstract object with the same sensitivity as the
   ///         first parameter. out_modifications will be true if the resulting

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -98,6 +98,7 @@ class array_abstract_objectt : public abstract_objectt
   /// \param env: the environment
   /// \param index: the expression used to access the specific value
   ///               in the array
+  /// \param ns: the current variable namespace
   ///
   /// \return An abstract object representing the value in the array
   virtual abstract_object_pointert read_index(

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -35,6 +35,20 @@ class constant_abstract_valuet : public abstract_valuet
   {
   }
 
+  /// Interface for transforms
+  ///
+  /// \param expr: the expression to evaluate and find the result of it.
+  ///              This will be the symbol referred to be op0()
+  /// \param operands: an abstract_object (pointer) that represent
+  ///                  the possible values of each operand
+  /// \param environment: the abstract environment in which the
+  ///                     expression is being evaluated
+  /// \param ns: the current variable namespace
+  ///
+  /// \return Returns the abstract_object representing the result of
+  ///         this expression to the maximum precision available.
+  ///
+  /// Uses the rewriter to constant fold expressions where possible.
   abstract_object_pointert expression_transform(
     const exprt &expr,
     const std::vector<abstract_object_pointert> &operands,

src/analyses/variable-sensitivity/constant_array_abstract_object.h

@@ -93,6 +93,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
   /// \param env: the environment
   /// \param index: the expression used to access the specific value
   ///               in the array
+  /// \param ns: the namespace
   ///
   /// \return An abstract object representing the value in the array
   abstract_object_pointert read_index(
@@ -139,10 +140,12 @@ class constant_array_abstract_objectt : public array_abstract_objectt
   /// object to TOP
   void make_top_internal() override;
 
-  /// Short hand method for creating a top element of the array
+  /// Evaluates the index and tries to convert it to a constant integer
   ///
-  /// \param environment: the abstract environment
+  /// \param index: the index expression showing where to access the array
+  /// \param env: the abstract environment
   /// \param ns: the namespace
+  /// \param out_index: the index if it can be converted to a constant
   ///
   /// \return An abstract object pointer of type type().subtype() (i.e. the
   ///         type of the array's values).
@@ -175,7 +178,7 @@ class constant_array_abstract_objectt : public array_abstract_objectt
 
   /// Short hand method for creating a top element of the array
   ///
-  /// \param environment: the abstract environment
+  /// \param env: the abstract environment
   /// \param ns: the namespace
   ///
   /// \return An abstract object pointer of type type().subtype() (i.e. the

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -14,46 +14,36 @@
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
-/// \param type: the type the abstract_object is representing
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
-  const typet &t)
-  : pointer_abstract_objectt(t)
+  const typet &type)
+  : pointer_abstract_objectt(type)
 {
-  PRECONDITION(t.id() == ID_pointer);
+  PRECONDITION(type.id() == ID_pointer);
 }
 
-/// \param type: the type the abstract_object is representing
-/// \param top: is the abstract_object starting as top
-/// \param bottom: is the abstract_object starting as bottom
-///
-/// Start the abstract object at either top or bottom or neither
-/// Asserts if both top and bottom are true
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
-  const typet &t,
-  bool tp,
-  bool bttm)
-  : pointer_abstract_objectt(t, tp, bttm)
+  const typet &type,
+  bool top,
+  bool bottom)
+  : pointer_abstract_objectt(type, top, bottom)
 {
-  PRECONDITION(t.id() == ID_pointer);
+  PRECONDITION(type.id() == ID_pointer);
 }
 
-/// \param old: the abstract object to copy from
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
   const constant_pointer_abstract_objectt &old)
   : pointer_abstract_objectt(old), value_stack(old.value_stack)
 {
 }
 
-/// \param expr: the expression to use as the starting pointer for
-///              an abstract object
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
-  const exprt &e,
+  const exprt &expr,
   const abstract_environmentt &environment,
   const namespacet &ns)
-  : pointer_abstract_objectt(e, environment, ns),
-    value_stack(e, environment, ns)
+  : pointer_abstract_objectt(expr, environment, ns),
+    value_stack(expr, environment, ns)
 {
-  PRECONDITION(e.type().id() == ID_pointer);
+  PRECONDITION(expr.type().id() == ID_pointer);
   if(value_stack.is_top_value())
   {
     make_top();
@@ -63,14 +53,7 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
     clear_top();
   }
 }
-/// Set this abstract object to be the result of merging this
-/// abstract object. This calls the merge_constant_pointers if
-/// we are trying to merge a constant pointer we use the constant pointer
-/// constant pointer merge
-///
-/// \param other: the pointer being merged
-///
-/// \return Returns the result of the merge.
+
 abstract_object_pointert
 constant_pointer_abstract_objectt::merge(abstract_object_pointert other) const
 {
@@ -87,14 +70,6 @@ constant_pointer_abstract_objectt::merge(abstract_object_pointert other) const
   }
 }
 
-/// Merges two constant pointers. If they are pointing at the same
-/// value, we merge, otherwise we set to top.
-///
-/// \param other: the pointer being merged
-///
-/// \return Returns a new abstract object that is the result of the merge
-///         unless the merge is the same as this abstract object, in which
-///         case it returns this.
 abstract_object_pointert
 constant_pointer_abstract_objectt::merge_constant_pointers(
   const constant_pointer_abstract_pointert other) const
@@ -119,15 +94,6 @@ constant_pointer_abstract_objectt::merge_constant_pointers(
   }
 }
 
-/// To try and find a constant expression for this abstract object
-///
-/// \return Returns an expression representing the value if it can.
-///          Returns a nil expression if it can be more than one value.
-///          Returns null_pointer expression if it must be null
-///          Returns an address_of_exprt with the value set to the
-///          result of to_constant called on whatever abstract object this
-///          pointer is pointing to.
-///
 exprt constant_pointer_abstract_objectt::to_constant() const
 {
   if(is_top() || is_bottom())
@@ -142,12 +108,6 @@ exprt constant_pointer_abstract_objectt::to_constant() const
   }
 }
 
-/// Print the value of the pointer. Either NULL if nullpointer or
-/// ptr -> ( output of what the pointer is pointing to).
-///
-/// \param out: the stream to write to
-/// \param ai: ?
-/// \param ns: ?
 void constant_pointer_abstract_objectt::output(
   std::ostream &out,
   const ai_baset &ai,
@@ -191,15 +151,6 @@ void constant_pointer_abstract_objectt::output(
   }
 }
 
-/// A helper function to dereference a value from a pointer. Providing
-/// the pointer can only be pointing at one thing, returns an abstract
-/// object representing that thing. If null or top will return top.
-///
-/// \param env: the environment
-/// \param ns: the namespace
-///
-/// \return An abstract object representing the value this pointer is pointing
-///         to
 abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
   const abstract_environmentt &env,
   const namespacet &ns) const
@@ -218,23 +169,6 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
   }
 }
 
-/// A helper function to evaluate writing to a pointers value.
-/// If the pointer can only be pointing to one element that it overwrites
-/// that element (or merges if merging_write) with the new value.
-/// If don't know what we are pointing to, we delegate to the parent.
-///
-/// \param environment: the environment
-/// \param ns: the namespace
-/// \param stack: the remaining stack
-/// \param new_value: the value to write to the dereferenced pointer
-/// \param merging_write: is it a merging write (i.e. we aren't certain
-///                       we are writing to this particular pointer therefore
-///                       the value should be merged with whatever is already
-///                       there or we are certain we are writing to this pointer
-///                       so therefore the value can be replaced
-///
-/// \return A modified abstract object representing this pointer after it
-///         has been written to.
 sharing_ptrt<pointer_abstract_objectt>
 constant_pointer_abstract_objectt::write_dereference(
   abstract_environmentt &environment,