From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- .../multiple_procs_unusual_identifiers.bpl | 75 ++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 Test/commandline/multiple_procs_unusual_identifiers.bpl (limited to 'Test/commandline/multiple_procs_unusual_identifiers.bpl') 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 */ -- cgit v1.2.3