diff options
| author |  rustanleino <unknown> | 2010-05-12 01:00:42 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-12 01:00:42 +0000 |
| commit | 33a5c553fab275428437c0439667fc09d2f89dce (patch) | |
| tree | 531ad9f246c4996e71371f925a11570e417915c9 /BCT/Test | |
| parent | e5fcbeda373f505f4ebfd29cafe776d9ec7b8db5 (diff) | |
BCT: Added prelude. Started test1 as a test of verification.
Diffstat (limited to 'BCT/Test')
| -rw-r--r-- | BCT/Test/alltests.txt | 1 | ||||
| -rw-r--r-- | BCT/Test/test1/Answer | 0 | ||||
| -rw-r--r-- | BCT/Test/test1/Locals.cs | 23 | ||||
| -rw-r--r-- | BCT/Test/test1/runtest.bat | 17 |
4 files changed, 41 insertions, 0 deletions
diff --git a/BCT/Test/alltests.txt b/BCT/Test/alltests.txt index 9d2f739d..0c01ab99 100644 --- a/BCT/Test/alltests.txt +++ b/BCT/Test/alltests.txt @@ -1 +1,2 @@ test0 Use Translation of Statements
+test1 Use Some simple verification tests
diff --git a/BCT/Test/test1/Answer b/BCT/Test/test1/Answer new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/BCT/Test/test1/Answer diff --git a/BCT/Test/test1/Locals.cs b/BCT/Test/test1/Locals.cs new file mode 100644 index 00000000..f07c0e3f --- /dev/null +++ b/BCT/Test/test1/Locals.cs @@ -0,0 +1,23 @@ +using System;
+using System.Collections.Generic;
+//using System.Diagnostics.Contracts;
+
+class Program
+{
+ private int i;
+
+ void M0(int j) {
+ i = 7;
+ int k;
+ k = i + 20;
+ i = k / j; // error: possible division by zero
+ }
+
+ void M1(int j) {
+ // Contract.Requires(0 < j);
+ if (!(0 < j)) throw new Exception();
+ i = 7;
+ int k = i + 20;
+ i = k / j;
+ }
+}
diff --git a/BCT/Test/test1/runtest.bat b/BCT/Test/test1/runtest.bat new file mode 100644 index 00000000..cff01f44 --- /dev/null +++ b/BCT/Test/test1/runtest.bat @@ -0,0 +1,17 @@ +@echo off
+setlocal
+
+set BCTDIR=..\..\Binaries
+set BEXE=%BCTDIR%\BytecodeTranslator.exe
+set BOOGIE=..\..\..\Binaries\Boogie.exe
+
+if not exist Output.txt goto justRunTest
+del Output.txt
+
+:justRunTest
+for %%f in (*.cs) do (
+ echo -------------------- %%f --------------------
+ csc /nologo /t:library /debug %%~nf.cs
+ %BEXE% %%~nf.dll
+ %BOOGIE% %%~nf.bpl >> Output.txt
+)
|