ROOT
author chunhan
Wed, 08 Jan 2014 18:40:38 +0800
changeset 91 1a1df29d3507
parent 65 6f9a588bcfc4
permissions -rw-r--r--
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