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/WhereParsing.bpl | |
| parent | 4e5d28feec671e5e2493f9ecc89fc5e14018d017 (diff) | |
Allow attributes on procedure formals, function formals, and bound variables
Diffstat (limited to 'Test/test0/WhereParsing.bpl')
| -rw-r--r-- | Test/test0/WhereParsing.bpl | 9 |
1 files changed, 9 insertions, 0 deletions
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
+{
+}
|