From 717eaee0063074b804098d3cfd44a7a3f822b064 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 16 Feb 2010 05:07:46 +0000
Subject: Implemented block coalescing invoked right after type checking.
 Controlled by the option /coalesceBlocks (default is to perform the
 optimization).

---
 Test/aitest1/Answer      | 90 ++++++++----------------------------------------
 Test/aitest1/Linear4.bpl |  4 ++-
 Test/aitest1/Linear5.bpl |  8 +++--
 3 files changed, 23 insertions(+), 79 deletions(-)

(limited to 'Test/aitest1')

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index 4e5c8f27..ca9ff22a 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -121,29 +121,9 @@ implementation FooTooStepByStep()
   L0:
     assume true;
     i := 5;
-    assume i == 5;
-    goto L1;
-
-  L1:
-    assume i == 5;
     i := 3 * i + 1;
-    assume i == 16;
-    goto L2;
-
-  L2:
-    assume i == 16;
     i := 3 * (i + 1);
-    assume 1 / 3 * i == 17;
-    goto L3;
-
-  L3:
-    assume 1 / 3 * i == 17;
     i := 1 + 3 * i;
-    assume i == 154;
-    goto L4;
-
-  L4:
-    assume i == 154;
     i := (i + 1) * 3;
     assume 1 / 3 * i == 155;
     return;
@@ -256,13 +236,18 @@ implementation p()
     assume true;
     assume x < y;
     assume x + 1 <= y;
-    goto B;
+    goto B, C;
 
   B:
     assume x + 1 <= y;
     x := x * x;
     assume true;
     return;
+
+  C:
+    assume x + 1 <= y;
+    assume x + 1 <= y;
+    return;
 }
 
 
@@ -285,25 +270,30 @@ implementation p()
     assume true;
     assume 0 - 1 <= x;
     assume -1 <= x;
-    goto B;
+    goto B, E;
 
   B:
     assume -1 <= x;
     assume x < y;
     assume x + 1 <= y && -1 <= x;
-    goto C;
+    goto C, E;
 
   C:
     assume x + 1 <= y && -1 <= x;
     x := x * x;
     assume 0 <= y;
-    goto D;
+    goto D, E;
 
   D:
     assume 0 <= y;
     x := y;
     assume x == y && 0 <= y;
     return;
+
+  E:
+    assume true;
+    assume true;
+    return;
 }
 
 
@@ -405,54 +395,14 @@ implementation foo()
   A:
     assume true;
     n := 0;
-    assume n == 0;
-    goto B;
-
-  B:
-    assume n == 0;
     j := 0;
-    assume j == 0 && n == 0;
-    goto C;
-
-  C:
-    assume j == 0 && n == 0;
     i := j + 1;
-    assume i == j + 1 && j == 0 && n == 0;
-    goto D;
-
-  D:
-    assume i == j + 1 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 2 && j == 0 && n == 0;
-    goto E;
-
-  E:
-    assume i == j + 2 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 3 && j == 0 && n == 0;
-    goto F;
-
-  F:
-    assume i == j + 3 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 4 && j == 0 && n == 0;
-    goto G;
-
-  G:
-    assume i == j + 4 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 5 && j == 0 && n == 0;
-    goto H;
-
-  H:
-    assume i == j + 5 && j == 0 && n == 0;
     j := j + 1;
     assume i == j + 4 && j == 1 && n == 0;
-    goto I;
-
-  I:
-    assume i == j + 4 && j == 1 && n == 0;
-    assume i == j + 4 && j == 1 && n == 0;
     return;
 }
 
@@ -481,19 +431,9 @@ implementation foo()
   loop0:  // cut point
     assume 4 <= n && 0 <= i && j == i + 1;
     assume j <= n;
-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;
-    goto loop1;
-
-  loop1:
-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;
     i := i + 1;
-    assume 1 <= i && j == i && j <= n && 4 <= n;
-    goto loop2;
-
-  loop2:
-    assume j <= n && 4 <= n && 1 <= i && j == i;
     j := j + 1;
-    assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;
+    assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
     goto loop0, exit;
 
   exit:
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
index c8c4605c..2207debe 100644
--- a/Test/aitest1/Linear4.bpl
+++ b/Test/aitest1/Linear4.bpl
@@ -8,8 +8,10 @@ procedure p()
 {
   A:
     assume x < y;
-    goto B;
+    goto B, C;
   B:
     x := x*x;
     return;
+  C:
+    return;
 }
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 4f04999c..199cb6f2 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -8,14 +8,16 @@ procedure p()
 {
   A:
     assume -1 <= x;
-    goto B;
+    goto B, E;
   B:
     assume x < y;
-    goto C;
+    goto C, E;
   C:
     x := x*x;
-    goto D;
+    goto D, E;
   D:
     x := y;
     return;
+  E:
+    return;
 }
-- 
cgit v1.2.3