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.

1 files changed, 19 insertions, 0 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;

+    }

+

   }

 }