sig
  type state
  val top : Abstract_domain.Lattice.state
  val is_included :
    Abstract_domain.Lattice.state -> Abstract_domain.Lattice.state -> bool
  val join :
    Abstract_domain.Lattice.state ->
    Abstract_domain.Lattice.state -> Abstract_domain.Lattice.state
  val join_and_is_included :
    Abstract_domain.Lattice.state ->
    Abstract_domain.Lattice.state -> Abstract_domain.Lattice.state * bool
  val widen :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    Abstract_domain.Lattice.state ->
    Abstract_domain.Lattice.state -> Abstract_domain.Lattice.state
end