equal
deleted
inserted
replaced
34 bytecode = "instr list" |
34 bytecode = "instr list" |
35 exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" |
35 exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" |
36 -- "start-pc, end-pc, handler-pc, exception type" |
36 -- "start-pc, end-pc, handler-pc, exception type" |
37 exception_table = "exception_entry list" |
37 exception_table = "exception_entry list" |
38 jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" |
38 jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" |
|
39 -- "max stacksize, length of local var array, \<dots>" |
39 jvm_prog = "jvm_method prog" |
40 jvm_prog = "jvm_method prog" |
40 |
41 |
41 end |
42 end |