Fix #497 (#516)

* fix #497. * fix & test
kframework · Jul 3, 2019 · dce53ce · dce53ce
1 parent fc23dfc
commit dce53ce
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 4 deletions.
diff --git a/semantics/cpp/language/execution/expr/function-call.k b/semantics/cpp/language/execution/expr/function-call.k
@@ -159,9 +159,18 @@ module CPP-EXECUTION-EXPR-FUNCTION-CALL
                <most-derived-class> MDC </most-derived-class>
           ...</function-control>)
 
-     rule <k> bindParam(X::CId, T::CPPType, V:Val) => declareNonStaticObjectExec(X, T,
-               ExecName(NoNNS(), X) :=init V,
-               Var(CopyInit()), AutoStorage, .Set) ...</k>
+     syntax SymBase ::= getBaseOfVal(Val) [function]
+
+     rule getBaseOfVal(lv(...v: L::SymLoc) #Or xv(...v: L::SymLoc) #Or prv(...v: L::SymLoc))
+          => baseOfLoc(L)
+
+     syntax SymBase ::= baseOfLoc(SymLoc) [function]
+
+     rule baseOfLoc(loc(Base::SymBase, _)) => Base
+
+     rule <k> bindParam(X::CId, T::CPPType, V:Val)
+              => addToExecEnv(X, T, getBaseOfVal(V), false)
+           ...</k>
           <curr-function-params>... .List => ListItem(X) </curr-function-params>
           requires notBool isCPPRefType(T)
                andBool X =/=K #NoName

diff --git a/semantics/cpp/language/execution/init.k b/semantics/cpp/language/execution/init.k
@@ -36,7 +36,13 @@ module CPP-EXECUTION-INIT
           requires getParams(T) ==K .List
 
      rule #callCppEntryPoint(T::CPPType, Base::SymBase, Argc:Int, X:CId, Args:K)
-          => Args ~> setupCppEnv(Argc) ~> BuiltinCallOp(lv(lnew(Base), noTrace, T), false, ListItem(prv(Argc, noTrace, type(int))) ListItem(ExecName(NoNNS(), X)))
+          => Args
+          ~> setupCppEnv(Argc)
+          ~> BuiltinCallOp(lv(lnew(Base), noTrace, T), false,
+               ListItem(le(temp(!I:Int, type(int)), noTrace, T) :=init prv(Argc, noTrace, type(int)))
+
+               ListItem(ExecName(NoNNS(), X))
+          )
           requires size(getParams(T)) ==Int 2
 
      syntax KItem ::= setupCppEnv(Int)

diff --git a/tests/unit-pass/argc.C b/tests/unit-pass/argc.C
@@ -0,0 +1,3 @@
+int main(int argc, char *argv[]) {
+	return -1 + argc;
+}
diff --git a/tests/unit-pass/call-by-value.C b/tests/unit-pass/call-by-value.C
@@ -0,0 +1,8 @@
+struct A {};
+
+void foo(A a) {}
+
+int main() {
+	A a;
+	foo(a);
+}