diff options
Diffstat (limited to 'BCT')
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 238 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 22 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 15 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 19 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 2 | ||||
-rw-r--r-- | BCT/RegressionTests/RegressionTestInput/Class1.cs | 24 | ||||
-rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 288 | ||||
-rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 288 |
8 files changed, 764 insertions, 132 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index ccd3f748..b15b48ec 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -349,11 +349,16 @@ namespace BytecodeTranslator lit.Type = Bpl.Type.Int;
TranslatedExpressions.Push(lit);
break;
- case PrimitiveTypeCode.Float32:
- case PrimitiveTypeCode.Float64:
- var c = this.sink.FindOrCreateConstant((double)(constant.Value));
- TranslatedExpressions.Push(Bpl.Expr.Ident(c));
- return;
+ case PrimitiveTypeCode.Float32: {
+ var c = this.sink.FindOrCreateConstant((float)(constant.Value));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(c));
+ return;
+ }
+ case PrimitiveTypeCode.Float64: {
+ var c = this.sink.FindOrCreateConstant((double)(constant.Value));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(c));
+ return;
+ }
case PrimitiveTypeCode.NotPrimitive:
if (constant.Type.IsEnum) {
lit = Bpl.Expr.Literal((int)constant.Value);
@@ -902,7 +907,45 @@ namespace BytecodeTranslator base.Visit(addition);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp));
+ Bpl.Expr e;
+ switch (addition.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ addition.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealPlus),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
+ }
+
+ public override void Visit(IBitwiseAnd bitwiseAnd) {
+ base.Visit(bitwiseAnd);
+ Bpl.Expr rexp = TranslatedExpressions.Pop();
+ Bpl.Expr lexp = TranslatedExpressions.Pop();
+ var e = new Bpl.NAryExpr(
+ bitwiseAnd.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.BitwiseAnd),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ TranslatedExpressions.Push(e);
+ }
+
+ public override void Visit(IBitwiseOr bitwiseOr) {
+ base.Visit(bitwiseOr);
+ Bpl.Expr rexp = TranslatedExpressions.Pop();
+ Bpl.Expr lexp = TranslatedExpressions.Pop();
+ var e = new Bpl.NAryExpr(
+ bitwiseOr.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.BitwiseOr),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ TranslatedExpressions.Push(e);
}
public override void Visit(IDivision division)
@@ -910,15 +953,33 @@ namespace BytecodeTranslator base.Visit(division);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp));
+ Bpl.Expr e;
+ switch (division.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ division.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealDivide),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
- // TODO: Encode this correctly!
public override void Visit(IExclusiveOr exclusiveOr) {
base.Visit(exclusiveOr);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, lexp, rexp));
+ var e = new Bpl.NAryExpr(
+ exclusiveOr.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.BitwiseExclusiveOr),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ TranslatedExpressions.Push(e);
}
public override void Visit(ISubtraction subtraction)
@@ -926,7 +987,21 @@ namespace BytecodeTranslator base.Visit(subtraction);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp));
+ Bpl.Expr e;
+ switch (subtraction.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ subtraction.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealMinus),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
public override void Visit(IMultiplication multiplication)
@@ -934,7 +1009,21 @@ namespace BytecodeTranslator base.Visit(multiplication);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp));
+ Bpl.Expr e;
+ switch (multiplication.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ multiplication.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealTimes),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
public override void Visit(IModulus modulus)
@@ -1002,48 +1091,54 @@ namespace BytecodeTranslator /// </summary>
public override void Visit(IConditional conditional) {
#region Try and reconstruct And, Or, Not expressions
- CompileTimeConstant ctc = conditional.ResultIfFalse as CompileTimeConstant;
- if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32)
- {
- int v = (int)ctc.Value;
- if (v == 0) { // x ? y : 0 == x && y
- Visit(conditional.Condition);
- Bpl.Expr x = TranslatedExpressions.Pop();
- Visit(conditional.ResultIfTrue);
- Bpl.Expr y = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, x, y));
- return;
- }
- if (v == 1) { // x ? y : 1 == !x || y
- Visit(conditional.Condition);
- Bpl.Expr x = TranslatedExpressions.Pop();
- Visit(conditional.ResultIfTrue);
- Bpl.Expr y = TranslatedExpressions.Pop();
- var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x);
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, notX, y));
- return;
- }
- }
- ctc = conditional.ResultIfTrue as CompileTimeConstant;
- if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32)
- {
- int v = (int)ctc.Value;
- if (v == 1) { // x ? 1 : y == x || y
- Visit(conditional.Condition);
- Bpl.Expr x = TranslatedExpressions.Pop();
- Visit(conditional.ResultIfFalse);
- Bpl.Expr y = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, x, y));
- return;
+ if (conditional.Type.TypeCode == PrimitiveTypeCode.Boolean) {
+ CompileTimeConstant ctc = conditional.ResultIfFalse as CompileTimeConstant;
+ if (ctc != null) {
+ var v = BooleanValueOfCompileTimeConstant(ctc);
+ if (!v) { // x ? y : "false or 0" == x && y
+ Visit(conditional.Condition);
+ Bpl.Expr x = TranslatedExpressions.Pop();
+ x = PossiblyCoerceRefToBool(x);
+ Visit(conditional.ResultIfTrue);
+ Bpl.Expr y = TranslatedExpressions.Pop();
+ y = PossiblyCoerceRefToBool(y);
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, x, y));
+ return;
+ } else { // x ? y : "true or 1" == !x || y
+ Visit(conditional.Condition);
+ Bpl.Expr x = TranslatedExpressions.Pop();
+ x = PossiblyCoerceRefToBool(x);
+ Visit(conditional.ResultIfTrue);
+ Bpl.Expr y = TranslatedExpressions.Pop();
+ y = PossiblyCoerceRefToBool(y);
+ var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x);
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, notX, y));
+ return;
+ }
}
- if (v == 0) { // x ? 0 : y == !x && y
- Visit(conditional.Condition);
- Bpl.Expr x = TranslatedExpressions.Pop();
- Visit(conditional.ResultIfFalse);
- Bpl.Expr y = TranslatedExpressions.Pop();
- var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x);
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, notX, y));
- return;
+ ctc = conditional.ResultIfTrue as CompileTimeConstant;
+ if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32) {
+ var v = BooleanValueOfCompileTimeConstant(ctc);
+ if (v) { // x ? "true or 1" : y == x || y
+ Visit(conditional.Condition);
+ Bpl.Expr x = TranslatedExpressions.Pop();
+ x = PossiblyCoerceRefToBool(x);
+ Visit(conditional.ResultIfFalse);
+ Bpl.Expr y = TranslatedExpressions.Pop();
+ y = PossiblyCoerceRefToBool(y);
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, x, y));
+ return;
+ } else { // x ? "false or 0" : y == !x && y
+ Visit(conditional.Condition);
+ Bpl.Expr x = TranslatedExpressions.Pop();
+ x = PossiblyCoerceRefToBool(x);
+ Visit(conditional.ResultIfFalse);
+ Bpl.Expr y = TranslatedExpressions.Pop();
+ y = PossiblyCoerceRefToBool(y);
+ var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x);
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, notX, y));
+ return;
+ }
}
}
#endregion
@@ -1061,6 +1156,28 @@ namespace BytecodeTranslator }
+ private bool BooleanValueOfCompileTimeConstant(CompileTimeConstant ctc) {
+ if (ctc.Type.TypeCode == PrimitiveTypeCode.Int32)
+ return ((int)ctc.Value) != 0;
+ if (ctc.Type.TypeCode == PrimitiveTypeCode.Boolean)
+ return (bool)ctc.Value;
+ throw new NotImplementedException("BooleanValueOfCompileTimeConstant: Unknown type of compile-time constant");
+ }
+
+ /// <summary>
+ /// Sometimes the decompiler doesn't recreate the expression "o != null" when the
+ /// IL tests an object for being null by just branching on the object instead of
+ /// doing a ceq operation on the constant null.
+ /// </summary>
+ /// <returns>
+ /// If o is not of type Ref, then it just returns o, otherwise it returns
+ /// the expression "o != null".
+ /// </returns>
+ private Bpl.Expr PossiblyCoerceRefToBool(Bpl.Expr o) {
+ if (o.Type != this.sink.Heap.RefType) return o;
+ return Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, o, Bpl.Expr.Ident(this.sink.Heap.NullRef));
+ }
+
#endregion
#region Translate Unary Operators
@@ -1152,6 +1269,12 @@ namespace BytecodeTranslator default:
throw new NotImplementedException(msg);
}
+ case PrimitiveTypeCode.UIntPtr:
+ case PrimitiveTypeCode.IntPtr:
+ // just ignore the conversion. REVIEW: is that the right thing to do?
+ this.TranslatedExpressions.Push(exp);
+ return;
+
case PrimitiveTypeCode.Boolean:
if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {
TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0)));
@@ -1223,6 +1346,17 @@ namespace BytecodeTranslator }
}
+ public override void Visit(IOnesComplement onesComplement) {
+ base.Visit(onesComplement);
+ var exp = TranslatedExpressions.Pop();
+ var e = new Bpl.NAryExpr(
+ onesComplement.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.BitwiseNegation),
+ new Bpl.ExprSeq(exp)
+ );
+ TranslatedExpressions.Push(e);
+ }
+
public override void Visit(IUnaryNegation unaryNegation)
{
base.Visit(unaryNegation);
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 3dc1b5f9..40a3d4ad 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -229,6 +229,28 @@ namespace BytecodeTranslator { public Bpl.Function Real2Ref = null;
#endregion
+ #region Real number operations
+ [RepresentationFor("RealPlus", "function RealPlus(Real, Real): Real;")]
+ public Bpl.Function RealPlus = null;
+ [RepresentationFor("RealMinus", "function RealMinus(Real, Real): Real;")]
+ public Bpl.Function RealMinus = null;
+ [RepresentationFor("RealTimes", "function RealTimes(Real, Real): Real;")]
+ public Bpl.Function RealTimes = null;
+ [RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]
+ public Bpl.Function RealDivide = null;
+ #endregion
+
+ #region Bitwise operations
+ [RepresentationFor("BitwiseAnd", "function BitwiseAnd(int, int): int;")]
+ public Bpl.Function BitwiseAnd = null;
+ [RepresentationFor("BitwiseOr", "function BitwiseOr(int, int): int;")]
+ public Bpl.Function BitwiseOr = null;
+ [RepresentationFor("BitwiseExclusiveOr", "function BitwiseExclusiveOr(int, int): int;")]
+ public Bpl.Function BitwiseExclusiveOr = null;
+ [RepresentationFor("BitwiseNegation", "function BitwiseNegation(int): int;")]
+ public Bpl.Function BitwiseNegation = null;
+ #endregion
+
#region Ref conversions
[RepresentationFor("Ref2Int", "function Ref2Int(Ref, Type, Type): int;")]
public Bpl.Function Ref2Int = null;
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 18b8e0e6..1cad1a36 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -396,7 +396,20 @@ namespace BytecodeTranslator { } else { // method is translated as a function
//var func = decl as Bpl.Function;
//Contract.Assume(func != null);
- //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);
+ //var blocks = new List<Bpl.Block>();
+ //var counter = 0;
+ //var returnValue = decl.OutParams[0];
+ //foreach (var bb in translatedBody.BigBlocks) {
+ // var label = bb.LabelName ?? "L" + counter++.ToString();
+ // var newTransferCmd = (bb.tc is Bpl.ReturnCmd)
+ // ? new Bpl.ReturnExprCmd(bb.tc.tok, Bpl.Expr.Ident(returnValue))
+ // : bb.tc;
+ // var b = new Bpl.Block(bb.tok, label, bb.simpleCmds, newTransferCmd);
+ // blocks.Add(b);
+ //}
+ //var localVars = new Bpl.VariableSeq();
+ //localVars.Add(returnValue);
+ //func.Body = new Bpl.CodeExpr(localVars, blocks);
}
#endregion
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index bc28d9be..127317e9 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -251,6 +251,20 @@ namespace BytecodeTranslator { }
return c;
}
+ public Bpl.Constant FindOrCreateConstant(float f) {
+ Bpl.Constant c;
+ var str = f.ToString();
+ if (!this.declaredRealConstants.TryGetValue(str, out c)) {
+ var tok = Bpl.Token.NoToken;
+ var t = Heap.RealType;
+ var name = "$real_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str) + "_" + declaredStringConstants.Count;
+ var tident = new Bpl.TypedIdent(tok, name, t);
+ c = new Bpl.Constant(tok, tident, true);
+ this.declaredRealConstants.Add(str, c);
+ this.TranslatedProgram.TopLevelDeclarations.Add(c);
+ }
+ return c;
+ }
private Dictionary<string, Bpl.Constant> declaredRealConstants = new Dictionary<string, Bpl.Constant>();
private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();
@@ -431,7 +445,7 @@ namespace BytecodeTranslator { // Can't visit the method's contracts until the formalMap and procedure are added to the
// table because information in them might be needed (e.g., if a parameter is mentioned
// in a contract.
- #region Check The Method Contracts
+ #region Translate the method's contracts
var possiblyUnspecializedMethod = Unspecialize(method);
@@ -586,6 +600,9 @@ namespace BytecodeTranslator { // also, should it return true for properties and all of the other things the tools
// consider pure?
private bool IsPure(IMethodDefinition method) {
+ bool isPropertyGetter = method.IsSpecialName && method.Name.Value.StartsWith("get_");
+ if (isPropertyGetter) return true;
+
foreach (var a in method.Attributes) {
if (TypeHelper.GetTypeName(a.Type).EndsWith("PureAttribute")) {
return true;
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index d554d83e..cf856024 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -111,6 +111,7 @@ namespace BytecodeTranslator { s = s.Replace('-', '$');
s = s.Replace(' ', '$');
s = s.Replace('\t', '$');
+ s = s.Replace('\r', '$');
s = s.Replace('\n', '$');
s = s.Replace('/', '$');
s = s.Replace('\\', '$');
@@ -119,6 +120,7 @@ namespace BytecodeTranslator { s = s.Replace(';', '$');
s = s.Replace('%', '$');
s = s.Replace('&', '$');
+ s = s.Replace('"', '$');
return s;
}
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index 90fa7b50..d9f7b66c 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -157,4 +157,28 @@ namespace RegressionTestInput { }
}
+ public class RealNumbers {
+ public void WriteDouble(double d) {
+ Console.WriteLine(d);
+ }
+ public void ObjectToDouble(object o) {
+ WriteDouble((double)o);
+ }
+ public void RealOperations() {
+ double d = 3.0;
+ double d2 = 4.0;
+ WriteDouble(d + d2);
+ WriteDouble(d - d2);
+ WriteDouble(d * d2);
+ WriteDouble(d / d2);
+ }
+ }
+
+ public class BitwiseOperations {
+ public int BitwiseAnd(int x, int y) { return x & y; }
+ public int BitwiseOr(int x, int y) { return x | y; }
+ public int ExclusiveOr(int x, int y) { return x ^ y; }
+ public int BitwiseNegation(int x) { return ~x; }
+ }
+
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index eff71038..9ad72923 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -333,6 +333,22 @@ function Ref2Real(Ref, Type, Type) : Real; function Real2Ref(Real, Type, Type) : Ref;
+function RealPlus(Real, Real) : Real;
+
+function RealMinus(Real, Real) : Real;
+
+function RealTimes(Real, Real) : Real;
+
+function RealDivide(Real, Real) : Real;
+
+function BitwiseAnd(int, int) : int;
+
+function BitwiseOr(int, int) : int;
+
+function BitwiseExclusiveOr(int, int) : int;
+
+function BitwiseNegation(int) : int;
+
function Ref2Int(Ref, Type, Type) : int;
function Ref2Bool(Ref, Type, Type) : bool;
@@ -351,6 +367,110 @@ var $Method: [Ref][Ref]int; var $Receiver: [Ref][Ref]Ref;
+const unique RegressionTestInput.RealNumbers: Type;
+
+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real);
+
+
+
+procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);
+
+
+
+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real)
+{
+ var d: Real;
+
+ d := d$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+ call System.Console.WriteLine$System.Double(d);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref);
+
+
+
+const {:extern} unique System.Object: Type;
+
+const {:extern} unique System.Double: Type;
+
+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref)
+{
+ var o: Ref;
+
+ o := o$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, Ref2Real(o, System.Object, System.Double));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.RealOperations(this: Ref);
+
+
+
+const unique $real_literal_3_0: Real;
+
+const unique $real_literal_4_0: Real;
+
+implementation RegressionTestInput.RealNumbers.RealOperations(this: Ref)
+{
+ var local_0: Real;
+ var local_1: Real;
+ var $tmp0: Real;
+
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
+ local_0 := $real_literal_3_0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
+ local_1 := $real_literal_4_0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealPlus(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealMinus(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealTimes(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+ $tmp0 := local_1;
+ assert $tmp0 != 0;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, local_0 / $tmp0);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Object.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.RealNumbers.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.#cctor();
+
+
+
+implementation RegressionTestInput.RealNumbers.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field;
@@ -375,10 +495,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Re -procedure {:extern} System.Object.#ctor(this: Ref);
-
-
-
implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
{
$Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0));
@@ -417,14 +533,14 @@ const unique RegressionTestInput.S.b: Field; implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: Ref)
{
- var $tmp0: Ref;
+ var $tmp1: Ref;
var local_0: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
- call $tmp0 := Alloc();
- call RegressionTestInput.S.#default_ctor($tmp0);
- assume $DynamicType($tmp0) == RegressionTestInput.S;
- local_0 := $tmp0;
+ call $tmp1 := Alloc();
+ call RegressionTestInput.S.#default_ctor($tmp1);
+ assume $DynamicType($tmp1) == RegressionTestInput.S;
+ local_0 := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
assert Box2Int(Read($Heap, local_0, RegressionTestInput.S.x)) == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
@@ -491,22 +607,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: Ref;
- var $tmp1: Ref;
- var local_1: Ref;
var $tmp2: Ref;
+ var local_1: Ref;
+ var $tmp3: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- assume $ArrayLength($tmp1) == 1 * 5;
- local_0 := $tmp1;
+ call $tmp2 := Alloc();
+ assume $ArrayLength($tmp2) == 1 * 5;
+ local_0 := $tmp2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
assert local_0 == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- assume $ArrayLength($tmp2) == 1 * 4;
- local_1 := $tmp2;
+ call $tmp3 := Alloc();
+ assume $ArrayLength($tmp3) == 1 * 4;
+ local_1 := $tmp3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
@@ -525,22 +641,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: Ref;
- var local_0: Ref;
var $tmp4: Ref;
+ var local_0: Ref;
+ var $tmp5: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- assume $ArrayLength($tmp3) == 1 * 5;
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp4 := Alloc();
+ assume $ArrayLength($tmp4) == 1 * 5;
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp4;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
$ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
assert RegressionTestInput.ClassWithArrayTypes.s == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- assume $ArrayLength($tmp4) == 1 * 4;
- local_0 := $tmp4;
+ call $tmp5 := Alloc();
+ assume $ArrayLength($tmp5) == 1 * 4;
+ local_0 := $tmp5;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
@@ -587,7 +703,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: Ref;
xs := xs$in;
- if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
+ if (!(!(xs != null) || $ArrayLength(xs) <= 0))
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
$ArrayContents := $ArrayContents[Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][0 := Int2Box(xs)]];
@@ -626,6 +742,100 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor() +const unique RegressionTestInput.BitwiseOperations: Type;
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
+ $result := BitwiseAnd(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
+ $result := BitwiseOr(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
+ $result := BitwiseExclusiveOr(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32(this: Ref, x$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32(this: Ref, x$in: int) returns ($result: int)
+{
+ var x: int;
+
+ x := x$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
+ $result := BitwiseNegation(x);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.#cctor();
+
+
+
+implementation RegressionTestInput.BitwiseOperations.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.AsyncAttribute: Type;
procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
@@ -741,17 +951,17 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp6: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp6 := x;
+ assert $tmp6 != 0;
+ __temp_1 := 5 / $tmp6;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
- assert (if x == 3 then local_0 <= 8 else false);
+ assert x == 3 && local_0 <= 8;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
RegressionTestInput.Class0.StaticInt := local_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
@@ -815,11 +1025,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int)
{
- var $tmp6: int;
+ var $tmp7: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp6 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;
+ call $tmp7 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp7;
return;
}
@@ -902,12 +1112,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$i implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int)
{
var y: int;
- var $tmp7: int;
+ var $tmp8: int;
y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp7 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp7;
+ call {:async} $tmp8 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp8;
return;
}
@@ -995,10 +1205,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main()
{
- var $tmp8: bool;
+ var $tmp9: bool;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp8 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ call $tmp9 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
}
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 77d0950a..989ccfb9 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -323,6 +323,22 @@ function Ref2Real(Ref, Type, Type) : Real; function Real2Ref(Real, Type, Type) : Ref;
+function RealPlus(Real, Real) : Real;
+
+function RealMinus(Real, Real) : Real;
+
+function RealTimes(Real, Real) : Real;
+
+function RealDivide(Real, Real) : Real;
+
+function BitwiseAnd(int, int) : int;
+
+function BitwiseOr(int, int) : int;
+
+function BitwiseExclusiveOr(int, int) : int;
+
+function BitwiseNegation(int) : int;
+
function Ref2Int(Ref, Type, Type) : int;
function Ref2Bool(Ref, Type, Type) : bool;
@@ -341,6 +357,110 @@ var $Method: [Ref][Ref]int; var $Receiver: [Ref][Ref]Ref;
+const unique RegressionTestInput.RealNumbers: Type;
+
+procedure RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real);
+
+
+
+procedure {:extern} System.Console.WriteLine$System.Double(value$in: Real);
+
+
+
+implementation RegressionTestInput.RealNumbers.WriteDouble$System.Double(this: Ref, d$in: Real)
+{
+ var d: Real;
+
+ d := d$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 162} true;
+ call System.Console.WriteLine$System.Double(d);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 163} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref);
+
+
+
+const {:extern} unique System.Object: Type;
+
+const {:extern} unique System.Double: Type;
+
+implementation RegressionTestInput.RealNumbers.ObjectToDouble$System.Object(this: Ref, o$in: Ref)
+{
+ var o: Ref;
+
+ o := o$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 165} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, Ref2Real(o, System.Object, System.Double));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 166} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.RealOperations(this: Ref);
+
+
+
+const unique $real_literal_3_0: Real;
+
+const unique $real_literal_4_0: Real;
+
+implementation RegressionTestInput.RealNumbers.RealOperations(this: Ref)
+{
+ var local_0: Real;
+ var local_1: Real;
+ var $tmp0: Real;
+
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 168} true;
+ local_0 := $real_literal_3_0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 169} true;
+ local_1 := $real_literal_4_0;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 170} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealPlus(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 171} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealMinus(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 172} true;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, RealTimes(local_0, local_1));
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 173} true;
+ $tmp0 := local_1;
+ assert $tmp0 != 0;
+ call RegressionTestInput.RealNumbers.WriteDouble$System.Double(this, local_0 / $tmp0);
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 174} true;
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.#ctor(this: Ref);
+
+
+
+procedure {:extern} System.Object.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.RealNumbers.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.RealNumbers.#cctor();
+
+
+
+implementation RegressionTestInput.RealNumbers.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int;
@@ -365,10 +485,6 @@ procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Re -procedure {:extern} System.Object.#ctor(this: Ref);
-
-
-
implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref)
{
RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0;
@@ -407,14 +523,14 @@ var RegressionTestInput.S.b: [Ref]bool; implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: Ref)
{
- var $tmp0: Ref;
+ var $tmp1: Ref;
var local_0: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 141} true;
- call $tmp0 := Alloc();
- call RegressionTestInput.S.#default_ctor($tmp0);
- assume $DynamicType($tmp0) == RegressionTestInput.S;
- local_0 := $tmp0;
+ call $tmp1 := Alloc();
+ call RegressionTestInput.S.#default_ctor($tmp1);
+ assume $DynamicType($tmp1) == RegressionTestInput.S;
+ local_0 := $tmp1;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 142} true;
assert Box2Int(local_0[RegressionTestInput.S.x]) == 0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 143} true;
@@ -481,22 +597,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1()
{
var local_0: Ref;
- var $tmp1: Ref;
- var local_1: Ref;
var $tmp2: Ref;
+ var local_1: Ref;
+ var $tmp3: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 86} true;
- call $tmp1 := Alloc();
- assume $ArrayLength($tmp1) == 1 * 5;
- local_0 := $tmp1;
+ call $tmp2 := Alloc();
+ assume $ArrayLength($tmp2) == 1 * 5;
+ local_0 := $tmp2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 87} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 88} true;
assert local_0 == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 90} true;
- call $tmp2 := Alloc();
- assume $ArrayLength($tmp2) == 1 * 4;
- local_1 := $tmp2;
+ call $tmp3 := Alloc();
+ assume $ArrayLength($tmp3) == 1 * 4;
+ local_1 := $tmp3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 91} true;
$ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 92} true;
@@ -515,22 +631,22 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2()
{
- var $tmp3: Ref;
- var local_0: Ref;
var $tmp4: Ref;
+ var local_0: Ref;
+ var $tmp5: Ref;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 100} true;
- call $tmp3 := Alloc();
- assume $ArrayLength($tmp3) == 1 * 5;
- RegressionTestInput.ClassWithArrayTypes.s := $tmp3;
+ call $tmp4 := Alloc();
+ assume $ArrayLength($tmp4) == 1 * 5;
+ RegressionTestInput.ClassWithArrayTypes.s := $tmp4;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 101} true;
$ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 102} true;
assert RegressionTestInput.ClassWithArrayTypes.s == 2;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 104} true;
- call $tmp4 := Alloc();
- assume $ArrayLength($tmp4) == 1 * 4;
- local_0 := $tmp4;
+ call $tmp5 := Alloc();
+ assume $ArrayLength($tmp5) == 1 * 4;
+ local_0 := $tmp5;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 105} true;
$ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]];
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 106} true;
@@ -577,7 +693,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: Ref;
xs := xs$in;
- if (!(if xs != null then $ArrayLength(xs) <= 0 else true))
+ if (!(!(xs != null) || $ArrayLength(xs) <= 0))
{
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 121} true;
$ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][0 := Int2Box(xs)]];
@@ -616,6 +732,100 @@ implementation RegressionTestInput.ClassWithArrayTypes.#cctor() +const unique RegressionTestInput.BitwiseOperations: Type;
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseAnd$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 178} true;
+ $result := BitwiseAnd(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 179} true;
+ $result := BitwiseOr(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.ExclusiveOr$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) returns ($result: int)
+{
+ var x: int;
+ var y: int;
+
+ x := x$in;
+ y := y$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 180} true;
+ $result := BitwiseExclusiveOr(x, y);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32(this: Ref, x$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.BitwiseNegation$System.Int32(this: Ref, x$in: int) returns ($result: int)
+{
+ var x: int;
+
+ x := x$in;
+ assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 181} true;
+ $result := BitwiseNegation(x);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.#ctor(this: Ref);
+
+
+
+implementation RegressionTestInput.BitwiseOperations.#ctor(this: Ref)
+{
+ call System.Object.#ctor(this);
+ return;
+}
+
+
+
+procedure RegressionTestInput.BitwiseOperations.#cctor();
+
+
+
+implementation RegressionTestInput.BitwiseOperations.#cctor()
+{
+}
+
+
+
const unique RegressionTestInput.AsyncAttribute: Type;
procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref);
@@ -731,17 +941,17 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) {
var x: int;
var __temp_1: int;
- var $tmp5: int;
+ var $tmp6: int;
var local_0: int;
x := x$in;
- $tmp5 := x;
- assert $tmp5 != 0;
- __temp_1 := 5 / $tmp5;
+ $tmp6 := x;
+ assert $tmp6 != 0;
+ __temp_1 := 5 / $tmp6;
x := 3;
local_0 := __temp_1 + 3;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 22} true;
- assert (if x == 3 then local_0 <= 8 else false);
+ assert x == 3 && local_0 <= 8;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 23} true;
RegressionTestInput.Class0.StaticInt := local_0;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 24} true;
@@ -805,11 +1015,11 @@ procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int)
{
- var $tmp6: int;
+ var $tmp7: int;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 34} true;
- call $tmp6 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;
+ call $tmp7 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
+ $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp7;
return;
}
@@ -892,12 +1102,12 @@ procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$i implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int)
{
var y: int;
- var $tmp7: int;
+ var $tmp8: int;
y := y$in;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp7 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp7;
+ call {:async} $tmp8 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
+ $result := $tmp8;
return;
}
@@ -985,10 +1195,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main()
{
- var $tmp8: bool;
+ var $tmp9: bool;
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 78} true;
- call $tmp8 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
+ call $tmp9 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
assert {:sourceFile "C:\dev\BoogieCodePlex\BCT\RegressionTests\RegressionTestInput\Class1.cs"} {:sourceLine 79} true;
return;
}
|