Merge pull request diffblue#450 from diffblue/documentation/lvsa-api

[SEC-442] Add get_references_reconstructed

Author: NathanJPhillips

cbmc/src/pointer-analysis/value_set.h

@@ -39,6 +39,14 @@ class namespacet;
 /// pairs of an `exprt` and an optional offset if known (0 for both dynamic
 /// objects in the example given above). RHS expressions are represented using
 /// numbering to avoid storing redundant duplicate expressions.
+///
+/// This object is used both for building and querying a single value set
+///
+/// To query the value set use get_value_set and get_reference_set
+/// get_value_set takes an expression representing a pointer and returns all
+/// the objects pointed to by that pointer
+/// get_reference_set takes an expression reprsenting a value and returns
+/// other expressions that refer to the same memory as the passed expression
 class value_sett
 {
 public:

src/pointer-analysis/local_value_set_analysis.cpp

@@ -959,6 +959,20 @@ void local_value_set_analysist::get_values_reconstructed(
   query_value_set.value_set.get_value_set(expr, dest, ns);
 }
 
+void local_value_set_analysist::get_references_reconstructed(
+  locationt l, const exprt &expr, value_setst::valuest &dest)
+{
+  optionalt<local_value_set_domaint> reconstructed_value_set =
+    reconstruct_value_set(l);
+
+  // If reconstruct returns nothing, no reconstruction was necessary--
+  // query the real value set.
+  const local_value_set_domaint &query_value_set =
+    reconstructed_value_set ? *reconstructed_value_set : (*this)[l];
+
+  query_value_set.value_set.get_reference_set(expr, dest, ns);
+}
+
 optionalt<local_value_set_domaint>
 local_value_set_analysist::reconstruct_value_set(locationt l)
 {

src/pointer-analysis/local_value_set_analysis.h

@@ -30,6 +30,17 @@
 /// external value sets or fields thereof (represented as a suffix, e.g.
 /// `some_static_field.x` or `dynamic_object13.y`).
 /// RHS expressions can be dynamic objects, external value sets or null.
+///
+/// This object is used both for building and querying value sets for each
+/// program location
+///
+/// To query a  value set use get_values_reconstructed and
+/// get_references_reconstructed
+/// get_values_reconstructed takes a location and an expression representing a
+/// pointer and returns all the objects pointed to by that pointer
+/// get_references_reconstructed takes a location and an expression
+/// reprsenting a value and returns other expressions that refer to the same
+/// memory as the passed expression
 class lvsaa_single_external_set_summaryt : public summaryt
 {
 public:
@@ -237,6 +248,9 @@ class local_value_set_analysist
   void get_values_reconstructed(
     locationt l, const exprt &expr, value_setst::valuest &dest);
 
+  void get_references_reconstructed(
+    locationt l, const exprt &expr, value_setst::valuest &dest);
+
   void reconstruct_all_value_sets(const goto_programt &);
 
 protected: