Merge pull request #167 from lucasccordeiro/aisimplifier

Aisimplifier

Author: Daniel Kroening

regression/goto-analyzer/intervals2/intervals2.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x > -10 && x < 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals2/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals2.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals3/intervals3.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x > -10 || x < 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals3/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals3.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals4/intervals4.c

@@ -0,0 +1,12 @@
+//#include <assert.h>
+
+int main()
+{
+  int i;
+  
+  if(i>0)
+    if(i<3)
+      assert(i>=1 && i<=2);
+ 
+  return 0;
+} 

regression/goto-analyzer/intervals4/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals4.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals5/intervals5.c

@@ -0,0 +1,12 @@
+//#include <assert.h>
+
+int main()
+{
+  int i;
+  
+  if(i>0)
+    if(i<3)
+      assert(i>=1 || i<=2);
+ 
+  return 0;
+} 

regression/goto-analyzer/intervals5/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals5.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/intervals6/intervals6.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x < -10 || x > 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals6/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals6.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/intervals7/intervals7.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main(){
+  int x;
+  if (x > 0) {
+    if (x < 20) {
+      assert(x < -10 && x > 100);
+    }
+  }
+  return 0;
+}

regression/goto-analyzer/intervals7/test.desc

@@ -0,0 +1,8 @@
+CORE
+intervals7.c
+--intervals
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$
+--
+^warning: ignoring

src/analyses/interval_domain.cpp

@@ -148,7 +148,7 @@ bool interval_domaint::merge(
   if(bottom) { *this=b; return true; }
 
   bool result=false;
-  
+
   for(int_mapt::iterator it=int_map.begin();
       it!=int_map.end(); ) // no it++
   {
@@ -293,7 +293,7 @@ void interval_domaint::assume_rec(
   if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
   {
     irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
-    
+
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
       mp_integer tmp;