ROOT
author chunhan
Mon, 24 Jun 2013 09:01:42 +0800
changeset 25 259a50be4381
parent 11 3e7617baa6a3
child 34 e7f850d1e08e
permissions -rw-r--r--
wrong of info-flow-shm, it is a inductive(transitive) notion, not a simple relation just between 2 nodes, more information, see 5.7 of ideas_of_selinux.txt
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     1
session "dynamic" = "HOL" +
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     2
  options [document = false]
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     3
  theories
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     4
    List_Prefix
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     5
    My_list_prefix
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     6
    File_renaming
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     7
    Flask_type
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     8
    OS_type_def
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
     9
    Flask
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    10
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    11
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    12
session "alive" = "dynamic" + 
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    13
  options [document = false]
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    14
  theories
11
chunhan
parents: 1
diff changeset
    15
    Static_type
chunhan
parents: 1
diff changeset
    16
    Static
1
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    17
    Valid_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    18
    Init_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    19
    Current_files_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    20
    Current_sockets_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    21
    Alive_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    22
    Proc_fd_of_file_prop
7d9c0ed02b56 thy files
chunhan
parents:
diff changeset
    23
    Finite_current
11
chunhan
parents: 1
diff changeset
    24
    New_obj_prop