equal
deleted
inserted
replaced
953 done |
953 done |
954 qed |
954 qed |
955 ultimately show ?case using vd_enrich_cons sf_cons tainted_cons |
955 ultimately show ?case using vd_enrich_cons sf_cons tainted_cons |
956 by auto |
956 by auto |
957 qed |
957 qed |
|
958 |
|
959 fun enrich_file_link :: "t_state \<Rightarrow> t_file \<Rightarrow> t_state \<Rightarrow> (t_file \<times> t_state)" |
|
960 where |
|
961 "enrich_file_link [] tf df = []" |
|
962 |
|
963 fun enrich_file_set :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> t_state" |
|
964 where |
|
965 "enrich_file_set [] tf df = []" |
|
966 | "enrich_file_set [] (Open p f flags fd (Some inum) # s) = |
|
967 |
|
968 |
958 |
969 |
959 |
970 |
960 |
971 |
961 lemma enrich_msgq_s2ss: |
972 lemma enrich_msgq_s2ss: |
962 "" |
973 "" |