Merge

8 files changed, 243 insertions, 4 deletions

diff --git a/Chalice/scripts/create_release/create_release.bat b/Chalice/scripts/create_release/create_release.bat
index a0d67fd9..5aadd36e 100644
--- a/Chalice/scripts/create_release/create_release.bat
+++ b/Chalice/scripts/create_release/create_release.bat
@@ -6,7 +6,7 @@ set BASE_DIR=%~dp0\..\..
 set RELEASE_DIR_SRC=%~dp0\files

 set RELEASE_DIR_DST=%~dp0\release

 

-set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.8.1.final\chalice_2.8.1-1.0.jar

+set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.9.2\chalice_2.9.2-1.0.jar

 set CHALICE_JAR_DST=%RELEASE_DIR_DST%\chalice.jar

 

 pushd %BASE_DIR%

diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice
new file mode 100644
index 00000000..b37b83f2
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.chalice
@@ -0,0 +1,23 @@
+class Node { 
+	var v: int 
+	var next: Node 
+	 
+	predicate V { 
+			 acc(v) 
+		&& acc(next) 
+		&& (next != null ==> next.V) 
+	} 
+
+	unlimited function length(): int 
+		requires rd(V) 
+	{ 1 + unfolding rd(V) in next == null ? 0 : next.length() } 
+	 
+	unlimited function at(i: int): int
+		requires rd(V) 
+		requires i >= 0 
+		requires i < length() // XXXX
+	{
+		unfolding rd(V) in i == 0 ? v : next.at(i - 1)
+		// Precondition at XXX might not hold
+	} 
+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt
new file mode 100644
index 00000000..96f05468
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10189.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10189.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings

diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice
new file mode 100644
index 00000000..ae1a7d89
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.chalice
@@ -0,0 +1,41 @@
+class Test {

+  var f1: int;

+  var f2: int;

+

+  predicate valid {

+    acc(f1) && acc(f2) && f1 == f2

+  }

+  

+  method test()

+    requires valid

+  {

+    unfold valid

+    f1 := 2

+    f2 := 2

+    fold valid

+    

+    /* --- not strictly necessary */

+    unfold valid

+    assert f1 == 2

+    fold valid

+    /* --- */

+    

+    call test2()

+    

+    unfold valid

+    assert f1 == 2 // BUG: this should not verify (1)

+    assert false // BUG: this should not verify (2)

+  }

+  

+  method test2()

+    requires valid

+    ensures valid

+    ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition

+  {

+    unfold valid

+    f1 := 1

+    f2 := 1

+    fold valid

+  }

+  

+}

diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt
new file mode 100644
index 00000000..0666393a
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10208.output.txt
@@ -0,0 +1,8 @@
+Verification of workitem-10208.chalice using parameters="" 

+

+  26.5: Assertion might not hold. The expression at 26.12 might not evaluate to true.
+
+The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
+  9.3: The end of method test is unreachable.
+
+Boogie program verifier finished with 1 errors and 1 smoke test warnings

diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice
new file mode 100644
index 00000000..2a8ae723
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.chalice
@@ -0,0 +1,158 @@
+// In this example, additional unfold/fold pairs make the verification of the last three methods fail.

+

+class Node {

+  var next : Node;

+  var val : int;

+

+  predicate list {

+    acc(next) && acc(val) && (next!=null ==> next.list)

+  }

+  

+  function vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : [val] ++ next.vals())

+  }

+

+  function reverse_vals() : seq<int>

+    requires list

+  {

+    unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val])

+  }

+

+  method reverse_in_place() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+//      if (r != null) {

+//        unfold r.list; fold r.list;

+//      }

+      unfold l.list;

+//      if (l.next != null) {

+//        unfold l.next.list; fold l.next.list;

+//      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+

+   method reverse_in_place_01() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+//      if (r != null) {

+//        unfold r.list; fold r.list;

+//      }

+      unfold l.list;

+      if (l.next != null) {

+        unfold l.next.list; fold l.next.list;

+      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+

+   method reverse_in_place_10() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      if (r != null) {

+        unfold r.list; fold r.list;

+      }

+      unfold l.list;

+//      if (l.next != null) {

+//        unfold l.next.list; fold l.next.list;

+//      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+

+

+   method reverse_in_place_11() returns (r:Node)

+    requires list;

+    ensures true;

+  {

+    var l : Node := this;

+    r := null;

+

+    var rev : seq<int> := this.reverse_vals();

+    

+    while (l != null) 

+      invariant l!=null ==> l.list;

+      invariant r!=null ==> r.list;

+      invariant rev == (l==null ? nil<int> : l.reverse_vals()) ++ (r==null ? nil<int> : r.vals());

+    { 

+      var y: Node;

+      if (r != null) {

+        unfold r.list; fold r.list;

+      }

+      unfold l.list;

+      if (l.next != null) {

+        unfold l.next.list; fold l.next.list;

+      }

+    

+      y := l.next;

+      l.next := r;

+      r := l;

+      fold r.list;

+      l := y;

+    }

+    assert r.vals() == rev; // should be the post-condition

+  }

+  

+   

+}
\ No newline at end of file
diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt
new file mode 100644
index 00000000..e209c3c1
--- /dev/null
+++ b/Chalice/tests/regressions/workitem-10221.output.txt
@@ -0,0 +1,4 @@
+Verification of workitem-10221.chalice using parameters="" 

+

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings

diff --git a/Source/Core/Makefile b/Source/Core/Makefile
index 192a16db..4d3f433a 100644
--- a/Source/Core/Makefile
+++ b/Source/Core/Makefile
@@ -10,10 +10,11 @@ FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified
 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

 # nmake that.  --KRML

-all: Parser.ssc 

+all: Parser.cs

 

-Parser.ssc: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame BoogiePL.atg

+Parser.cs: $(FRAME_DIR)\Scanner.frame $(FRAME_DIR)\Parser.frame BoogiePL.atg

 	$(COCO) BoogiePL.atg -namespace Microsoft.Boogie -frames $(FRAME_DIR)

 

 clean:

-	rm -f Scanner.cs Parser.cs

+	if exist Scanner.cs del Scanner.cs

+	if exist Parser.cs del Parser.cs