author | chunhan |
Thu, 29 Aug 2013 13:29:32 +0800 | |
changeset 34 | e7f850d1e08e |
parent 33 | 6884b3c9284b |
child 35 | f2e620d799cf |
permissions | -rw-r--r-- |
(*<*) theory S2ss_prop imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop begin (*>*) context tainting_s begin (* simpset for s2ss*) lemma s2ss_execve: "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p)) then (case (cp2sproc (Execve p f fds # s) s2ss s \<union> {} "