From 40b33d58e537fbe551abd02396acd26ad9065a97 Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Fri, 6 Sep 2024 16:56:06 +0300
Subject: [PATCH] One more test

---
 rust-semantics/expression/calls.md  | 1 -
 rust-semantics/test/execution.md    | 7 +++++++
 tests/execution/function-call.7.run | 6 ++++++
 tests/execution/function-call.rs    | 7 +++++++
 4 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/execution/function-call.7.run

diff --git a/rust-semantics/expression/calls.md b/rust-semantics/expression/calls.md
index c49241e..32abd98 100644
--- a/rust-semantics/expression/calls.md
+++ b/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
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index 4b2ccfa..ee6f3e8 100644
--- a/rust-semantics/test/execution.md
+++ b/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
 
 ```
\ No newline at end of file
diff --git a/tests/execution/function-call.7.run b/tests/execution/function-call.7.run
new file mode 100644
index 0000000..942835a
--- /dev/null
+++ b/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
diff --git a/tests/execution/function-call.rs b/tests/execution/function-call.rs
index ce247d9..ec3db18 100644
--- a/tests/execution/function-call.rs
+++ b/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
+    }
 }