found a bug: has_same_inode is a redundant concept of same_inode_files, which is the general form, has_same_inode should be deleted
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