From 34ae74207119493d494498cc3bb2cb5f1cdd27ba Mon Sep 17 00:00:00 2001
From: Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com>
Date: Wed, 7 Sep 2011 08:22:08 -0700
Subject: Completed basic version of GPUVerify tool

---
 Source/GPUVerify/Scripts/GPUVerifyDriver.bat | 60 ++++++++++++++++++++++++++--
 1 file changed, 56 insertions(+), 4 deletions(-)

(limited to 'Source/GPUVerify/Scripts/GPUVerifyDriver.bat')

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
-- 
cgit v1.2.3