diff options
| author |  Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-07 08:22:08 -0700 |
|---|---|---|
| committer | Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-07 08:22:08 -0700 |
| commit | 34ae74207119493d494498cc3bb2cb5f1cdd27ba (patch) | |
| tree | e00429ef49b1d60ad3c7952aeb41b089bb50d820 /Source/GPUVerify/Scripts/GPUVerifyDriver.bat | |
| parent | 45415e8c070cfe424d4aaa01c3c19cac4dea3345 (diff) | |
Completed basic version of GPUVerify tool
Diffstat (limited to 'Source/GPUVerify/Scripts/GPUVerifyDriver.bat')
| -rw-r--r-- | Source/GPUVerify/Scripts/GPUVerifyDriver.bat | 60 |
1 files changed, 56 insertions, 4 deletions
diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat index dda5ddcf..d81c0fc1 100644 --- a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat +++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat @@ -1,9 +1,61 @@ -echo off
+@ECHO OFF
-Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl
+set InputFile=""
+set SkeletonFile=""
+set ScriptDir=%~p0
+
+:Loop
+IF "%1"=="" GOTO Continue
+
+set temp=%1
+
+IF %temp:~0,26%==/generateFormulaSkeletons: GOTO SetSkeletonFile
+
+set InputFile=%1
+
+GOTO LastPartOfLoop
+
+:SetSkeletonFile
+
+set SkeletonFile=%temp:~26%
+
+:LastPartOfLoop
+
+SHIFT
+GOTO Loop
+:Continue
+
+IF %InputFile%=="" GOTO Error
+
+echo Preprocess
+Boogie /noVerify /printUnstructured /print:temp_unstructured.bpl %InputFile% %ScriptDir%..\BoogieLibrary\GPUVerifyLibrary.bpl
+
+IF %SkeletonFile%=="" GOTO Verify
+
+GOTO Generate
+
+
+
+
+:Verify
+echo Verify
GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl
+Boogie temp_ready_to_verify.bpl formulas.bpl /prover:smtlib
+del temp_unstructured.bpl
+GOTO End
+
+:Generate
+echo Generate
+GPUVerify temp_unstructured.bpl /generateFormulaSkeletons:%SkeletonFile%
+del temp_unstructured.bpl
+GOTO End
+
+:Error
+echo Error: Bad command line specified for GPUVerify
+GOTO End
+
+
-Boogie temp_ready_to_verify.bpl /prover:smtlib
-del temp_instrumented.bpl
+:End
\ No newline at end of file |