add boundedint (#1459)

* change z3expr to float used in interval value * fix symabs * add boundedint * fix bug * float to double * fix is real * fix ZExt --------- Co-authored-by: jiawei-95 <jiawei.ren95@foxmail.com> Co-authored-by: bjjwwang <bjjwwang@github.com>
SVF-tools · May 16, 2024 · 1bf0f0d · 1bf0f0d
1 parent b39e8ab
commit 1bf0f0d
Show file tree

Hide file tree

Showing 9 changed files with 738 additions and 1,040 deletions.
diff --git a/svf/include/AE/Core/AbstractValue.h b/svf/include/AE/Core/AbstractValue.h
@@ -213,31 +213,31 @@ class AbstractValue
         return interval.isBottom();
     }
 
-    const NumericLiteral& lb() const
+    const BoundedInt& lb() const
     {
         assert(isInterval());
         return interval.lb();
     }
 
-    const NumericLiteral& ub() const
+    const BoundedInt& ub() const
     {
         assert(isInterval());
         return interval.ub();
     }
 
-    void setLb(const NumericLiteral& lb)
+    void setLb(const BoundedInt& lb)
     {
         assert(isInterval());
         interval.setLb(lb);
     }
 
-    void setUb(const NumericLiteral& ub)
+    void setUb(const BoundedInt& ub)
     {
         assert(isInterval());
         interval.setUb(ub);
     }
 
-    void setValue(const NumericLiteral &lb, const NumericLiteral &ub)
+    void setValue(const BoundedInt &lb, const BoundedInt &ub)
     {
         assert(isInterval());
         interval.setValue(lb, ub);