diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-07 19:41:58 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-07 19:41:58 -0800 |
| commit | 2219ef06a1e87125273a9fa2dc24b92a388ec4de (patch) | |
| tree | 7fcdff5bfccd8671e045af5e722fdb0a854b6012 /Test/test0 | |
| parent | 4e5d28feec671e5e2493f9ecc89fc5e14018d017 (diff) | |
Allow attributes on procedure formals, function formals, and bound variables
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 11 | ||||
| -rw-r--r-- | Test/test0/WhereParsing.bpl | 9 | ||||
| -rw-r--r-- | Test/test0/WhereParsing0.bpl | 4 |
3 files changed, 19 insertions, 5 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index 0eda9e2e..d71ac997 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -133,11 +133,12 @@ Types1.bpl(6,11): Error: undeclared type: x Types1.bpl(7,11): Error: undeclared type: x
Types1.bpl(7,14): Error: undeclared type: x
3 name resolution errors detected in Types1.bpl
-WhereParsing.bpl(14,37): error: where clause not allowed here
-WhereParsing.bpl(15,33): error: where clause not allowed here
-2 parse errors detected in WhereParsing.bpl
-WhereParsing0.bpl(17,38): error: where clause not allowed here
-WhereParsing0.bpl(18,38): error: where clause not allowed here
+WhereParsing.bpl(14,37): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(15,33): error: where clause not allowed on the 'implementation' copies of formals
+WhereParsing.bpl(32,38): error: attributes are not allowed on the 'implementation' copies of formals
+3 parse errors detected in WhereParsing.bpl
+WhereParsing0.bpl(17,38): error: where clause not allowed on bound variables
+WhereParsing0.bpl(18,38): error: where clause not allowed on bound variables
2 parse errors detected in WhereParsing0.bpl
WhereParsing1.bpl(14,27): error: ")" expected
1 parse errors detected in WhereParsing1.bpl
diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl index ec18dc3b..33e500d6 100644 --- a/Test/test0/WhereParsing.bpl +++ b/Test/test0/WhereParsing.bpl @@ -23,3 +23,12 @@ implementation P(xx: int where xx > 0) // error: where not allowed in implement yy := b;
return;
}
+
+procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool)
+{
+}
+
+procedure BadAttrs(x: int);
+implementation BadAttrs({:myParamAttr} x: int) // error: attributes not allowed in implementation decl
+{
+}
diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl index 84f92741..f99dc1ab 100644 --- a/Test/test0/WhereParsing0.bpl +++ b/Test/test0/WhereParsing0.bpl @@ -26,3 +26,7 @@ procedure Q(x: int where x > 0) returns (y: int where y < 0) y := b;
return;
}
+
+axiom (forall yu: bool, {:myAttr} x: int :: x < 100);
+axiom (forall {:myAttr} x: int :: x < 100);
+axiom (forall <T> {:myAttr} x: T :: x == x);
|