Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: JVMExceptions.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/JVM/JVMExceptions.thy
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2001 Technische Universitaet Muenchen
*)

section \<open>Exception handling in the JVM\<close>

theory JVMExceptions imports JVMInstructions begin

definition match_exception_entry :: "jvm_prog \ cname \ p_count \ exception_entry \ bool" where
  "match_exception_entry G cn pc ee ==
                 let (start_pc, end_pc, handler_pc, catch_type) = ee in
                 start_pc <= pc \<and> pc < end_pc \<and> G\<turnstile> cn \<preceq>C catch_type"

primrec match_exception_table :: "jvm_prog \ cname \ p_count \ exception_table
    \<Rightarrow> p_count option"
where
  "match_exception_table G cn pc [] = None"
| "match_exception_table G cn pc (e#es) = (if match_exception_entry G cn pc e
                                           then Some (fst (snd (snd e)))
                                           else match_exception_table G cn pc es)"

abbreviation
  ex_table_of :: "jvm_method \ exception_table"
  where "ex_table_of m == snd (snd (snd m))"

primrec find_handler :: "jvm_prog \ val option \ aheap \ frame list
    \<Rightarrow> jvm_state"
where
  "find_handler G xcpt hp [] = (xcpt, hp, [])"
| "find_handler G xcpt hp (fr#frs) =
      (case xcpt of
         None \<Rightarrow> (None, hp, fr#frs)
       | Some xc \<Rightarrow>
       let (stk,loc,C,sig,pc) = fr in
       (case match_exception_table G (cname_of hp xc) pc
              (ex_table_of (snd(snd(the(method (G,C) sig))))) of
          None \<Rightarrow> find_handler G (Some xc) hp frs
        | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))"

text \<open>
  System exceptions are allocated in all heaps:
\<close>

text \<open>
  Only program counters that are mentioned in the exception table
  can be returned by \<^term>\<open>match_exception_table\<close>:
\<close>
lemma match_exception_table_in_et:
  "match_exception_table G C pc et = Some pc' \ \e \ set et. pc' = fst (snd (snd e))"
  by (induct et) (auto split: if_split_asm)

end

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.