One more test

rust-semantics/expression/calls.md

@@ -44,7 +44,6 @@ module RUST-EXPRESSION-CALLS
         <values> A |-> struct(TraitName:TypePath, _) ... </values>
         requires isValueWithPtr(Args)
 
-    // TODO: Test for this.
     rule methodCall
             (... traitName: _TraitName:TypePath
             , method: _MethodName:Identifier

rust-semantics/test/execution.md

@@ -10,6 +10,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "call" TypePath "." Identifier
                             | "return_value"
                             | "check_eq" Expression  [strict]
+                            | "push" Expression [strict]
 endmodule
 
 module RUST-EXECUTION-TEST
@@ -73,6 +74,12 @@ module RUST-EXECUTION-TEST
         <k> check_eq ptrValue(_, V:Value) => .K ... </k>
         <test-stack> ListItem(ptrValue(_, V)) => .List ... </test-stack>
 
+    rule
+        <k> push ptrValue(_, V:Value) => .K ... </k>
+        <test-stack> .List => ListItem(ptr(NVI)) ... </test-stack>
+        <values> VALUES:Map => VALUES[NVI <- V] </values>
+        <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
+
 endmodule
 
 ```

tests/execution/function-call.7.run

@@ -0,0 +1,6 @@
+new FunctionCalls;
+push 1_u64;
+push 3_u64;
+call FunctionCalls.call_arguments;
+return_value;
+check_eq 4_u64

tests/execution/function-call.rs

@@ -36,4 +36,11 @@ pub trait FunctionCalls {
         self.get_self().one()
     }
     fn get_self(&self) -> FunctionCalls { self }
+
+    fn call_arguments(&self, x: u64, y: &u64) -> u64 {
+        self.sum_arguments(x, y)
+    }
+    fn sum_arguments(&self, x: u64, y: &u64) -> u64 {
+        x + y
+    }
 }