equal
deleted
inserted
replaced
675 apply (rule_tac x = obj in exI, simp add:alive_simps co2sobj_readfile split:t_object.splits) |
675 apply (rule_tac x = obj in exI, simp add:alive_simps co2sobj_readfile split:t_object.splits) |
676 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
676 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
677 apply (rule_tac x = obj in exI, simp add:alive_simps) |
677 apply (rule_tac x = obj in exI, simp add:alive_simps) |
678 apply (drule_tac obj = obj in co2sobj_readfile, simp) |
678 apply (drule_tac obj = obj in co2sobj_readfile, simp) |
679 apply (simp split:t_object.splits) |
679 apply (simp split:t_object.splits) |
680 apply (simp add:co2sobj.simps)+ |
|
681 done |
680 done |
682 |
681 |
683 lemma same_inode_files_prop9: |
682 lemma same_inode_files_prop9: |
684 "is_file s f \<Longrightarrow> f \<in> same_inode_files s f" |
683 "is_file s f \<Longrightarrow> f \<in> same_inode_files s f" |
685 by (simp add:same_inode_files_def) |
684 by (simp add:same_inode_files_def) |
2551 apply simp |
2550 apply simp |
2552 apply (rule_tac x = obj in exI) |
2551 apply (rule_tac x = obj in exI) |
2553 apply (auto simp add:co2sobj_createshm alive_simps split:t_object.splits if_splits) |
2552 apply (auto simp add:co2sobj_createshm alive_simps split:t_object.splits if_splits) |
2554 done |
2553 done |
2555 |
2554 |
2556 |
2555 end |
2557 lemma s2ss_attach1: |
2556 |
2558 "valid (Attach p h SHM_RDWR # s) \<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = " |
2557 end |
2559 |
|
2560 lemma s2ss_attach1: |
|
2561 "valid (Attach p h SHM_RDONLY # s) \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = " |
|
2562 |
|
2563 lemma s2ss_attach1: |
|
2564 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = " |
|
2565 |
|
2566 lemma s2ss_Detach: |
|
2567 "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = " |
|
2568 |
|
2569 lemma s2ss_deleteshm: |
|
2570 "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s)" |
|
2571 |
|
2572 |
|
2573 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
|
2574 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
|
2575 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
|
2576 s2ss_createshm |
|
2577 |
|