PROOF: add unique-pointer predicate

Author: sipma

chc/proof/CPOPredicate.py

@@ -94,6 +94,7 @@
     'ub': 'upper-bound',
     'uio': 'uint-overflow',
     'uiu': 'uint-underflow',
+    'up': 'unique-pointer',
     'va': 'var-args',
     'vc': 'value-constraint',
     'vm': 'valid-mem',
@@ -297,6 +298,10 @@ def is_stack_address_escape(self) -> bool:
     def is_type_at_offset(self) -> bool:
         return False
 
+    @property
+    def is_unique_pointer(self) -> bool:
+        return False
+
     @property
     def is_upper_bound(self) -> bool:
         return False
@@ -2182,6 +2187,29 @@ def __str__(self) -> str:
         return "value-constraint(" + str(self.exp) + ")"
 
 
+@pdregistry.register_tag("up", CPOPredicate)
+class CPOUniquePointer(CPOPredicate):
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def exp(self) -> "CExp":
+        return self.cd.get_exp(self.args[0])
+
+    @property
+    def is_unique_pointer(self) -> bool:
+        return True
+
+    def has_variable(self, vid: int) -> bool:
+        return self.exp.has_variable(vid)
+
+    def __str__(self) -> str:
+        return "unique-pointer(" + str(self.exp) + ")"
+
+
 @pdregistry.register_tag("prm", CPOPredicate)
 class CPOPreservedAllMemory(CPOPredicate):
     """preserves-all-memory(): true of a function that does not free any memory.