BCT: Added prelude. Started test1 as a test of verification.

6 files changed, 33 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