From 2a6bca050cc8418f506851dd2d8699bdf145ca6e Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Mon, 12 Mar 2012 14:03:04 -0700
Subject: Boogie: Simplified (and liberalized) parsing of string literals as
 attribute parameters

---
 Test/test0/Answer               |  6 ++++++
 Test/test0/AttributeParsing.bpl | 13 +++++++++++++
 2 files changed, 19 insertions(+)

(limited to 'Test/test0')

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;
-- 
cgit v1.2.3