461 *) |
461 *) |
462 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
462 definition info_flow_sproc_sshms :: "t_sproc_sshm set \<Rightarrow> t_sproc_sshm set \<Rightarrow> bool" |
463 where |
463 where |
464 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
464 "info_flow_sproc_sshms shms shms' \<equiv> (\<exists> sh flag'. (sh, SHM_RDWR) \<in> shms \<and> (sh, flag') \<in> shms')" |
465 |
465 |
|
466 (* |
466 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
467 fun info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
467 where |
468 where |
468 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
469 "info_flow_sshm (pi,sec,fds,shms) (pi',sec',fds',shms') = info_flow_sproc_sshms shms shms'" |
|
470 *) |
|
471 inductive info_flow_sshm :: "t_sproc \<Rightarrow> t_sproc \<Rightarrow> bool" |
|
472 where |
|
473 "info_flow_sshm sp sp" |
|
474 | "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk> |
|
475 \<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')" |
469 |
476 |
470 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state" |
477 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state" |
471 where |
478 where |
472 "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. |
479 "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. |
473 (case sobj' of |
480 (case sobj' of |