diff -r f27ba31b7e96 -r 6f7b9039715f no_shm_selinux/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/no_shm_selinux/ROOT	Tue Dec 17 13:30:21 2013 +0800
@@ -0,0 +1,38 @@
+session "dynamic" = "HOL" +
+  options [document = false]
+  theories
+    List_Prefix
+    My_list_prefix
+    File_renaming
+    Flask_type
+    OS_type_def
+    Flask
+
+
+session "alive" = "dynamic" + 
+  options [document = false]
+  theories
+    Static_type
+    Static
+    Valid_prop
+    Init_prop
+    Current_files_prop
+    Current_sockets_prop
+    Alive_prop
+    Proc_fd_of_file_prop
+    Finite_current
+    New_obj_prop
+
+session "co2sobj" = "alive" + 
+  options [document = false]
+  theories
+    Sectxt_prop
+    Delete_prop
+    Tainted_prop
+    Co2sobj_prop
+
+session "s2ss" = "co2sobj" +
+  options [document = false]
+  theories
+    S2ss_prop
+    S2ss_prop2
\ No newline at end of file