3 Temp Enrich Proc_fd_of_file_prop |
3 Temp Enrich Proc_fd_of_file_prop |
4 begin |
4 begin |
5 |
5 |
6 context tainting_s begin |
6 context tainting_s begin |
7 |
7 |
8 fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)" |
8 fun new_cf :: "t_state \<Rightarrow> t_file set \<Rightarrow> t_file \<Rightarrow> t_file" |
9 where |
9 where |
10 "enrich_file [] tf s = ({}, [])" |
10 "new_cf s fs [] = []" |
11 | "enrich_file (Open p f flags fd (Some inum) # s) tf s = |
11 | "new_cf s fs (f#pf) = new_childf_general pf s fs" |
12 " |
12 |
13 |
13 fun enrich_dufs:: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_file) list" |
|
14 where |
|
15 "enrich_dufs [] tf s = []" |
|
16 | "enrich_dufs (Open p f flags fd (Some inum) # s) tf s' = |
|
17 (if (f \<in> same_inode_files s' tf) |
|
18 then [(f, new_cf s' {} f)] |
|
19 else enrich_dufs s tf s')" |
|
20 | "enrich_dufs (LinkHard p f f' # s) tf s' = |
|
21 (if (f' \<in> same_inode_files s' tf) |
|
22 then (f', new_cf s' (set (map snd (enrich_dufs s tf s'))) f') # enrich_dufs s tf s' |
|
23 else enrich_dufs s tf s')" |
|
24 | "enrich_dufs (_ # s) tf s' = enrich_dufs s tf s'" |
|
25 |
|
26 lemma enrich_dufs_sameinodes: |
|
27 "valid s \<Longrightarrow> set (map snd (enrich_dufs s f s)) = same_inode_files s f" |
|
28 thm enrich_dufs.induct |
|
29 apply (induct rule:enrich_dufs.induct) |
|
30 |
|
31 apply (erule enrich_dufs.induct) |
|
32 |
|
33 fun enrich_file :: "t_state \<Rightarrow> t_file \<Rightarrow> t_inode_num \<Rightarrow> t_state \<Rightarrow> (t_file set \<times> t_state)" |
|
34 where |
|
35 "enrich_file [] tf ninum s = ({}, [])" |
|
36 | "enrich_file (Open p f flags fd (Some inum) # s) tf ninum s = |
|
37 if (f \<in> same_inode_fies s tf) |
|
38 then Open p f flags fd (Some" |
14 |
39 |
15 |
40 |
16 |
41 |
17 |
42 |
18 lemma enrich_msgq_s2ss: |
43 lemma enrich_msgq_s2ss: |