Add dynamic-object-expr recency

This adds the recency attribute and a simple pretty-printer.

Author: smowton

src/pointer-analysis/value_set.cpp

@@ -195,6 +195,16 @@ void value_sett::output(
       else
       {
         result="<"+from_expr(ns, identifier, o)+", ";
+        if(o.id()==ID_dynamic_object)
+        {
+          dynamic_object_exprt::recencyt recency=
+            to_dynamic_object_expr(o).get_recency();
+
+          if(recency==dynamic_object_exprt::recencyt::MOST_RECENT_ALLOCATION)
+            result+=as_string(ID_most_recent_allocation)+", ";
+          else if(recency==dynamic_object_exprt::recencyt::ANY_ALLOCATION)
+            result+=as_string(ID_any_allocation)+", ";
+        }
 
         if(o_it->second.offset_is_set)
           result+=integer2string(o_it->second.offset)+"";

src/util/irep_ids.txt

@@ -511,6 +511,9 @@ overflow_mult overflow-*
 overflow_unary_minus overflow-unary-
 object_descriptor
 dynamic_object
+is_most_recent_allocation
+most_recent_allocation
+any_allocation
 object_size
 good_pointer
 integer_address

src/util/std_expr.h

@@ -1490,6 +1490,8 @@ inline object_descriptor_exprt &to_object_descriptor_expr(exprt &expr)
 class dynamic_object_exprt:public exprt
 {
 public:
+  enum recencyt { MOST_RECENT_ALLOCATION, ANY_ALLOCATION, RECENCY_UNSET };
+
   dynamic_object_exprt():exprt(ID_dynamic_object)
   {
     operands().resize(2);
@@ -1505,6 +1507,40 @@ class dynamic_object_exprt:public exprt
     op1().id(ID_unknown);
   }
 
+  explicit dynamic_object_exprt(bool recent):
+    exprt(ID_dynamic_object)
+  {
+    operands().resize(2);
+    op0().id(ID_unknown);
+    op1().id(ID_unknown);
+    set_recency(recent);
+  }
+
+  dynamic_object_exprt(const typet &type, bool recent):
+    exprt(ID_dynamic_object, type)
+  {
+    operands().resize(2);
+    op0().id(ID_unknown);
+    op1().id(ID_unknown);
+    set_recency(recent);
+  }
+
+  recencyt get_recency() const
+  {
+    if(get(ID_is_most_recent_allocation)==ID_most_recent_allocation)
+      return MOST_RECENT_ALLOCATION;
+    else if(get(ID_is_most_recent_allocation)==ID_any_allocation)
+      return ANY_ALLOCATION;
+    else
+      return RECENCY_UNSET;
+  }
+
+  void set_recency(bool recent)
+  {
+    set(ID_is_most_recent_allocation,
+      (recent ? ID_most_recent_allocation : ID_any_allocation));
+  }
+
   exprt &instance()
   {
     return op0();