(* Title: HOL/MicroJava/JVM/Method.thy
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
Method invocation
*)
Method = JVMState +
(** method invocation and return instructions **)
datatype
meth_inv =
Invokevirtual mname (ty list) (** inv. instance meth of an object **)
consts
exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
primrec
"exec_mi (Invokevirtual mn ps) G hp stk pc =
(let n = length ps;
argsoref = take (n+1) stk;
oref = last argsoref;
xp' = raise_xcpt (oref=Null) NullPointer;
dynT = fst(hp \\<And> (the_Addr oref));
(dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
in
(xp' , frs' , drop (n+1) stk , pc+1))"
constdefs
exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
"exec_mr stk0 frs \\<equiv>
(let val = hd stk0;
(stk,loc,cn,met,pc) = hd frs
in
(val#stk,loc,cn,met,pc)#tl frs)"
end