1 theory Tainted_prop 

     2 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop

     3 begin

     4 

     5 context tainting begin

     6 

     7 lemma tainted_in_current:

     8   "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"

     9 apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)

    10 

    11 

    12 

    13 

    14 end

    15 

    16 end

    17 

    18 

    19 

    20