From 4a588e982b06bdd493b72853ffc320476f630449 Mon Sep 17 00:00:00 2001 From: Tobias Eidelpes Date: Thu, 3 Jun 2021 10:20:37 +0200 Subject: [PATCH] Add RETURN definition --- Project2.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Project2.fst b/Project2.fst index 92729bb..fa6857d 100644 --- a/Project2.fst +++ b/Project2.fst @@ -140,7 +140,7 @@ let step te cs = | (JUMP i, stack') -> Next (Exec((((gas-1, i, mem, stack'), (actor, input, code), gs))::ps)) | (JUMPI i, b::stack') -> let j = (if b = 0 then pc+1 else i) in Next (Exec((((gas-1, j, mem, stack'), (actor, input, code), gs)) :: ps)) - | (RETURN, v::stack') -> magic () + | (RETURN, v::stack') -> Next (Ter (HaltState gs v (gas-1)) ps) | (STOP, stack') -> Next (Ter (HaltState gs 0 (gas-1)) ps) | (TIMESTAMP, stack') -> magic () | (CALL, to::v::inp::resaddr::stack') -> magic ()