diff options
| -rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 1 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MethodTraverser.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Prelude.cs | 25 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 4 | ||||
| -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 | ||||
| -rw-r--r-- | Source/Core/Util.ssc | 15 |
11 files changed, 89 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
+)
diff --git a/Source/Core/Util.ssc b/Source/Core/Util.ssc index e90358ac..87323eb5 100644 --- a/Source/Core/Util.ssc +++ b/Source/Core/Util.ssc @@ -200,6 +200,21 @@ namespace Microsoft.Boogie this.col = 0;
}
+ public void WriteText(string! text) {
+ int processed = 0;
+ while (true) {
+ int n = text.IndexOf('\n', processed);
+ if (n == -1) {
+ this.writer.Write(text);
+ this.col += text.Length - processed;
+ return;
+ }
+ processed = n + 1;
+ this.line++;
+ this.col = 0;
+ }
+ }
+
public void WriteLine(string! text, params object[] args)
{
this.WriteLine(string.Format(text, args));
|