attribute ttynode;
attribute ptynode;

#
# console_device_t is the type of /dev/console.
#
type console_device_t;

devices_make_device_node(console_device_t)

#
# devtty_t is the type of /dev/tty.
#
type devtty_t;

devices_make_device_node(devtty_t)

#
# tty_device_t is the type of /dev/*tty*
#
type tty_device_t, ttynode;

devices_make_device_node(tty_device_t)

#
# bsdpty_device_t is the type of /dev/[tp]ty[abcdepqrstuvwxyz][0-9a-f]
type bsdpty_device_t, ptynode;

devices_make_device_node(bsdpty_device_t)


# ptmx_t is the type for /dev/ptmx.
type ptmx_t;

devices_make_device_node(ptmx_t)

#
# devpts_t is the type of the devpts file system and 
# the type of the root directory of the file system.
#
type devpts_t;