enrich msgq done; but find bugs of s2ss, it should only considerate 'appropriate' objects, not including msg/fd ...
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
session "enrich" = "s2ss" +
options [document = false]
theories
Enrich
Enrich1