search

Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K
2 stars 2 forks source link

Return priority #33

Closed mariaKt closed 2 months ago

mariaKt commented 2 months ago

There was non determinism between the following two rules for the return statement,

  rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
       <store>... I |-> L ...</store>

  rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
       <env> _ => E </env>
       <call-stack>... ListItem(frame(K, E)) => .List </call-stack>

where a TypedVal lv(Int, .List, Type) would match both. This PR adds the appropriate priority, and updates the reference outputs accordingly.