--- a/Static_type.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Static_type.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -77,9 +77,9 @@
 | S_file "t_sfile set" "bool"  (* here sfile set is for "linking", tainted is the inode *)
 | S_dir  "t_sfile"     
 | S_msgq "t_smsgq"
-| S_shm  "t_sshm"
+| S_shm  "t_sshm"  (*
 | S_msg  "t_smsgq"    "t_smsg"
-
+*)
 (*
 datatype t_tainted_sobj = 
   TS_proc "t_sproc"     "bool"