10 files changed, 74 insertions, 7 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 3c5c510f..9af26786 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -107,6 +107,7 @@
     <Reference Include="System.Xml" />
   </ItemGroup>
   <ItemGroup>
+    <Compile Include="Prelude.cs" />
     <Compile Include="ExpressionTraverser.cs" />
     <Compile Include="ClassTraverser.cs" />
     <Compile Include="MethodTraverser.cs" />
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 2db2e403..c9b89bd9 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -330,7 +330,7 @@ namespace BytecodeTranslator {
 
       Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
 
-      #region Create the $this argument for the function call
+      #region Create the 'this' argument for the function call
       ExpressionTraverser thistraverser = new ExpressionTraverser(StmtTraverser);
       thistraverser.Visit(methodCall.ThisArgument);
       inexpr.Add(thistraverser.TranslatedExpressions.Pop());
diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs
index 45cb6b6c..fdda674d 100644
--- a/BCT/BytecodeTranslator/MethodTraverser.cs
+++ b/BCT/BytecodeTranslator/MethodTraverser.cs
@@ -164,12 +164,12 @@ namespace BytecodeTranslator {
 
         #endregion
 
-        #region Create $this parameter
+        #region Create 'this' parameter
         in_count++;
         Bpl.Type selftype = Bpl.Type.Int;
         Bpl.Formal self = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),
             new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),
-                "$inst", selftype), true);
+                "this", selftype), true);
 
         #endregion
 
@@ -179,7 +179,7 @@ namespace BytecodeTranslator {
         int i = 0;
         int j = 0;
 
-        #region Add $this parameter as first in parameter
+        #region Add 'this' parameter as first in parameter
         invars[i++] = self;
         #endregion
 
diff --git a/BCT/BytecodeTranslator/Prelude.cs b/BCT/BytecodeTranslator/Prelude.cs
new file mode 100644
index 00000000..0ebcd9f9
--- /dev/null
+++ b/BCT/BytecodeTranslator/Prelude.cs
@@ -0,0 +1,25 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Text;
+
+namespace BytecodeTranslator {
+  class Prelude {
+    public static void Emit(Microsoft.Boogie.TokenTextWriter wr) {
+      wr.WriteText(@"// Copyright (c) 2010, Microsoft Corp.
+// Bytecode Translator prelude
+
+type Ref;
+const null: Ref;
+
+type Field alpha;
+
+type HeapType = <alpha>[Ref, Field alpha]alpha;
+function IsGoodHeap(HeapType): bool;
+
+var $Heap: HeapType where IsGoodHeap($Heap);
+
+");
+    }
+  }
+}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 3c2a1fa0..26696250 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -66,8 +66,8 @@ namespace BytecodeTranslator {
         translator.Visit(module);
       #endregion Pass 3: Translate the code model to BPL
       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(module.Name + ".bpl");
+      Prelude.Emit(writer);
       translator.TranslatedProgram.Emit(writer);
-      writer.WriteLine(";ENDE");
       writer.Close();
       return 0; // success
     }
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index 978a9412..0bbad693 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -50,11 +50,11 @@ namespace BytecodeTranslator {
     }
 
     public static Bpl.Variable TempHeapVar() {
-      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$heap", Bpl.Type.Int)); 
+      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$Heap", Bpl.Type.Int)); 
     }
 
     public static Bpl.Variable TempThisVar() {
-      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$this", Bpl.Type.Int));
+      return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "this", Bpl.Type.Int));
     }
 
     #endregion
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
+)