Added test cases

Author: radumcostache

Test/irreduciblecfg/Await.bpl

@@ -0,0 +1,44 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+var new: int;
+procedure await_eq_add(val : int)
+    modifies new;
+    ensures val == old(val);
+    ensures (new == old(new) + val);
+{
+    var x : int;
+    var tmp : bool;
+    assume tmp == true;
+    B: 
+        havoc x;
+        if (x == val) {
+            goto E;
+        }
+        else {
+            goto C;
+        }
+    C: 
+        if (tmp == true) {
+            havoc x;
+        }
+        goto D;
+    D: 
+        if (x != val) {
+            goto C;
+        }
+        else {
+            goto E;
+        }
+    E:
+        havoc tmp;
+        if (tmp == true) {
+            new := new + x;
+            goto G;
+        }
+        else {
+            goto C;
+        }
+    G:
+}

Test/irreduciblecfg/Canonical.bpl

@@ -0,0 +1,11 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+procedure Irreducible ()
+{
+A: goto B,C;
+B: goto C,D;
+C: goto B;
+D: return;
+} 

Test/irreduciblecfg/CanonicalAssertAssume.bpl

@@ -0,0 +1,26 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure irreducible() {
+    var i: int;
+    var j: int;
+
+    i := 1;
+    goto B1, B4;
+
+    B1:
+        assume j > 0;
+        goto B2;
+    
+    B2:
+        assert i > 0;
+        goto B3;
+    
+    B3:
+        assert j > 0;
+        goto B4;
+    
+    B4:
+        i := i+1;
+        goto B2;
+}

Test/irreduciblecfg/CanonicalAssertAssume.bpl.expect

@@ -0,0 +1,5 @@
+CanonicalAssertAssume.bpl(20,9): Error: this loop invariant could not be proved on entry
+Execution trace:
+    CanonicalAssertAssume.bpl(8,7): anon0
+
+Boogie program verifier finished with 0 verified, 1 error

Test/irreduciblecfg/CanonicalConditions.bpl

@@ -0,0 +1,22 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+procedure simple_irreducible() {
+    var x: int;
+    x := 0;
+    A:
+        assert x == 0;
+        x := x + 1;
+        goto B, C;
+
+    B:
+        assert x <= 2;
+        x := x - 1;
+        goto C, D;
+    C: 
+        x := x + 1;
+        goto B;
+    D: 
+        assert x <= 1;
+}

Test/irreduciblecfg/Tangled.bpl

@@ -0,0 +1,49 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+var x, y, z : int;
+var add: int;
+procedure tangled()
+    requires x > 0;
+    requires y > 0;
+    requires z > 0;
+    modifies x;
+    modifies y;
+    modifies z;
+    modifies add;
+    ensures (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+{
+    A: 
+        goto B, C;
+    B:
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        z := z - 1;
+        x := x + 1;
+        goto C, D, F, EXIT; 
+    C: 
+        x := x - 1;
+        y := y + 1;
+        goto B, D, E, EXIT;
+    D: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        y := y + 1;
+        add := add + 1;
+        goto E, F, D, G;
+    E: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        z := z + 1;
+        add := add + 1;
+        goto E, F, D, B;
+    F: 
+        assert (x + y + z) == old(x) + old(y) + old(z) + add - old(add);
+        x := x + 1;
+        add := add + 1;
+        goto E, F, D, C;
+    G: 
+        z := z + 1;
+        y := y - 1;
+        goto B, D, EXIT;
+
+    EXIT: 
+}

Test/irreduciblecfg/Unsound.bpl

@@ -0,0 +1,15 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure unsound() {
+    var x: int;
+    assume(x == 0);
+    if (true) {
+        goto Inside;
+    }
+    while (x < 10000) {
+        Inside: x := x + 1;
+    }
+
+    assert(x == -1);
+}

Test/irreduciblecfg/Unsound.bpl.expect

@@ -0,0 +1,7 @@
+Unsound.bpl(14,5): Error: this assertion could not be proved
+Execution trace:
+    Unsound.bpl(6,5): anon0
+    Unsound.bpl(8,9): anon4_Then
+    Unsound.bpl(10,5): anon5_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error