From 3ddba599df3f5cc737216cb8b25f90002893907b Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 19 Sep 2012 14:51:00 -0700 Subject: Boogie: improved parser makefile --- Source/Core/Makefile | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 -- cgit v1.2.3 From 071a2eae55d581e725a0bbd9a032b4c036b4b266 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Thu, 20 Sep 2012 11:01:25 +0200 Subject: Chalice: New regression test case from workitem 10221. --- Chalice/tests/regressions/workitem-10221.chalice | 158 +++++++++++++++++++++ .../tests/regressions/workitem-10221.output.txt | 4 + 2 files changed, 162 insertions(+) create mode 100644 Chalice/tests/regressions/workitem-10221.chalice create mode 100644 Chalice/tests/regressions/workitem-10221.output.txt 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 + requires list + { + unfolding list in (next == null ? [val] : [val] ++ next.vals()) + } + + function reverse_vals() : seq + 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 := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : 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 := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : 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 := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : 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 := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : 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 -- cgit v1.2.3 From f5a4ee5fb54f704387dcfdc7e4ee183d1bbc7876 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Thu, 20 Sep 2012 11:34:50 +0200 Subject: Chalice: New regression tests for fixed workitems 10189 and 10208. --- Chalice/tests/regressions/workitem-10189.chalice | 23 ++++++++++++ .../tests/regressions/workitem-10189.output.txt | 4 +++ Chalice/tests/regressions/workitem-10208.chalice | 41 ++++++++++++++++++++++ .../tests/regressions/workitem-10208.output.txt | 8 +++++ 4 files changed, 76 insertions(+) create mode 100644 Chalice/tests/regressions/workitem-10189.chalice create mode 100644 Chalice/tests/regressions/workitem-10189.output.txt create mode 100644 Chalice/tests/regressions/workitem-10208.chalice create mode 100644 Chalice/tests/regressions/workitem-10208.output.txt 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 -- cgit v1.2.3 From 1eaa3f92b844ab69824df8e87d26250c3e5552a0 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Fri, 21 Sep 2012 08:49:26 +0200 Subject: Chalice: Update release script to adapt to new scala version. --- Chalice/scripts/create_release/create_release.bat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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% -- cgit v1.2.3