# HG changeset patch
# User kleing
# Date 976021702 -3600
# Node ID 6d6cb845e841e9f07a629e3369bee8ab359747d3
# Parent  315afa77adeac01335060b6d889544eac9e7cf4a
jvm_progs now also store maximum op_stack depth

diff -r 315afa77adea -r 6d6cb845e841 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Dec 05 14:08:22 2000 +0100
@@ -19,7 +19,7 @@
 
   "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
   (let 
-     i = snd(snd(snd(the(method (G,C) sig)))) ! pc
+     i = snd(snd(snd(snd(the(method (G,C) sig))))) ! pc
    in
      Some (exec_instr i G hp stk loc C sig pc frs))"
 
diff -r 315afa77adea -r 6d6cb845e841 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Dec 05 14:08:22 2000 +0100
@@ -66,7 +66,7 @@
 	     oref	= last argsoref;
 	     xp'	= raise_xcpt (oref=Null) NullPointer;
 	     dynT	= fst(the(hp(the_Addr oref)));
-	     (dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
+	     (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
 	     frs'	= if xp'=None then 
                 [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
 	            else []
diff -r 315afa77adea -r 6d6cb845e841 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Tue Dec 05 08:22:49 2000 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Tue Dec 05 14:08:22 2000 +0100
@@ -33,6 +33,6 @@
 
 types
   bytecode = "instr list"
-  jvm_prog = "(nat \<times> bytecode) prog" 
+  jvm_prog = "(nat \<times> nat \<times> bytecode) prog" 
 
 end