| changeset 33 | 6884b3c9284b |
| parent 32 | 705e1e41faf7 |
| child 34 | e7f850d1e08e |
| 32:705e1e41faf7 | 33:6884b3c9284b |
|---|---|
3 imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop |
3 imports Main Flask Flask_type Static Static_type Init_prop Tainted_prop Valid_prop Alive_prop Co2sobj_prop |
4 begin |
4 begin |
5 (*>*) |
5 (*>*) |
6 |
6 |
7 context tainting_s begin |
7 context tainting_s begin |
8 |
|
9 (* simpset for s2ss*) |
|
10 |
|
11 lemma s2ss_execve: |
|
12 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) = s2ss s " |