diff options
author | wuestholz <unknown> | 2011-12-21 17:49:31 +0100 |
---|---|---|
committer | wuestholz <unknown> | 2011-12-21 17:49:31 +0100 |
commit | 9152bf2ff98b1dce60a347afa4ec39bc3df86c4a (patch) | |
tree | 0a1eab252e247e4c2768634bfccdeaa9124639ca /Test/dafny0 | |
parent | 4e73a3397844fa7802854fd059a32b0c33c46de7 (diff) |
Dafny: Added support for attributes on method/constructor calls.
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Answer | 2 | ||||
-rw-r--r-- | Test/dafny0/SmallTests.dfy | 40 |
2 files changed, 41 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index aa58ac6e..5e1428c2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -247,7 +247,7 @@ SmallTests.dfy(411,41): Error: possible violation of function postcondition Execution trace:
(0,0): anon6_Else
-Dafny program verifier finished with 49 verified, 21 errors
+Dafny program verifier finished with 56 verified, 21 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7adc26a3..e6590ed1 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -418,6 +418,26 @@ function F(b: bool): int class AttributeTests {
var f: int;
+ method m0()
+ {
+
+ }
+
+ method m1() returns (r: bool)
+ {
+ r := false;
+ }
+
+ function method m2() : bool
+ {
+ true
+ }
+
+ constructor C()
+ {
+
+ }
+
method testAttributes0()
ensures {:boolAttr true} true;
ensures {:boolAttr false} true;
@@ -465,5 +485,25 @@ class AttributeTests { {
}
+
+ m0() {:boolAttr true};
+ m0() {:boolAttr false};
+ m0() {:intAttr 0};
+ m0() {:intAttr 1};
+
+ var b1 := m1() {:boolAttr true};
+ b1 := m1() {:boolAttr false};
+ b1 := m1() {:intAttr 0};
+ b1 := m1() {:intAttr 1};
+
+ var b2 := m2() {:boolAttr true};
+ b2 := m2() {:boolAttr false};
+ b2 := m2() {:intAttr 0};
+ b2 := m2() {:intAttr 1};
+
+ var c := new AttributeTests.C() {:boolAttr true};
+ c := new AttributeTests.C() {:boolAttr false};
+ c := new AttributeTests.C() {:intAttr 0};
+ c := new AttributeTests.C() {:intAttr 1};
}
}
|