Skip to content

Commit

Permalink
Update TEST.md
Browse files Browse the repository at this point in the history
  • Loading branch information
ShinWonho committed Jul 15, 2024
1 parent 09dadf7 commit 3bc3fa8
Showing 1 changed file with 10 additions and 8 deletions.
18 changes: 10 additions & 8 deletions spectec/test-prose/TEST.md
Original file line number Diff line number Diff line change
Expand Up @@ -979,8 +979,8 @@ execution_of_FRAME_
execution_of_RETURN
1. Pop all values val* from the top of the stack.
2. If a frame is now on the top of the stack, then:
a. Let F be the current frame.
b. Let n be the arity of F.
a. Let f be the current frame.
b. Let n be the arity of f.
c. Pop the current frame from the stack.
d. Let val'* ++ val^n be val*.
e. Push the values val^n to the stack.
Expand Down Expand Up @@ -2895,8 +2895,8 @@ execution_of_FRAME_
execution_of_RETURN
1. Pop all values val* from the top of the stack.
2. If a frame is now on the top of the stack, then:
a. Let F be the current frame.
b. Let n be the arity of F.
a. Let f be the current frame.
b. Let n be the arity of f.
c. Pop the current frame from the stack.
d. Let val'* ++ val^n be val*.
e. Push the values val^n to the stack.
Expand Down Expand Up @@ -6077,10 +6077,12 @@ with_data x b*
2. Replace s.DATAS[f.MODULE.DATAS[x]].BYTES with b*.

with_struct a i fv
1. Replace s.STRUCTS[a].FIELDS[i] with fv.
1. Let f be the current frame.
2. Replace s.STRUCTS[a].FIELDS[i] with fv.

with_array a i fv
1. Replace s.ARRAYS[a].FIELDS[i] with fv.
1. Let f be the current frame.
2. Replace s.ARRAYS[a].FIELDS[i] with fv.

ext_structinst si*
1. Let f be the current frame.
Expand Down Expand Up @@ -6518,8 +6520,8 @@ execution_of_FRAME_
execution_of_RETURN
1. Pop all values val* from the top of the stack.
2. If a frame is now on the top of the stack, then:
a. Let F be the current frame.
b. Let n be the arity of F.
a. Let f be the current frame.
b. Let n be the arity of f.
c. Pop the current frame from the stack.
d. Let val'* ++ val^n be val*.
e. Push the values val^n to the stack.
Expand Down

0 comments on commit 3bc3fa8

Please sign in to comment.