diff -r 7d9c0ed02b56 -r 5a01ee1c9b4d Static.thy --- a/Static.thy Fri May 03 08:20:21 2013 +0100 +++ b/Static.thy Mon May 06 02:04:27 2013 +0800 @@ -51,7 +51,7 @@ definition init_cfs2sfiles :: "t_file set \ t_sfile set" where - "init_cfs2sfiles fs \ {sf. \f \ fs. init_cf2sfile f = Some sf}" + "init_cfs2sfiles fs \ {sf. \f \ fs. init_cf2sfile f = Some sf \ is_init_file f}" definition init_cfd2sfd :: "t_process \ t_fd \ (security_context_t \ t_open_flags \ t_sfile) option" where @@ -109,10 +109,6 @@ (Some sec, Some sms) \ Some (Init q, sec, sms) | _ \ None)" -definition init_same_inode_files :: "t_file \ t_file set" -where - "init_same_inode_files f \ {f'. init_inum_of_file f = init_inum_of_file f'}" - fun init_obj2sobj :: "t_object \ t_sobject option" where "init_obj2sobj (O_proc p) = @@ -720,10 +716,6 @@ where "cfs2sfiles s fs \ {sf. \ f \ fs. cf2sfile s f True = Some sf}" -definition same_inode_files :: "t_state \ t_file \ t_file set" -where - "same_inode_files s f \ {f'. inum_of_file s f = inum_of_file s f'}" - (* here cf2sfile is passed with True, because, process' fds are only for files not dirs *) definition cfd2sfd :: "t_state \ t_process \ t_fd \ t_sfd option" where