50 "eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" | |
50 "eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" | |
51 "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) |
51 "eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) |
52 = (PrimT Integer#ST,LT)" | |
52 = (PrimT Integer#ST,LT)" | |
53 "eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" | |
53 "eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" | |
54 "eff' (Goto b, G, s) = s" | |
54 "eff' (Goto b, G, s) = s" | |
55 -- "Return has no successor instruction in the same method" |
55 \<comment> "Return has no successor instruction in the same method" |
56 "eff' (Return, G, s) = s" | |
56 "eff' (Return, G, s) = s" | |
57 -- "Throw always terminates abruptly" |
57 \<comment> "Throw always terminates abruptly" |
58 "eff' (Throw, G, s) = s" | |
58 "eff' (Throw, G, s) = s" | |
59 "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
59 "eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST |
60 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
60 in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" |
61 |
61 |
62 |
62 |