evm.md: don't store <endPC> for VMTESTS execmode

runtimeverification · Apr 2, 2020 · 5f22e47 · 5f22e47
1 parent 769a747
commit 5f22e47
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/evm.md b/evm.md
@@ -266,6 +266,10 @@ Control Flow
          <statusCode> _ => SC     </statusCode>
          <endPC>      _ => PCOUNT </endPC>
          <pc>         PCOUNT      </pc>
+         <mode>       EXECMODE    </mode>
+      requires EXECMODE =/=K VMTESTS
+
+    rule <k> #end SC => #halt ... </k> <statusCode> _ => SC </statusCode> <mode> VMTESTS </mode>
 
     rule <k> #halt ~> (_:Int    => .) ... </k>
     rule <k> #halt ~> (_:OpCode => .) ... </k>