23 |
23 |
24 "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = |
24 "exec_instr (LitPush v) G hp stk vars Cl sig pc frs = |
25 (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
25 (None, hp, (v # stk, vars, Cl, sig, pc+1)#frs)" |
26 |
26 |
27 "exec_instr (New C) G hp stk vars Cl sig pc frs = |
27 "exec_instr (New C) G hp stk vars Cl sig pc frs = |
28 (let xp' = raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory; |
28 (let (oref,xp') = new_Addr hp; |
29 oref = newref hp; |
|
30 fs = init_vars (fields(G,C)); |
29 fs = init_vars (fields(G,C)); |
31 hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp; |
30 hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp; |
32 stk' = if xp'=None then (Addr oref)#stk else stk |
31 stk' = if xp'=None then (Addr oref)#stk else stk |
33 in |
32 in |
34 (xp', hp', (stk', vars, Cl, sig, pc+1)#frs))" |
33 (xp', hp', (stk', vars, Cl, sig, pc+1)#frs))" |