Merge pull request #1461 from bjjwwang/absval

remove some ambiguous API in AbstractValue
SVF-tools · May 16, 2024 · 5051626 · 5051626
2 parents 021f0f8 + f09c82d
commit 5051626
Show file tree

Hide file tree

Showing 9 changed files with 101 additions and 379 deletions.
diff --git a/svf-llvm/tools/AE/ae.cpp b/svf-llvm/tools/AE/ae.cpp
@@ -111,7 +111,7 @@ class SymblicAbstractionTest
         // var1 := var0 + 1;
         relation[1] =
             getContext().int_const("1") == getContext().int_const("0") + 1;
-        itv[1] = itv[0] + IntervalValue(1);
+        itv[1] = itv[0].getInterval() + IntervalValue(1);
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[1], res);
@@ -145,7 +145,7 @@ class SymblicAbstractionTest
         // var1 := var0 + 1;
         relation[1] =
             getContext().int_const("1") == getContext().int_const("0") * 2;
-        itv[1] = itv[0] * IntervalValue(2);
+        itv[1] = itv[0].getInterval() * IntervalValue(2);
 
         // Test extract sub vars
         Set<u32_t> res;
@@ -184,7 +184,7 @@ class SymblicAbstractionTest
         // var2 := var1 - var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") - getContext().int_const("0");
-        itv[2] = itv[1] - itv[0];
+        itv[2] = itv[1].getInterval() - itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);
@@ -226,7 +226,7 @@ class SymblicAbstractionTest
         // var2 := var1 - var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") - getContext().int_const("0");
-        itv[2] = itv[1] - itv[0];
+        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
         // Test extract sub vars
         Set<u32_t> res;
@@ -269,7 +269,7 @@ class SymblicAbstractionTest
         // var2 := var1 - var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") - getContext().int_const("0");
-        itv[2] = itv[1] - itv[0];
+        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
         // Test extract sub vars
         Set<u32_t> res;
@@ -312,7 +312,7 @@ class SymblicAbstractionTest
         // var2 := var1 - var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") - getContext().int_const("0");
-        itv[2] = itv[1] - itv[0];
+        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
         // Test extract sub vars
         Set<u32_t> res;
@@ -355,7 +355,7 @@ class SymblicAbstractionTest
         // var2 := var1 - var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") - getContext().int_const("0");
-        itv[2] = itv[1] - itv[0];
+        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
         // Test extract sub vars
         Set<u32_t> res;
@@ -398,7 +398,7 @@ class SymblicAbstractionTest
         // var2 := var1 / var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") / getContext().int_const("0");
-        itv[2] = itv[1] / itv[0];
+        itv[2] = itv[1].getInterval() / itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);
@@ -440,7 +440,7 @@ class SymblicAbstractionTest
         // var2 := var1 / var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") / getContext().int_const("0");
-        itv[2] = itv[1] / itv[0];
+        itv[2] = itv[1].getInterval() / itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);
@@ -482,7 +482,7 @@ class SymblicAbstractionTest
         // var2 := var1 / var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") / getContext().int_const("0");
-        itv[2] = itv[1] / itv[0];
+        itv[2] = itv[1].getInterval() / itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);
@@ -523,7 +523,7 @@ class SymblicAbstractionTest
         // var2 := var1 / var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") / getContext().int_const("0");
-        itv[2] = itv[1] / itv[0];
+        itv[2] = itv[1].getInterval() / itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);
@@ -565,7 +565,7 @@ class SymblicAbstractionTest
         // var2 := var1 / var0;
         relation[2] = getContext().int_const("2") ==
                       getContext().int_const("1") / getContext().int_const("0");
-        itv[2] = itv[1] / itv[0];
+        itv[2] = itv[1].getInterval() / itv[0].getInterval();
         // Test extract sub vars
         Set<u32_t> res;
         relation.extractSubVars(relation[2], res);