diff options
| author |  Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-06 08:57:15 -0700 |
|---|---|---|
| committer | Unknown <t-alasdo@MSR-RISE-GUEST.redmond.corp.microsoft.com> | 2011-09-06 08:57:15 -0700 |
| commit | 45415e8c070cfe424d4aaa01c3c19cac4dea3345 (patch) | |
| tree | b803c8e7884cd89e44113e013f2458bdf13215eb /Source/GPUVerify/Scripts | |
| parent | 68abcafd6a654bb319738415a4d94dfa6baa3bfd (diff) | |
Added driver script and GPUVerify libary. The driver script works around the fact that Boogie does not do deep cloning of expressions when turning a structured program into an unstructured one.
Diffstat (limited to 'Source/GPUVerify/Scripts')
| -rw-r--r-- | Source/GPUVerify/Scripts/GPUVerifyDriver.bat | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat new file mode 100644 index 00000000..dda5ddcf --- /dev/null +++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat @@ -0,0 +1,9 @@ +echo off
+
+Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl
+
+GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl
+
+Boogie temp_ready_to_verify.bpl /prover:smtlib
+
+del temp_instrumented.bpl
|