diff options
Diffstat (limited to 'Test/commandline')
8 files changed, 219 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 */ diff --git a/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl new file mode 100644 index 00000000..e0f8eef3 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_four_asterisk_wildcard.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie "-proc:*Bar" "-proc:*Foo" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 4 verified, 0 errors + +procedure foo() +{ + assert false; +} + +procedure helpfulFoo() +{ + assert true; +} + +procedure Foo() +{ + assert true; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_one.bpl b/Test/commandline/multiple_procs_verify_one.bpl new file mode 100644 index 00000000..5eaef4b1 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_one.bpl @@ -0,0 +1,22 @@ +// RUN: %boogie -proc:foo "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors + +// Only this procedure should be verified, the others should be ignored +procedure foo() +{ + assume true; +} + +// An old version of Boogie just checked if the name passed to ``-proc:`` +// occurs somewhere in procedure name which would cause it to try and also +// verify the procedures below. +procedure foo2() +{ + assert false; +} + +procedure function_foo() +{ + assert false; +} diff --git a/Test/commandline/multiple_procs_verify_one_request_twice.bpl b/Test/commandline/multiple_procs_verify_one_request_twice.bpl new file mode 100644 index 00000000..7c6ee34e --- /dev/null +++ b/Test/commandline/multiple_procs_verify_one_request_twice.bpl @@ -0,0 +1,20 @@ +// RUN: %boogie -proc:foo -proc:foo "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors + +// Although the command line requests two verify this procedure twice we should +// only do try once. +procedure foo() +{ + assume true; +} + +procedure bar() +{ + assert false; +} + +procedure baz() +{ + assert false; +} diff --git a/Test/commandline/multiple_procs_verify_two.bpl b/Test/commandline/multiple_procs_verify_two.bpl new file mode 100644 index 00000000..b089bd5b --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie -proc:foo -proc:bar "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assume true; +} + +procedure bar() +{ + assert true; +} + +procedure barz() +{ + assert false; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl new file mode 100644 index 00000000..0f6571ba --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_begin.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:*Bar" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure translucentBar() +{ + assert true; +} + +procedure opaqueBar() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl new file mode 100644 index 00000000..5cb102e2 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_end.bpl @@ -0,0 +1,17 @@ +// RUN: %boogie "-proc:bar*" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +procedure bar() +{ + assert true; +} + +procedure barzzz() +{ + assert true; +} diff --git a/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl new file mode 100644 index 00000000..7e19fe79 --- /dev/null +++ b/Test/commandline/multiple_procs_verify_two_asterisk_wildcard_inbetween.bpl @@ -0,0 +1,23 @@ +// RUN: %boogie "-proc:trivial*ZZZ" "%s" > "%t" +// RUN: %OutputCheck --file-to-check "%t" "%s" +// CHECK-L: Boogie program verifier finished with 2 verified, 0 errors +procedure foo() +{ + assert false; +} + +// should not be matched +procedure trivialFooZZX() +{ + assert false; +} + +procedure trivialFooZZZ() +{ + assert true; +} + +procedure trivialBarZZZ() +{ + assert true; +} |