Merge pull request #13313 from QGarchery/develop

fix: global state object in yul formal specification
This commit is contained in:
chriseth 2022-07-28 15:30:44 +02:00 committed by GitHub
commit d5a78b18b3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -663,10 +663,10 @@ We will use a destructuring notation for the AST nodes.
E(G, L, <var_1, ..., var_n := rhs>: Assignment) = E(G, L, <var_1, ..., var_n := rhs>: Assignment) =
let G1, L1, v1, ..., vn = E(G, L, rhs) let G1, L1, v1, ..., vn = E(G, L, rhs)
let L2 be a copy of L1 where L2[$var_i] = vi for i = 1, ..., n let L2 be a copy of L1 where L2[$var_i] = vi for i = 1, ..., n
G, L2, regular G1, L2, regular
E(G, L, <for { i1, ..., in } condition post body>: ForLoop) = E(G, L, <for { i1, ..., in } condition post body>: ForLoop) =
if n >= 1: if n >= 1:
let G1, L, mode = E(G, L, i1, ..., in) let G1, L1, mode = E(G, L, i1, ..., in)
// mode has to be regular or leave due to the syntactic restrictions // mode has to be regular or leave due to the syntactic restrictions
if mode is leave then if mode is leave then
G1, L1 restricted to variables of L, leave G1, L1 restricted to variables of L, leave
@ -686,7 +686,7 @@ We will use a destructuring notation for the AST nodes.
else: else:
G3, L3, mode = E(G2, L2, post) G3, L3, mode = E(G2, L2, post)
if mode is leave: if mode is leave:
G2, L3, leave G3, L3, leave
otherwise otherwise
E(G3, L3, for {} condition post body) E(G3, L3, for {} condition post body)
E(G, L, break: BreakContinue) = E(G, L, break: BreakContinue) =