diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-07-11 19:09:41 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-07-11 19:09:41 -0700 |
| commit | 59eff583615e198bd7381adda7be9c1527c2f199 (patch) | |
| tree | 9ccf8116e3740e04c18a9b76fa030fd5deff6b51 /Test | |
| parent | cb20c2a781055190994851bb375828db642fa271 (diff) | |
| parent | 4ba34f910f6d89b2f379f9fd79eab35d366abc08 (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/bitvectors/Answer | 3 | ||||
| -rw-r--r-- | Test/bitvectors/bv10.bpl | 10 | ||||
| -rw-r--r-- | Test/bitvectors/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Basics.dfy | 14 |
5 files changed, 29 insertions, 2 deletions
diff --git a/Test/bitvectors/Answer b/Test/bitvectors/Answer index 6f4068c6..f0f65b04 100644 --- a/Test/bitvectors/Answer +++ b/Test/bitvectors/Answer @@ -49,6 +49,9 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- bv8.bpl --------------------
Boogie program verifier finished with 2 verified, 0 errors
+-------------------- bv10.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
-------------------- bv9.bpl /bv:z /proverOpt:OPTIMIZE_FOR_BV=true --------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/bitvectors/bv10.bpl b/Test/bitvectors/bv10.bpl new file mode 100644 index 00000000..7c325d95 --- /dev/null +++ b/Test/bitvectors/bv10.bpl @@ -0,0 +1,10 @@ +var x: bv32;
+
+procedure main()
+modifies x;
+{
+
+ x := 0bv32;
+ assume x == 1bv32;
+ assert false;
+}
diff --git a/Test/bitvectors/runtest.bat b/Test/bitvectors/runtest.bat index fd5136f5..a0480645 100644 --- a/Test/bitvectors/runtest.bat +++ b/Test/bitvectors/runtest.bat @@ -11,7 +11,7 @@ for %%f in (arrays.bpl bv0.bpl bv1.bpl bv2.bpl bv3.bpl bv4.bpl bv7.bpl) do ( echo -------------------- bv4.bpl - /bv:n --------------------
%BGEXE% /bv:n %* /logPrefix:-1 bv4.bpl
-for %%f in (bv5.bpl bv6.bpl bv8.bpl) do (
+for %%f in (bv5.bpl bv6.bpl bv8.bpl bv10.bpl) do (
echo -------------------- %%f --------------------
%BGEXE% %* %%f
)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a29c64fa..7a972f22 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -657,7 +657,7 @@ Execution trace: (0,0): anon8
(0,0): anon14_Then
-Dafny program verifier finished with 16 verified, 11 errors
+Dafny program verifier finished with 19 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 1ae5b9c4..6aa1e34d 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -171,3 +171,17 @@ method SwapEm(a: int, b: int) returns (x: int, y: int) {
x, y := b, a;
}
+
+function method abs(a:int): int
+{
+ if a <= 0 then -a else a
+}
+// test of verifier using euclidean division.
+method EuclideanTest(a: int, b: int)
+ requires b != 0;
+{
+ var q, r := a / b, a % b;
+ assert 0 <= r < abs(b);
+ assert a == b * q + r;
+ assert (a/b) * b + a % b == a;
+}
\ No newline at end of file |