Address more review comments

Author: Owen Jones

src/analyses/ai.cpp

@@ -85,7 +85,7 @@ jsont ai_baset::output_json(
 /// Output the domains for a single function as JSON
 /// \param ns: The namespace
 /// \param goto_program: The goto program
-/// \param identifier: the identifier used to find a symbol to identify the
+/// \param identifier: The identifier used to find a symbol to identify the
 ///   source language
 /// \return The JSON object
 jsont ai_baset::output_json(
@@ -144,7 +144,7 @@ xmlt ai_baset::output_xml(
 /// Output the domains for a single function as XML
 /// \param ns: The namespace
 /// \param goto_program: The goto program
-/// \param identifier: the identifier used to find a symbol to identify the
+/// \param identifier: The identifier used to find a symbol to identify the
 ///   source language
 /// \return The XML object
 xmlt ai_baset::output_xml(
@@ -341,7 +341,7 @@ bool ai_baset::do_function_call(
 
   if(!goto_function.body_available())
   {
-    // if we don't have a body, we just do an edge call -> return
+    // If we don't have a body, we just do an edge call -> return
     std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
     tmp_state->transform(
       calling_function_identifier,

src/analyses/ai.h

@@ -96,21 +96,21 @@ class ai_baset
   /// use \ref get_state or \ref find_state to access the actual underlying
   /// state.
   /// PRECONDITION(l is dereferenceable)
-  /// \param l: The location we want the domain before
-  /// \return The domain before `l`. We return a pointer to a copy as the method
-  ///   should be const and there are some non-trivial cases including merging
-  ///   domains, etc.
+  /// \param l: The location before which we want the abstract state
+  /// \return The abstract state before `l`. We return a pointer to a copy as
+  ///   the method should be const and there are some non-trivial cases
+  ///   including merging abstract states, etc.
   virtual std::unique_ptr<statet> abstract_state_before(locationt l) const = 0;
 
   /// Get a copy of the abstract state after the given instruction, without
   /// needing to know what kind of domain or history is used. Note: intended
   /// for users of the abstract interpreter; derived classes should
   /// use \ref get_state or \ref find_state to access the actual underlying
   /// state.
-  /// \param l: The location we want the domain after
-  /// \return The domain after `l`. We return a pointer to a copy as the method
-  ///   should be const and there are some non-trivial cases including merging
-  ///   domains, etc.
+  /// \param l: The location before which we want the abstract state
+  /// \return The abstract state after `l`. We return a pointer to a copy as
+  ///   the method should be const and there are some non-trivial cases
+  ///   including merging abstract states, etc.
   virtual std::unique_ptr<statet> abstract_state_after(locationt l) const
   {
     /// PRECONDITION(l is dereferenceable && std::next(l) is dereferenceable)
@@ -119,18 +119,18 @@ class ai_baset
     return abstract_state_before(std::next(l));
   }
 
-  /// Reset the domain
+  /// Reset the abstract state
   virtual void clear()
   {
   }
 
-  /// Output the domains for a whole program
+  /// Output the abstract states for a whole program
   virtual void output(
     const namespacet &ns,
     const goto_functionst &goto_functions,
     std::ostream &out) const;
 
-  /// Output the domains for a whole program
+  /// Output the abstract states for a whole program
   void output(
     const goto_modelt &goto_model,
     std::ostream &out) const
@@ -139,7 +139,7 @@ class ai_baset
     output(ns, goto_model.goto_functions, out);
   }
 
-  /// Output the domains for a function
+  /// Output the abstract states for a function
   void output(
     const namespacet &ns,
     const goto_programt &goto_program,
@@ -148,7 +148,7 @@ class ai_baset
     output(ns, goto_program, "", out);
   }
 
-  /// Output the domains for a function
+  /// Output the abstract states for a function
   void output(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function,
@@ -157,57 +157,57 @@ class ai_baset
     output(ns, goto_function.body, "", out);
   }
 
-  /// Output the domains for the whole program as JSON
+  /// Output the abstract states for the whole program as JSON
   virtual jsont output_json(
     const namespacet &ns,
     const goto_functionst &goto_functions) const;
 
-  /// Output the domains for a whole program as JSON
+  /// Output the abstract states for a whole program as JSON
   jsont output_json(
     const goto_modelt &goto_model) const
   {
     const namespacet ns(goto_model.symbol_table);
     return output_json(ns, goto_model.goto_functions);
   }
 
-  /// Output the domains for a single function as JSON
+  /// Output the abstract states for a single function as JSON
   jsont output_json(
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
     return output_json(ns, goto_program, "");
   }
 
-  /// Output the domains for a single function as JSON
+  /// Output the abstract states for a single function as JSON
   jsont output_json(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
   {
     return output_json(ns, goto_function.body, "");
   }
 
-  /// Output the domains for the whole program as XML
+  /// Output the abstract states for the whole program as XML
   virtual xmlt output_xml(
     const namespacet &ns,
     const goto_functionst &goto_functions) const;
 
-  /// Output the domains for the whole program as XML
+  /// Output the abstract states for the whole program as XML
   xmlt output_xml(
     const goto_modelt &goto_model) const
   {
     const namespacet ns(goto_model.symbol_table);
     return output_xml(ns, goto_model.goto_functions);
   }
 
-  /// Output the domains for a single function as XML
+  /// Output the abstract states for a single function as XML
   xmlt output_xml(
     const namespacet &ns,
     const goto_programt &goto_program) const
   {
     return output_xml(ns, goto_program, "");
   }
 
-  /// Output the domains for a single function as XML
+  /// Output the abstract states for a single function as XML
   xmlt output_xml(
     const namespacet &ns,
     const goto_functionst::goto_functiont &goto_function) const
@@ -216,30 +216,33 @@ class ai_baset
   }
 
 protected:
-  /// Initialize all the domains for a single function. Override this to do
-  /// custom per-domain initialization.
+  /// Initialize all the abstract states for a single function. Override this to
+  /// do custom per-domain initialization.
   virtual void initialize(const goto_programt &goto_program);
 
-  /// Initialize all the domains for a single function.
+  /// Initialize all the abstract states for a single function.
   virtual void initialize(const goto_functionst::goto_functiont &goto_function);
 
-  /// Initialize all the domains for a whole program. Override this to do custom
-  /// per-analysis initialization.
+  /// Initialize all the abstract states for a whole program. Override this to
+  /// do custom per-analysis initialization.
   virtual void initialize(const goto_functionst &goto_functions);
 
-  /// Override this to add a cleanup step after fixedpoint has run
+  /// Override this to add a cleanup or post-processing step after fixedpoint
+  /// has run
   virtual void finalize();
 
-  /// Ensure the entry point to a single function has a reasonable state
-  void entry_state(const goto_programt &goto_functions);
+  /// Set the abstract state of the entry location of a single function to the
+  /// entry state required by the analysis
+  void entry_state(const goto_programt &goto_program);
 
-  /// Ensure the entry point to a whole program has a reasonable state
-  void entry_state(const goto_functionst &goto_program);
+  /// Set the abstract state of the entry location of a whole program to the
+  /// entry state required by the analysis
+  void entry_state(const goto_functionst &goto_functions);
 
-  /// Output the domains for a single function
+  /// Output the abstract states for a single function
   /// \param ns: The namespace
   /// \param goto_program: The goto program
-  /// \param identifier: the identifier used to find a symbol to identify the
+  /// \param identifier: The identifier used to find a symbol to identify the
   ///   source language
   /// \param out: The ostream to direct output to
   virtual void output(
@@ -248,21 +251,21 @@ class ai_baset
     const irep_idt &identifier,
     std::ostream &out) const;
 
-  /// Output the domains for a single function as JSON
+  /// Output the abstract states for a single function as JSON
   /// \param ns: The namespace
   /// \param goto_program: The goto program
-  /// \param identifier: the identifier used to find a symbol to identify the
+  /// \param identifier: The identifier used to find a symbol to identify the
   ///   source language
   /// \return The JSON object
   virtual jsont output_json(
     const namespacet &ns,
     const goto_programt &goto_program,
     const irep_idt &identifier) const;
 
-  /// Output the domains for a single function as XML
+  /// Output the abstract states for a single function as XML
   /// \param ns: The namespace
   /// \param goto_program: The goto program
-  /// \param identifier: the identifier used to find a symbol to identify the
+  /// \param identifier: The identifier used to find a symbol to identify the
   ///   source language
   /// \return The XML object
   virtual xmlt output_xml(

src/analyses/ai_domain.cpp

@@ -35,8 +35,8 @@ xmlt ai_domain_baset::output_xml(const ai_baset &ai, const namespacet &ns) const
 /// an assignment. This for example won't simplify symbols to their values, but
 /// does simplify indices in arrays, members of structs and dereferencing of
 /// pointers
-/// \param condition: the expression to simplify
-/// \param ns: the namespace
+/// \param condition: The expression to simplify
+/// \param ns: The namespace
 /// \return True if condition did not change. False otherwise. condition will be
 ///   updated with the simplified condition if it has worked
 bool ai_domain_baset::ai_simplify_lhs(exprt &condition, const namespacet &ns)