Translate calls to static methods.

3 files changed, 29 insertions, 4 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 2e2df9fc..0f288955 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -334,8 +334,10 @@ namespace BytecodeTranslator {
       Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

 

       #region Create the 'this' argument for the function call

-      this.Visit(methodCall.ThisArgument);

-      inexpr.Add(this.TranslatedExpressions.Pop());

+      if (!methodCall.IsStaticCall) {

+        this.Visit(methodCall.ThisArgument);

+        inexpr.Add(this.TranslatedExpressions.Pop());

+      }

       #endregion

 

       Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index cd2a96f9..39188b03 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -9,6 +9,10 @@ namespace RegressionTestInput {
 

     static int StaticInt;

 

+    static int StaticMethod(int x) {

+      return x + 1;

+    }

+

     void M(int x) {

       int y = (5 / x) + (x = 3);

       Contract.Assert(x == 3 && y <= 8);

@@ -17,7 +21,7 @@ namespace RegressionTestInput {
     }

 

     int NonVoid() {

-      return 3 + StaticInt;

+      return 3 + StaticInt + StaticMethod(3);

     }

 

     int OutParam(out int x) {

diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
index a75316c8..bc72f5bf 100644
--- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
+++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
@@ -23,6 +23,23 @@ axiom (forall h: HeapType, c: TName :: { h[ClassRepr(c), $allocated] } IsHeap(h)
 

 var RegressionTestInput.Class0.StaticInt: int;

 

+procedure RegressionTestInput.Class0.StaticMethod$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.StaticMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    local_0 := x + 1;

+    $result := local_0;

+    return;

+}

+

+

+

 procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

 

 

@@ -59,8 +76,10 @@ procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($r
 implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)

 {

   var local_0: int;

+  var $tmp1: int;

 

-    local_0 := 3 + RegressionTestInput.Class0.StaticInt;

+    call $tmp1 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp1;

     $result := local_0;

     return;

 }