diff options
| author |  mikebarnett <unknown> | 2010-07-05 15:47:08 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2010-07-05 15:47:08 +0000 |
| commit | 609b1d52af4c48b98de2bd5e77b8da888ce89d1f (patch) | |
| tree | a89fbf5346966e7526565782944328246d1d2d63 /BCT/RegressionTests | |
| parent | f24ac57418f9aee520f10f6ba75c6970a2cada6b (diff) | |
Cleaned up the sink: removed the OutVars, which was state the sink needed only for assigning the local copy of a method's parameter to the out parameter of the Boogie procedure. But now that is simplified: instead of three versions of each parameter (in, local, and out), there are only two: in and out. For a parameter that is *not* by reference and is *not* an out parameter (i.e., just a plain pass-by-value parameter), the "out" version is a local variable. Otherwise it is an out parameter of the Boogie procedure.
Diffstat (limited to 'BCT/RegressionTests')
| -rw-r--r-- | BCT/RegressionTests/RegressionTestInput/Class1.cs | 19 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/RegressionTestInput.txt | 65 |
2 files changed, 83 insertions, 1 deletions
diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index f537f861..c6ab393c 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -11,5 +11,24 @@ namespace RegressionTestInput { Contract.Assert(x == 3 && y <= 8);
}
+ int NonVoid() {
+ return 3;
+ }
+
+ int OutParam(out int x) {
+ x = 3;
+ return x;
+ }
+
+ int RefParam(ref int x) {
+ x = x + 1;
+ return x;
+ }
+
+ int AssignToInParam(int x) {
+ x = x + 1;
+ return x;
+ }
+
}
}
diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt index 564dd07e..329731f1 100644 --- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt +++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt @@ -17,12 +17,12 @@ procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int); implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)
{
+ var x: int;
var __temp_1: int;
var $tmp0: int;
var __temp_2: int;
var __temp_3: int;
var local_0: int;
- var x: int;
x := x$in;
$tmp0 := x;
@@ -38,6 +38,69 @@ implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int) +procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)
+{
+ $result := 3;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int);
+
+
+
+implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int)
+{
+ var local_0: int;
+
+ x$out := 3;
+ local_0 := x$out;
+ $result := local_0;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int);
+
+
+
+implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int)
+{
+ var local_0: int;
+
+ x$out := x$in;
+ x$out := x$out + 1;
+ local_0 := x$out;
+ $result := local_0;
+ return;
+}
+
+
+
+procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);
+
+
+
+implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
+{
+ var x: int;
+ var local_0: int;
+
+ x := x$in;
+ x := x + 1;
+ local_0 := x;
+ $result := local_0;
+ return;
+}
+
+
+
procedure RegressionTestInput.Class0..ctor$System.Void(this: int);
|