sig
type tag =
MARK of Cil_types.stmt
| THEN of Cil_types.stmt
| ELSE of Cil_types.stmt
| CALL of Cil_types.stmt * Cil_types.kernel_function
| CASE of Cil_types.stmt * int64 list
| DEFAULT of Cil_types.stmt
| ASSERT of Cil_types.identified_predicate * int * int
val loc : Wp.Splitter.tag -> Cil_types.location
val pretty : Format.formatter -> Wp.Splitter.tag -> unit
val mark : Cil_types.stmt -> Wp.Splitter.tag
val if_then : Cil_types.stmt -> Wp.Splitter.tag
val if_else : Cil_types.stmt -> Wp.Splitter.tag
val switch_cases : Cil_types.stmt -> int64 list -> Wp.Splitter.tag
val switch_default : Cil_types.stmt -> Wp.Splitter.tag
val cases :
Cil_types.identified_predicate ->
(Wp.Splitter.tag * Cil_types.predicate) list option
val call : Cil_types.stmt -> Cil_types.kernel_function -> Wp.Splitter.tag
type 'a t
val empty : 'a Wp.Splitter.t
val singleton : 'a -> 'a Wp.Splitter.t
val group :
Wp.Splitter.tag ->
('a list -> 'a) -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
val union :
('a -> 'a -> 'a) ->
'a Wp.Splitter.t -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
val merge :
left:('a -> 'c) ->
both:('a -> 'b -> 'c) ->
right:('b -> 'c) ->
'a Wp.Splitter.t -> 'b Wp.Splitter.t -> 'c Wp.Splitter.t
val merge_all :
('a list -> 'a) -> 'a Wp.Splitter.t list -> 'a Wp.Splitter.t
val length : 'a Wp.Splitter.t -> int
val map : ('a -> 'b) -> 'a Wp.Splitter.t -> 'b Wp.Splitter.t
val iter : (Wp.Splitter.tag list -> 'a -> unit) -> 'a Wp.Splitter.t -> unit
val fold :
(Wp.Splitter.tag list -> 'a -> 'b -> 'b) -> 'a Wp.Splitter.t -> 'b -> 'b
val exists : ('a -> bool) -> 'a Wp.Splitter.t -> bool
val for_all : ('a -> bool) -> 'a Wp.Splitter.t -> bool
val filter : ('a -> bool) -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
end