summaryrefslogtreecommitdiff
path: root/BCT/RegressionTests
diff options
context:
space:
mode:
Diffstat (limited to 'BCT/RegressionTests')
-rw-r--r--BCT/RegressionTests/RegressionTestInput/Class1.cs24
-rw-r--r--BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt288
-rw-r--r--BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt288
3 files changed, 522 insertions, 78 deletions
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;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-28 01:08:59 +0000