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/AttributeParsing.bpl | |
parent | 8f9d247e5c0aca8d811939892ab3be2a5acbdb5d (diff) |
Boogie: Simplified (and liberalized) parsing of string literals as attribute parameters
Diffstat (limited to 'Test/test0/AttributeParsing.bpl')
-rw-r--r-- | Test/test0/AttributeParsing.bpl | 13 |
1 files changed, 13 insertions, 0 deletions
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;
|