diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-12 14:03:04 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-12 14:03:04 -0700 |
| commit | 2a6bca050cc8418f506851dd2d8699bdf145ca6e (patch) | |
| tree | c0aa1d854148aaf446052a991030fe0c3fe53ebb /Test/test0 | |
| parent | 8f9d247e5c0aca8d811939892ab3be2a5acbdb5d (diff) | |
Boogie: Simplified (and liberalized) parsing of string literals as attribute parameters
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 6 | ||||
| -rw-r--r-- | Test/test0/AttributeParsing.bpl | 13 |
2 files changed, 19 insertions, 0 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index d434a8ca..51a139b7 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -186,6 +186,12 @@ type any; type name;
+procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();
+
+
+
+const again: int;
+
Boogie program verifier finished with 0 verified, 0 errors
AttributeResolution.bpl(1,18): Error: undeclared identifier: foo
AttributeResolution.bpl(3,18): Error: undeclared identifier: bar
diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl index a6a8418b..e2b6101c 100644 --- a/Test/test0/AttributeParsing.bpl +++ b/Test/test0/AttributeParsing.bpl @@ -23,3 +23,16 @@ implementation {:id 2} foo(x : int) returns(n : int) }
type ref, any, name;
+
+
+// allow \" and other backslashes rather liberally:
+
+procedure
+ {:myAttribute
+ "h\n\"ello\"",
+ "again",
+ "and\\" a\"gain\"",
+ again}
+P();
+
+const again: int;
|