Test expects
diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index a8b8629..03f4e76 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst
@@ -320,7 +320,7 @@ $${rule-prose: Step/call_addr} -$${rule: {Step/call_addr}} +$${rule: {Step/call_addr-func}} .. note:: For non-defaultable types, the respective local is left uninitialized by these rules. @@ -367,7 +367,7 @@ However, all store modifications must result in an :ref:`extension <extend-store>` of the original store, i.e., they must only modify mutable contents and must not have instances removed. Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all data and code in it is well-typed. -$${rule: {Step/call_host-*}} +$${rule: {Step/call_addr-hostfunc-*}} Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:hf} in current store ${:s} with arguments ${:val^n}. It yields a set of possible outcomes, where each element is either a pair of a modified store ${:s'} and a :ref:`result <syntax-result>`
diff --git a/specification/wasm-3.0/4.3-execution.instructions.spectec b/specification/wasm-3.0/4.3-execution.instructions.spectec index ed86701..3f26a3d 100644 --- a/specification/wasm-3.0/4.3-execution.instructions.spectec +++ b/specification/wasm-3.0/4.3-execution.instructions.spectec
@@ -184,7 +184,7 @@ -- if fi.CODE = FUNC x (LOCAL t)* (instr*) -- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE} -rule Step/call_host-res: +rule Step/call_addr-hostfunc-res: s; f; val^n (CALL_ADDR a) ~> s'; f; $lift_result(result) ---- -- if s.FUNCS[a] = fi @@ -192,7 +192,7 @@ -- if fi.CODE = _HOSTFUNC hf -- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n) -rule Step/call_host-div: +rule Step/call_addr-hostfunc-div: s; f; val^n (CALL_ADDR a) ~> s; f; val^n (CALL_ADDR a) ---- -- if s.FUNCS[a] = fi
diff --git a/specification/wasm-latest/4.3-execution.instructions.spectec b/specification/wasm-latest/4.3-execution.instructions.spectec index 390576e..3f26a3d 100644 --- a/specification/wasm-latest/4.3-execution.instructions.spectec +++ b/specification/wasm-latest/4.3-execution.instructions.spectec
@@ -176,7 +176,7 @@ rule Step_read/call_ref-func: z; (REF.FUNC_ADDR a) (CALL_REF x) ~> (CALL_ADDR a) -rule Step/call_addr: +rule Step/call_addr-func: z; val^n (CALL_ADDR a) ~> z; (FRAME_ m `{f} (LABEL_ m `{eps} instr*)) ---- -- if $funcinst(z)[a] = fi @@ -184,7 +184,7 @@ -- if fi.CODE = FUNC x (LOCAL t)* (instr*) -- if f = {LOCALS val^n ($default_(t))*, MODULE fi.MODULE} -rule Step/call_host-res: +rule Step/call_addr-hostfunc-res: s; f; val^n (CALL_ADDR a) ~> s'; f; $lift_result(result) ---- -- if s.FUNCS[a] = fi @@ -192,7 +192,7 @@ -- if fi.CODE = _HOSTFUNC hf -- if RES s' result <- $hostcall(_HOSTFUNC hf, s, val^n) -rule Step/call_host-div: +rule Step/call_addr-hostfunc-div: s; f; val^n (CALL_ADDR a) ~> s; f; val^n (CALL_ADDR a) ---- -- if s.FUNCS[a] = fi