Aisimplifier

regression/goto-analyzer/Makefile

@@ -12,3 +12,8 @@ show:
 			vim -o "$$dir/*.java" "$$dir/*.out"; \
 		fi; \
 	done;
+
+clean:
+	find . -name *.*~ | xargs rm -f
+	find . -name *.out | xargs rm -f
+	rm -f tests.log	

regression/goto-analyzer/constant_propagation_01/constant_propagation1.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+
+  if (j==20)
+  {
+    int x=1,y=2,z;
+    z=x+y;
+    assert(z==3);
+  }
+
+}

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation1.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i==0) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_02.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c

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

regression/goto-analyzer/constant_propagation_03/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_03.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j==3);
+}

regression/goto-analyzer/constant_propagation_04/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_04.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  if (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j!=3);
+}

regression/goto-analyzer/constant_propagation_05/test.desc

@@ -0,0 +1,8 @@
+CORE
+constant_propagation_05.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main()
+{
+  int i, j=20;
+
+  if(i>=20)
+    assert(i>=10); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=30); // success
+
+  if(i>=10 && i<=20)
+    assert(i!=15); // fails
+
+  if(i<1 && i>10)
+    assert(0); // success
+
+  if(i>=10 && j>=i)
+    assert(j>=10); // success
+
+  if(i>=j)
+    assert(i>=j); // unknown
+
+  if(i>10)
+    assert(i>=11); // success
+
+  if(i<=100 && j<i)
+    assert(j<100); // success
+}

regression/goto-analyzer/constant_propagation_06/test.desc

@@ -0,0 +1,15 @@
+CORE
+constant_propagation_06.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
+^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
+^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
+^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
+^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
+^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
+^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
+^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<51);
+}
+

regression/goto-analyzer/constant_propagation_07/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_07.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<50: UNKNOWN$
+^\[main.assertion.2\] file constant_propagation_07.c line 13 function main, assertion i<51: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(i<50);
+  assert(i<51);
+  assert(i<52);
+}
+

regression/goto-analyzer/constant_propagation_08/test.desc

@@ -0,0 +1,10 @@
+CORE
+constant_propagation_08.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
+^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$
+^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i=0, j=2;
+
+  while (i<=50) 
+  {
+    i++;
+    j++;
+  }
+  assert(j<52);
+}
+

regression/goto-analyzer/constant_propagation_09/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_09.c
+--constant-propagation --intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+******** Function main
+^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+int main()
+{
+  signed int i;
+  signed int j;
+  i = 0;
+   if(!(i >= 2))
+  {
+    j = j + 1;
+    i = i + 1;
+    if(!(i >= 2))
+    {
+      j = j + 1;
+      i = i + 1;
+      if(!(i >= 2))
+      {
+        j = j + 1;
+        i = i + 1;
+      }
+      assert(!(i < 2));
+    }
+  }
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_10/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_10.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+int main()
+{
+  int a[2];
+  int i;
+  i = 0;
+
+  if (i==0)
+    a[0]=1;
+  else
+    a[1]=2;
+
+  assert(a[0]==1 || a[1]==2);
+
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_11/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_10.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==0);
+
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_12/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_12.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+  int i, y;
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==2);
+
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_13/test.desc

@@ -0,0 +1,8 @@
+CORE
+constant_propagation_13.c
+--constant-propagation --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$
+--
+^warning: ignoring

regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+int main()
+{
+  int a[2]={0,0};
+
+  if (a[0]==0)
+    a[0]=1;
+
+  assert(a[0]==1 /*|| a[0]==2*/);
+
+  return 0;
+}
+

regression/goto-analyzer/constant_propagation_14/test.desc

@@ -0,0 +1,9 @@
+CORE
+constant_propagation_14.c
+--constant-propagation --simplify
+^EXIT=0$
+^SIGNAL=0$
+^SIMPLIFIED:  assert: 1, assume: 0, goto: 0$
+^UNKNOWN:     assert: 0, assume: 0, goto: 0$
+--
+^warning: ignoring