equal
deleted
inserted
replaced
7 context tainting_s begin |
7 context tainting_s begin |
8 |
8 |
9 (* simpset for s2ss*) |
9 (* simpset for s2ss*) |
10 |
10 |
11 lemma s2ss_execve: |
11 lemma s2ss_execve: |
12 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s " |
12 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = ( |
|
13 if (\<exists> p'. p' \<noteq> p \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = co2sobj s (O_proc p)) |
|
14 then (case (cp2sproc (Execve p f fds # s) s2ss s \<union> {} " |