Static_type.thy
changeset 43 137358bd4921
parent 1 7d9c0ed02b56
equal deleted inserted replaced
42:021672ec28f5 43:137358bd4921
    75 datatype t_sobject =
    75 datatype t_sobject =
    76   S_proc "t_sproc"     "bool"
    76   S_proc "t_sproc"     "bool"
    77 | S_file "t_sfile set" "bool"  (* here sfile set is for "linking", tainted is the inode *)
    77 | S_file "t_sfile set" "bool"  (* here sfile set is for "linking", tainted is the inode *)
    78 | S_dir  "t_sfile"     
    78 | S_dir  "t_sfile"     
    79 | S_msgq "t_smsgq"
    79 | S_msgq "t_smsgq"
    80 | S_shm  "t_sshm"
    80 | S_shm  "t_sshm"  (*
    81 | S_msg  "t_smsgq"    "t_smsg"
    81 | S_msg  "t_smsgq"    "t_smsg"
    82 
    82 *)
    83 (*
    83 (*
    84 datatype t_tainted_sobj = 
    84 datatype t_tainted_sobj = 
    85   TS_proc "t_sproc"     "bool"
    85   TS_proc "t_sproc"     "bool"
    86 | TS_file "t_sfile set" "bool"
    86 | TS_file "t_sfile set" "bool"
    87 | TS_msg  "t_smsgq"     "t_smsg"
    87 | TS_msg  "t_smsgq"     "t_smsg"