Web3: use #clearGas in #eth_call_finalize (#577)

* web3.md: use #clearGas in #eth_call_finalize * web3.md: formatting * web3: formatting
runtimeverification · Nov 29, 2019 · 852e14e · 852e14e
1 parent 2680b07
commit 852e14e
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/web3.md b/web3.md
@@ -1277,7 +1277,13 @@ Transaction Receipts
 
     syntax KItem ::= "#eth_call_finalize"
  // -------------------------------------
-    rule <k> #eth_call_finalize => #setMode NORMAL ~> #popNetworkState ~> #rpcResponseSuccess(#unparseDataByteArray( OUTPUT )) ... </k>
+    rule <k> #eth_call_finalize
+          => #setMode NORMAL
+          ~> #popNetworkState
+          ~> #clearGas
+          ~> #rpcResponseSuccess(#unparseDataByteArray( OUTPUT ))
+         ...
+        </k>
          <output> OUTPUT </output>
 ```