From 318d49a0d3a22743ffa13a5c07171465fd2dff61 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 May 2019 11:22:20 +0100
Subject: [PATCH 1/7] get_value_set takes expr by copy

This avoids having to create a tmp expression and allows moving into the function.
---
 src/pointer-analysis/value_set.cpp | 11 +++++------
 src/pointer-analysis/value_set.h   |  4 ++--
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index b7a40dc36bf..b8e5a542b97 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -352,12 +352,12 @@ bool value_sett::eval_pointer_offset(
 }
 
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
 {
   object_mapt object_map;
-  get_value_set(expr, object_map, ns, false);
+  get_value_set(std::move(expr), object_map, ns, false);
 
   for(object_map_dt::const_iterator
       it=object_map.read().begin();
@@ -373,16 +373,15 @@ void value_sett::get_value_set(
 }
 
 void value_sett::get_value_set(
-  const exprt &expr,
+  exprt expr,
   object_mapt &dest,
   const namespacet &ns,
   bool is_simplified) const
 {
-  exprt tmp(expr);
   if(!is_simplified)
-    simplify(tmp, ns);
+    simplify(expr, ns);
 
-  get_value_set_rec(tmp, dest, "", tmp.type(), ns);
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
 }
 
 /// Check if 'suffix' starts with 'field'.
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 6ff79285d1c..4a141424237 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -264,7 +264,7 @@ class value_sett
   /// \param [out] dest: assigned a set of expressions that `expr` may point to
   /// \param ns: global namespace
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
 
@@ -461,7 +461,7 @@ class value_sett
   /// \param ns: global namespace
   /// \param is_simplified: if false, simplify `expr` before reading.
   void get_value_set(
-    const exprt &expr,
+    exprt expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;

From b633d6d829808b0028a9e1311295c349f0fec36f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 May 2019 11:31:51 +0100
Subject: [PATCH 2/7] Deprecate offset_is_zero

This is unused
---
 src/pointer-analysis/value_set.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 4a141424237..fc901b627b7 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -80,6 +80,7 @@ class value_sett
   /// Represents the offset into an object: either a unique integer offset,
   /// or an unknown value, represented by `!offset`.
   typedef optionalt<mp_integer> offsett;
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   bool offset_is_zero(const offsett &offset) const
   {
     return offset && offset->is_zero();

From 01dff419ef630551fdac273f32e38eb16e2dc5a5 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 May 2019 11:35:11 +0100
Subject: [PATCH 3/7] Deprecate value_sett::get

This is not implemented.
---
 src/pointer-analysis/value_set.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index fc901b627b7..24ebfc17252 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -237,6 +237,7 @@ class value_sett
 
   /// Set of expressions; only used for the `get` API, not for internal
   /// data representation.
+  DEPRECATED(SINCE(2019, 05, 22, "Only used in deprecated function"))
   typedef std::set<exprt> expr_sett;
 
   /// Set of dynamic object numbers, equivalent to a set of
@@ -270,6 +271,7 @@ class value_sett
     const namespacet &ns) const;
 
   /// Appears to be unimplemented.
+  DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
   expr_sett &get(const irep_idt &identifier, const std::string &suffix);
 
   void clear()

From e1eb12e7e440867ba01d4aa686b8fe6b7100c93c Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 May 2019 11:36:47 +0100
Subject: [PATCH 4/7] Deprecate dynamic_object_id_sett

This is unused.
---
 src/pointer-analysis/value_set.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 24ebfc17252..4d08fe5b236 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -243,6 +243,7 @@ class value_sett
   /// Set of dynamic object numbers, equivalent to a set of
   /// `dynamic_object_exprt`s with corresponding IDs. Used only in internal
   /// implementation details.
+  DEPRECATED(SINCE(2019, 05, 22, "Unused"))
   typedef std::set<unsigned int> dynamic_object_id_sett;
 
   /// Map representing the entire value set, mapping from string LHS IDs

From 1e06eda6d23f275bb3350cf0c4e55a0a2249747b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 May 2019 12:14:08 +0100
Subject: [PATCH 5/7] Add versions of get_value_set returning a value

These return the computed value, which makes the information flow
clearer in the program.
We deprecate at the same time the functions from the previous version.
---
 src/goto-symex/postcondition.cpp              |  4 +--
 src/goto-symex/precondition.cpp               |  5 ++-
 src/goto-symex/symex_dereference_state.cpp    |  7 +++++
 src/goto-symex/symex_dereference_state.h      |  3 ++
 src/pointer-analysis/dereference_callback.h   |  3 ++
 .../goto_program_dereference.cpp              | 10 ++++++
 .../goto_program_dereference.h                |  3 ++
 src/pointer-analysis/value_set.cpp            | 31 +++++++++++++++----
 src/pointer-analysis/value_set.h              | 31 +++++++++++++------
 src/pointer-analysis/value_set_analysis.h     |  8 +++++
 .../value_set_analysis_fi.cpp                 | 14 +++++++++
 src/pointer-analysis/value_set_analysis_fi.h  |  6 ++++
 src/pointer-analysis/value_set_fi.cpp         | 20 +++++++++---
 src/pointer-analysis/value_set_fi.h           |  3 ++
 src/pointer-analysis/value_sets.h             |  7 +++++
 15 files changed, 130 insertions(+), 25 deletions(-)

diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 317297c6c7e..168712c5ee6 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -160,8 +160,8 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    value_setst::valuest expr_set;
-    value_set.get_value_set(to_dereference_expr(expr).pointer(), expr_set, ns);
+    value_setst::valuest expr_set =
+      value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index dd0ccb50296..5ac855872ee 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -112,9 +112,8 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    value_setst::valuest expr_set;
-    value_sets.get_values(
-      SSA_step.source.function_id, target, deref_expr.pointer(), expr_set);
+    value_setst::valuest expr_set = value_sets.get_values(
+      SSA_step.source.function_id, target, deref_expr.pointer());
     std::unordered_set<irep_idt> symbols;
 
     for(value_setst::valuest::const_iterator
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index 28dc90b916f..76711040e98 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -107,3 +107,10 @@ void symex_dereference_statet::get_value_set(
   std::cout << "**************************\n";
 #endif
 }
+
+/// Just forwards a value-set query to `state.value_set`
+value_setst::valuest
+symex_dereference_statet::get_value_set(const exprt &expr) const
+{
+  return state.value_set.get_value_set(expr, ns);
+}
diff --git a/src/goto-symex/symex_dereference_state.h b/src/goto-symex/symex_dereference_state.h
index b0c0e15682a..f561c8cd684 100644
--- a/src/goto-symex/symex_dereference_state.h
+++ b/src/goto-symex/symex_dereference_state.h
@@ -34,9 +34,12 @@ class symex_dereference_statet:
   goto_symext::statet &state;
   const namespacet &ns;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;
 
+  value_setst::valuest get_value_set(const exprt &expr) const override;
+
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 };
 
diff --git a/src/pointer-analysis/dereference_callback.h b/src/pointer-analysis/dereference_callback.h
index f39da7f75b4..537b1800796 100644
--- a/src/pointer-analysis/dereference_callback.h
+++ b/src/pointer-analysis/dereference_callback.h
@@ -29,9 +29,12 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt() = default;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   virtual void
   get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
+  virtual value_setst::valuest get_value_set(const exprt &expr) const = 0;
+
   virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
 };
 
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 7b75c1bbfe6..fad8b3ab01f 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -147,6 +147,16 @@ void goto_program_dereferencet::get_value_set(
   value_sets.get_values(current_function, current_target, expr, dest);
 }
 
+/// Gets the value set corresponding to the current target and
+/// expression \p expr.
+/// \param expr: an expression
+/// \return the value set
+std::list<exprt>
+goto_program_dereferencet::get_value_set(const exprt &expr) const
+{
+  return value_sets.get_values(current_function, current_target, expr);
+}
+
 /// Remove dereference expressions contained in `expr`.
 /// \param expr: an expression
 /// \param checks_only: when true, execute the substitution on a copy of expr
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index 2bce9d45380..96ec32cb999 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -65,9 +65,12 @@ class goto_program_dereferencet:protected dereference_callbackt
 
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
+  std::list<exprt> get_value_set(const exprt &expr) const override;
+
   void dereference_instruction(
     goto_programt::targett target,
     bool checks_only=false);
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index b8e5a542b97..8dfddf4de1b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 
 #include <langapi/language_util.h>
+#include <util/range.h>
 
 #ifdef DEBUG
 #include <iostream>
@@ -308,8 +309,7 @@ bool value_sett::eval_pointer_offset(
   {
     assert(expr.operands().size()==1);
 
-    object_mapt reference_set;
-    get_value_set(expr.op0(), reference_set, ns, true);
+    const object_mapt reference_set = get_value_set(expr.op0(), ns, true);
 
     exprt new_expr;
     mp_integer previous_offset=0;
@@ -356,8 +356,7 @@ void value_sett::get_value_set(
   value_setst::valuest &dest,
   const namespacet &ns) const
 {
-  object_mapt object_map;
-  get_value_set(std::move(expr), object_map, ns, false);
+  object_mapt object_map = get_value_set(std::move(expr), ns, false);
 
   for(object_map_dt::const_iterator
       it=object_map.read().begin();
@@ -372,6 +371,14 @@ void value_sett::get_value_set(
   #endif
 }
 
+std::list<exprt>
+value_sett::get_value_set(exprt expr, const namespacet &ns) const
+{
+  const object_mapt object_map = get_value_set(std::move(expr), ns, false);
+  return make_range(object_map.read())
+    .map([&](const object_map_dt::value_type &pair) { return to_expr(pair); });
+}
+
 void value_sett::get_value_set(
   exprt expr,
   object_mapt &dest,
@@ -384,6 +391,19 @@ void value_sett::get_value_set(
   get_value_set_rec(expr, dest, "", expr.type(), ns);
 }
 
+value_sett::object_mapt value_sett::get_value_set(
+  exprt expr,
+  const namespacet &ns,
+  bool is_simplified) const
+{
+  if(!is_simplified)
+    simplify(expr, ns);
+
+  object_mapt dest;
+  get_value_set_rec(expr, dest, "", expr.type(), ns);
+  return dest;
+}
+
 /// Check if 'suffix' starts with 'field'.
 /// Suffix is delimited by periods and '[]' (array access) tokens, so we're
 /// looking for ".field($|[]|.)"
@@ -1303,8 +1323,7 @@ void value_sett::assign(
   else
   {
     // basic type
-    object_mapt values_rhs;
-    get_value_set(rhs, values_rhs, ns, is_simplified);
+    object_mapt values_rhs = get_value_set(rhs, ns, is_simplified);
 
     // Permit custom subclass to alter the read values prior to write:
     adjust_assign_rhs_values(rhs, ns, values_rhs);
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 4d08fe5b236..e3e51136184 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -261,16 +261,22 @@ class value_sett
   /// `entryt` fields.
   typedef sharing_mapt<irep_idt, entryt> valuest;
 
-  /// Gets values pointed to by `expr`, including following dereference
+  /// Gets values pointed to by \p expr, including following dereference
   /// operators (i.e. this is not a simple lookup in `valuest`).
-  /// \param expr: query expression
-  /// \param [out] dest: assigned a set of expressions that `expr` may point to
-  /// \param ns: global namespace
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use get_value_set(exprt, const namespacet &) instead"))
   void get_value_set(
     exprt expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
 
+  /// Gets values pointed to by `expr`, including following dereference
+  /// operators (i.e. this is not a simple lookup in `valuest`).
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \return list of expressions that `expr` may point to
+  std::list<exprt> get_value_set(exprt expr, const namespacet &ns) const;
+
   /// Appears to be unimplemented.
   DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
   expr_sett &get(const irep_idt &identifier, const std::string &suffix);
@@ -458,18 +464,25 @@ class value_sett
   void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns);
 
 protected:
-  /// Reads the set of objects pointed to by `expr`, including making
+  /// Reads the set of objects pointed to by \p expr, including making
   /// recursive lookups for dereference operations etc.
-  /// \param expr: query expression
-  /// \param [out] dest: overwritten by the set of object numbers pointed to
-  /// \param ns: global namespace
-  /// \param is_simplified: if false, simplify `expr` before reading.
+  DEPRECATED(
+    SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
   void get_value_set(
     exprt expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;
 
+  /// Reads the set of objects pointed to by `expr`, including making
+  /// recursive lookups for dereference operations etc.
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \param is_simplified: if false, simplify `expr` before reading.
+  /// \return the set of object numbers pointed to
+  object_mapt
+  get_value_set(exprt expr, const namespacet &ns, bool is_simplified) const;
+
   /// See the other overload of `get_reference_set`. This one returns object
   /// numbers and offsets instead of expressions.
   void get_reference_set(
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 4f391c7b8bb..3a95476f69e 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -65,6 +65,7 @@ class value_set_analysis_templatet:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   void get_values(
     const irep_idt &,
     locationt l,
@@ -73,6 +74,13 @@ class value_set_analysis_templatet:
   {
     (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
   }
+
+  // interface value_sets
+  std::list<exprt>
+  get_values(const irep_idt &, locationt l, const exprt &expr) override
+  {
+    return (*this)[l].value_set.get_value_set(expr, baset::ns);
+  }
 };
 
 typedef
diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp
index c6b59e41986..46e46c54d13 100644
--- a/src/pointer-analysis/value_set_analysis_fi.cpp
+++ b/src/pointer-analysis/value_set_analysis_fi.cpp
@@ -195,3 +195,17 @@ bool value_set_analysis_fit::check_type(const typet &type)
 
   return false;
 }
+
+std::list<exprt> value_set_analysis_fit::get_values(
+  const irep_idt &function_id,
+  flow_insensitive_analysis_baset::locationt l,
+  const exprt &expr)
+{
+  state.value_set.from_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.to_function =
+    state.value_set.function_numbering.number(function_id);
+  state.value_set.from_target_index = l->location_number;
+  state.value_set.to_target_index = l->location_number;
+  return state.value_set.get_value_set(expr, ns);
+}
diff --git a/src/pointer-analysis/value_set_analysis_fi.h b/src/pointer-analysis/value_set_analysis_fi.h
index ec6b9d99a81..41c3ab59293 100644
--- a/src/pointer-analysis/value_set_analysis_fi.h
+++ b/src/pointer-analysis/value_set_analysis_fi.h
@@ -58,6 +58,7 @@ class value_set_analysis_fit:
 
 public:
   // interface value_sets
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning list instead"))
   void get_values(
     const irep_idt &function_id,
     locationt l,
@@ -72,6 +73,11 @@ class value_set_analysis_fit:
     state.value_set.to_target_index = l->location_number;
     state.value_set.get_value_set(expr, dest, ns);
   }
+
+  std::list<exprt> get_values(
+    const irep_idt &function_id,
+    locationt l,
+    const exprt &expr) override;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_FI_H
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 224059c779f..a965f82746a 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "value_set_fi.h"
 
 #include <cassert>
+#include <iterator>
 #include <ostream>
 
 #include <util/symbol_table.h>
@@ -296,6 +297,12 @@ void value_set_fit::get_value_set(
   const exprt &expr,
   std::list<exprt> &value_set,
   const namespacet &ns) const
+{
+  value_set = get_value_set(expr, ns);
+}
+
+std::list<exprt>
+value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
 {
   object_mapt object_map;
   get_value_set(expr, object_map, ns);
@@ -336,21 +343,24 @@ void value_set_fit::get_value_set(
       flat_map.write()[it->first]=it->second;
   }
 
+  std::list<exprt> result;
   forall_objects(fit, flat_map.read())
-    value_set.push_back(to_expr(*fit));
+    result.push_back(to_expr(*fit));
 
-  #if 0
+#if 0
   // Sanity check!
   for(std::list<exprt>::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
     assert(it->type().id()!="#REF");
-  #endif
+#endif
 
-  #if 0
+#if 0
   for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
     std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
-  #endif
+#endif
+
+  return result;
 }
 
 void value_set_fit::get_value_set(
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index d919c554ad1..0e23f52100c 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -205,11 +205,14 @@ class value_set_fit
   typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
   #endif
 
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
   void get_value_set(
     const exprt &expr,
     std::list<exprt> &dest,
     const namespacet &ns) const;
 
+  std::list<exprt> get_value_set(const exprt &expr, const namespacet &ns) const;
+
   expr_sett &get(
     const idt &identifier,
     const std::string &suffix);
diff --git a/src/pointer-analysis/value_sets.h b/src/pointer-analysis/value_sets.h
index 24153a71781..f11343e0fc8 100644
--- a/src/pointer-analysis/value_sets.h
+++ b/src/pointer-analysis/value_sets.h
@@ -28,12 +28,19 @@ class value_setst
   typedef std::list<exprt> valuest;
 
   // this is not const to allow a lazy evaluation
+  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
   virtual void get_values(
     const irep_idt &function_id,
     goto_programt::const_targett l,
     const exprt &expr,
     valuest &dest) = 0;
 
+  // this is not const to allow a lazy evaluation
+  virtual valuest get_values(
+    const irep_idt &function_id,
+    goto_programt::const_targett l,
+    const exprt &expr) = 0;
+
   virtual ~value_setst()
   {
   }

From 8d497eb59fdc30fa4f1f68f411a5f644a4089998 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 24 May 2019 14:09:13 +0100
Subject: [PATCH 6/7] Use vector instead of list for get_value_set result

vectors are generally more efficient than list, unless we use
concatenation or insertion which doesn't appear to be case here.
---
 src/goto-symex/postcondition.cpp                  |  9 +++------
 src/goto-symex/precondition.cpp                   |  9 +++------
 src/goto-symex/symex_dereference_state.cpp        |  2 +-
 src/goto-symex/symex_dereference_state.h          |  4 ++--
 src/pointer-analysis/dereference_callback.h       |  4 ++--
 src/pointer-analysis/goto_program_dereference.cpp |  2 +-
 src/pointer-analysis/goto_program_dereference.h   |  4 ++--
 src/pointer-analysis/value_set.cpp                |  2 +-
 src/pointer-analysis/value_set.h                  |  2 +-
 src/pointer-analysis/value_set_analysis.h         |  2 +-
 src/pointer-analysis/value_set_analysis_fi.cpp    |  2 +-
 src/pointer-analysis/value_set_analysis_fi.h      |  2 +-
 src/pointer-analysis/value_set_fi.cpp             | 10 +++++++---
 src/pointer-analysis/value_set_fi.h               |  5 +++--
 src/pointer-analysis/value_sets.h                 |  4 ++--
 15 files changed, 31 insertions(+), 32 deletions(-)

diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 168712c5ee6..f565f84cf9e 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -160,16 +160,13 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    value_setst::valuest expr_set =
+    std::vector<exprt> expr_set =
       value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
+    for(const exprt &e : expr_set)
     {
-      const exprt tmp = get_original_name(*it);
+      const exprt tmp = get_original_name(e);
       find_symbols(tmp, symbols);
     }
 
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 5ac855872ee..8c367c5bc2c 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -112,15 +112,12 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    value_setst::valuest expr_set = value_sets.get_values(
+    const std::vector<exprt> expr_set = value_sets.get_values(
       SSA_step.source.function_id, target, deref_expr.pointer());
     std::unordered_set<irep_idt> symbols;
 
-    for(value_setst::valuest::const_iterator
-        it=expr_set.begin();
-        it!=expr_set.end();
-        it++)
-      find_symbols(*it, symbols);
+    for(const exprt &e : expr_set)
+      find_symbols(e, symbols);
 
     if(symbols.find(lhs_identifier)!=symbols.end())
     {
diff --git a/src/goto-symex/symex_dereference_state.cpp b/src/goto-symex/symex_dereference_state.cpp
index 76711040e98..5828566db4f 100644
--- a/src/goto-symex/symex_dereference_state.cpp
+++ b/src/goto-symex/symex_dereference_state.cpp
@@ -109,7 +109,7 @@ void symex_dereference_statet::get_value_set(
 }
 
 /// Just forwards a value-set query to `state.value_set`
-value_setst::valuest
+std::vector<exprt>
 symex_dereference_statet::get_value_set(const exprt &expr) const
 {
   return state.value_set.get_value_set(expr, ns);
diff --git a/src/goto-symex/symex_dereference_state.h b/src/goto-symex/symex_dereference_state.h
index f561c8cd684..174fb0a9ee5 100644
--- a/src/goto-symex/symex_dereference_state.h
+++ b/src/goto-symex/symex_dereference_state.h
@@ -34,11 +34,11 @@ class symex_dereference_statet:
   goto_symext::statet &state;
   const namespacet &ns;
 
-  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void get_value_set(const exprt &expr, value_setst::valuest &value_set)
     const override;
 
-  value_setst::valuest get_value_set(const exprt &expr) const override;
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
 
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 };
diff --git a/src/pointer-analysis/dereference_callback.h b/src/pointer-analysis/dereference_callback.h
index 537b1800796..7a245fcd409 100644
--- a/src/pointer-analysis/dereference_callback.h
+++ b/src/pointer-analysis/dereference_callback.h
@@ -29,11 +29,11 @@ class dereference_callbackt
 public:
   virtual ~dereference_callbackt() = default;
 
-  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   virtual void
   get_value_set(const exprt &expr, value_setst::valuest &value_set) const = 0;
 
-  virtual value_setst::valuest get_value_set(const exprt &expr) const = 0;
+  virtual std::vector<exprt> get_value_set(const exprt &expr) const = 0;
 
   virtual const symbolt *get_or_create_failed_symbol(const exprt &expr) = 0;
 };
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index fad8b3ab01f..600463bc6bf 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -151,7 +151,7 @@ void goto_program_dereferencet::get_value_set(
 /// expression \p expr.
 /// \param expr: an expression
 /// \return the value set
-std::list<exprt>
+std::vector<exprt>
 goto_program_dereferencet::get_value_set(const exprt &expr) const
 {
   return value_sets.get_values(current_function, current_target, expr);
diff --git a/src/pointer-analysis/goto_program_dereference.h b/src/pointer-analysis/goto_program_dereference.h
index 96ec32cb999..eee508c2bae 100644
--- a/src/pointer-analysis/goto_program_dereference.h
+++ b/src/pointer-analysis/goto_program_dereference.h
@@ -65,11 +65,11 @@ class goto_program_dereferencet:protected dereference_callbackt
 
   const symbolt *get_or_create_failed_symbol(const exprt &expr) override;
 
-  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   void
   get_value_set(const exprt &expr, value_setst::valuest &dest) const override;
 
-  std::list<exprt> get_value_set(const exprt &expr) const override;
+  std::vector<exprt> get_value_set(const exprt &expr) const override;
 
   void dereference_instruction(
     goto_programt::targett target,
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 8dfddf4de1b..ff16df24ae7 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -371,7 +371,7 @@ void value_sett::get_value_set(
   #endif
 }
 
-std::list<exprt>
+std::vector<exprt>
 value_sett::get_value_set(exprt expr, const namespacet &ns) const
 {
   const object_mapt object_map = get_value_set(std::move(expr), ns, false);
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index e3e51136184..3fd5440a26a 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -275,7 +275,7 @@ class value_sett
   /// \param expr: query expression
   /// \param ns: global namespace
   /// \return list of expressions that `expr` may point to
-  std::list<exprt> get_value_set(exprt expr, const namespacet &ns) const;
+  std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
 
   /// Appears to be unimplemented.
   DEPRECATED(SINCE(2019, 05, 22, "Unimplemented"))
diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h
index 3a95476f69e..12606dee785 100644
--- a/src/pointer-analysis/value_set_analysis.h
+++ b/src/pointer-analysis/value_set_analysis.h
@@ -76,7 +76,7 @@ class value_set_analysis_templatet:
   }
 
   // interface value_sets
-  std::list<exprt>
+  std::vector<exprt>
   get_values(const irep_idt &, locationt l, const exprt &expr) override
   {
     return (*this)[l].value_set.get_value_set(expr, baset::ns);
diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp
index 46e46c54d13..4ea1df6235a 100644
--- a/src/pointer-analysis/value_set_analysis_fi.cpp
+++ b/src/pointer-analysis/value_set_analysis_fi.cpp
@@ -196,7 +196,7 @@ bool value_set_analysis_fit::check_type(const typet &type)
   return false;
 }
 
-std::list<exprt> value_set_analysis_fit::get_values(
+std::vector<exprt> value_set_analysis_fit::get_values(
   const irep_idt &function_id,
   flow_insensitive_analysis_baset::locationt l,
   const exprt &expr)
diff --git a/src/pointer-analysis/value_set_analysis_fi.h b/src/pointer-analysis/value_set_analysis_fi.h
index 41c3ab59293..d04724d6587 100644
--- a/src/pointer-analysis/value_set_analysis_fi.h
+++ b/src/pointer-analysis/value_set_analysis_fi.h
@@ -74,7 +74,7 @@ class value_set_analysis_fit:
     state.value_set.get_value_set(expr, dest, ns);
   }
 
-  std::list<exprt> get_values(
+  std::vector<exprt> get_values(
     const irep_idt &function_id,
     locationt l,
     const exprt &expr) override;
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index a965f82746a..9037eb147e5 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -298,10 +298,14 @@ void value_set_fit::get_value_set(
   std::list<exprt> &value_set,
   const namespacet &ns) const
 {
-  value_set = get_value_set(expr, ns);
+  std::vector<exprt> result_as_vector = get_value_set(expr, ns);
+  std::move(
+    result_as_vector.begin(),
+    result_as_vector.end(),
+    std::back_inserter(value_set));
 }
 
-std::list<exprt>
+std::vector<exprt>
 value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
 {
   object_mapt object_map;
@@ -343,7 +347,7 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
       flat_map.write()[it->first]=it->second;
   }
 
-  std::list<exprt> result;
+  std::vector<exprt> result;
   forall_objects(fit, flat_map.read())
     result.push_back(to_expr(*fit));
 
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index 0e23f52100c..d96f4c0a80a 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -205,13 +205,14 @@ class value_set_fit
   typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
   #endif
 
-  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning object_mapt instead"))
+  DEPRECATED(SINCE(2019, 05, 22, "Use the version returning vector instead"))
   void get_value_set(
     const exprt &expr,
     std::list<exprt> &dest,
     const namespacet &ns) const;
 
-  std::list<exprt> get_value_set(const exprt &expr, const namespacet &ns) const;
+  std::vector<exprt>
+  get_value_set(const exprt &expr, const namespacet &ns) const;
 
   expr_sett &get(
     const idt &identifier,
diff --git a/src/pointer-analysis/value_sets.h b/src/pointer-analysis/value_sets.h
index f11343e0fc8..2001b7ac763 100644
--- a/src/pointer-analysis/value_sets.h
+++ b/src/pointer-analysis/value_sets.h
@@ -28,7 +28,7 @@ class value_setst
   typedef std::list<exprt> valuest;
 
   // this is not const to allow a lazy evaluation
-  DEPRECATED(SINCE(2019, 05, 22, "use list returning version instead"))
+  DEPRECATED(SINCE(2019, 05, 22, "use vector returning version instead"))
   virtual void get_values(
     const irep_idt &function_id,
     goto_programt::const_targett l,
@@ -36,7 +36,7 @@ class value_setst
     valuest &dest) = 0;
 
   // this is not const to allow a lazy evaluation
-  virtual valuest get_values(
+  virtual std::vector<exprt> get_values(
     const irep_idt &function_id,
     goto_programt::const_targett l,
     const exprt &expr) = 0;

From fa1412c758edd7d4f50c92ddc73fbf5ba34791ae Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 29 May 2019 07:35:49 +0100
Subject: [PATCH 7/7] Predefine DEPRECATED macro in doxyfile

This prevents the macro from making doxyfile miss method definitions
that are deprecated and automatically add the deprecated methods to the
Deprecated List generated by doxygen
---
 src/doxyfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/doxyfile b/src/doxyfile
index c0da7ae247d..13b1e6e672c 100644
--- a/src/doxyfile
+++ b/src/doxyfile
@@ -2041,7 +2041,7 @@ INCLUDE_FILE_PATTERNS  =
 # recursively expanded use the := operator instead of the = operator.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-PREDEFINED             =
+PREDEFINED             = "DEPRECATED(msg)= /// \deprecated msg"
 
 # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
 # tag can be used to specify a list of macro names that should be expanded. The