From 2219ef06a1e87125273a9fa2dc24b92a388ec4de Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 7 Jan 2013 19:41:58 -0800 Subject: Allow attributes on procedure formals, function formals, and bound variables --- Test/test0/Answer | 11 ++++++----- Test/test0/WhereParsing.bpl | 9 +++++++++ Test/test0/WhereParsing0.bpl | 4 ++++ 3 files changed, 19 insertions(+), 5 deletions(-) (limited to 'Test/test0') 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 {:myAttr} x: T :: x == x); -- cgit v1.2.3