Static.thy
changeset 37 029cccce84b4
parent 34 e7f850d1e08e
child 39 13bba99ca090
equal deleted inserted replaced
36:1397b2a763ab 37:029cccce84b4
    97   "init_obj2sobj (O_proc p) = 
    97   "init_obj2sobj (O_proc p) = 
    98      (case (init_cp2sproc p) of 
    98      (case (init_cp2sproc p) of 
    99        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
    99        Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> seeds))
   100      | _ \<Rightarrow> None)"
   100      | _ \<Rightarrow> None)"
   101 | "init_obj2sobj (O_file f) = 
   101 | "init_obj2sobj (O_file f) = 
   102      (if (f \<in> init_files \<and> is_init_file f) 
   102      Some (S_file (init_cf2sfiles f) 
   103       then Some (S_file (init_cf2sfiles f) 
   103                   (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))"
   104                         (\<exists> f'. f' \<in> (init_same_inode_files f) \<and> O_file f \<in> seeds))
   104 | "init_obj2sobj (O_dir f) =
   105       else None)"
   105      (case (init_cf2sfile f) of
   106 | "init_obj2sobj (O_dir f) = 
   106         Some sf \<Rightarrow> Some (S_dir sf) 
   107      (if (is_init_dir f) then 
   107       | _ \<Rightarrow> None)"
   108         (case (init_cf2sfile f) of
       
   109            Some sf \<Rightarrow> Some (S_dir sf) 
       
   110          | _ \<Rightarrow> None)
       
   111       else None)"
       
   112 | "init_obj2sobj (O_msgq q) = 
   108 | "init_obj2sobj (O_msgq q) = 
   113      (case (init_cq2smsgq q) of
   109      (case (init_cq2smsgq q) of
   114        Some sq \<Rightarrow> Some (S_msgq sq)
   110        Some sq \<Rightarrow> Some (S_msgq sq)
   115      | _ \<Rightarrow> None)"
   111      | _ \<Rightarrow> None)"
   116 | "init_obj2sobj (O_shm h) = 
   112 | "init_obj2sobj (O_shm h) = 
   771   "co2sobj s (O_proc p) = 
   767   "co2sobj s (O_proc p) = 
   772      (case (cp2sproc s p) of 
   768      (case (cp2sproc s p) of 
   773         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
   769         Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
   774       | _       \<Rightarrow> None)"
   770       | _       \<Rightarrow> None)"
   775 | "co2sobj s (O_file f) = 
   771 | "co2sobj s (O_file f) = 
   776      (if (f \<in> current_files s) then 
   772      Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
   777         Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))
       
   778       else None)"
       
   779 | "co2sobj s (O_dir f) = 
   773 | "co2sobj s (O_dir f) = 
   780      (case (cf2sfile s f) of
   774      (case (cf2sfile s f) of
   781         Some sf  \<Rightarrow> Some (S_dir sf)
   775         Some sf  \<Rightarrow> Some (S_dir sf)
   782       | _ \<Rightarrow> None)"
   776       | _ \<Rightarrow> None)"
   783 | "co2sobj s (O_msgq q) = 
   777 | "co2sobj s (O_msgq q) =