--- a/Tainted_prop.thy Thu Sep 05 13:23:03 2013 +0800
+++ b/Tainted_prop.thy Thu Sep 12 13:50:22 2013 +0800
@@ -15,9 +15,9 @@
(if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)"
| "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}"
| "Tainted (Ptrace p p' # s) =
- (if (O_proc p) \<in> Tainted s
+ (if (O_proc p \<in> Tainted s)
then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}
- else if (O_proc p') \<in> Tainted s
+ else if (O_proc p' \<in> Tainted s)
then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}
else Tainted s)"
| "Tainted (Exit p # s) = Tainted s - {O_proc p}"