equal
deleted
inserted
replaced
1385 |
1385 |
1386 (* tobj: object that can be tainted *) |
1386 (* tobj: object that can be tainted *) |
1387 fun tobj_in_init :: "t_object \<Rightarrow> bool" |
1387 fun tobj_in_init :: "t_object \<Rightarrow> bool" |
1388 where |
1388 where |
1389 "tobj_in_init (O_proc p) = (p \<in> init_procs)" |
1389 "tobj_in_init (O_proc p) = (p \<in> init_procs)" |
1390 | "tobj_in_init (O_file f) = (f \<in> init_files)" |
1390 | "tobj_in_init (O_file f) = (is_init_file f)" |
1391 (* directory is not taintable |
1391 (* directory is not taintable |
1392 | "tobj_in_init (O_dir f) = (f \<in> init_files)" |
1392 | "tobj_in_init (O_dir f) = (f \<in> init_files)" |
1393 *) |
1393 *) |
1394 | "tobj_in_init (O_node n) = (n \<in> init_nodes)" |
1394 | "tobj_in_init (O_node n) = (n \<in> init_nodes)" |
1395 | "tobj_in_init (O_msg q m) = (member (init_msgs_of_queue q) ((op =) m))" |
1395 | "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)" |
1396 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *) |
1396 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *) |
1397 |
1397 |
1398 (* no use |
1398 (* no use |
1399 fun no_del_event:: "t_event list \<Rightarrow> bool" |
1399 fun no_del_event:: "t_event list \<Rightarrow> bool" |
1400 where |
1400 where |