diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
commit | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch) | |
tree | 8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Test/commandline/multiple_procs_unusual_identifiers.bpl | |
parent | 64e8b33656140b87137d0662d9e6835e004d13c2 (diff) | |
parent | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff) |
Merge branch 'upstream' into dfsg_free
Diffstat (limited to 'Test/commandline/multiple_procs_unusual_identifiers.bpl')
-rw-r--r-- | Test/commandline/multiple_procs_unusual_identifiers.bpl | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/Test/commandline/multiple_procs_unusual_identifiers.bpl b/Test/commandline/multiple_procs_unusual_identifiers.bpl new file mode 100644 index 00000000..a3a4a4c1 --- /dev/null +++ b/Test/commandline/multiple_procs_unusual_identifiers.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie "-proc:*Bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 10 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert false; +} + +/* Start should be matched */ + +procedure _Bar() +{ + assert true; +} + +procedure .Bar() +{ + assert true; +} + +procedure ..Bar..() +{ + assert true; +} + +procedure $Bar() +{ + assert true; +} + +procedure #Bar() +{ + assert true; +} + +procedure 'Bar''() +{ + assert true; +} + +procedure ``Bar``() +{ + assert true; +} + +procedure ~Bar() +{ + assert true; +} + +procedure Bar^^() +{ + assert true; +} + +/* This is Boogie2 claims backslash is a valid identifier + but the parser rejects this. +procedure Bar\\() +{ + assert true; +} +*/ + +procedure ??Bar() +{ + assert true; +} + +/* End should be matched */ |