From a3d7bd9b4a7b62cb0d8e4b0762d8db51c1548f1e Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 13 May 2011 14:38:28 -0700 Subject: Boogie: added features to help with modular verification. In particular, define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations. --- Test/test0/runtest.bat | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'Test/test0/runtest.bat') diff --git a/Test/test0/runtest.bat b/Test/test0/runtest.bat index c7c6ee3d..5ecc22dc 100644 --- a/Test/test0/runtest.bat +++ b/Test/test0/runtest.bat @@ -31,3 +31,12 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify Orderings.bpl %BGEXE% %* /noVerify BadQuantifier.bpl %BGEXE% %* /noVerify EmptyCallArgs.bpl + +echo ----- SeparateVerification0.bpl +%BGEXE% %* /noVerify SeparateVerification0.bpl +echo ----- SeparateVerification1.bpl SeparateVerification0.bpl +%BGEXE% %* /noVerify SeparateVerification1.bpl SeparateVerification0.bpl +echo ----- SeparateVerification0.bpl SeparateVerification0.bpl +%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl +echo ----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl +%BGEXE% %* /noVerify SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl -- cgit v1.2.3