Module Splitter

module Splitter: sig .. end

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 pretty : Format.formatter -> tag -> unit
val loc : tag -> Cil_types.location
val compare : tag -> tag -> int
val disjunction : Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named list
val unwrap : Cil_types.predicate Cil_types.named ->
Cil_types.predicate Cil_types.named list
val predicate : Cil_types.identified_predicate -> Cil_types.predicate Cil_types.named
val enumerate : Cil_types.identified_predicate ->
int -> int -> 'a list -> (tag * 'a) list
val cases : Cil_types.identified_predicate ->
(tag * Cil_types.predicate Cil_types.named) list option
val switch_cases : Cil_types.stmt -> int64 list -> tag
val switch_default : Cil_types.stmt -> tag
val if_then : Cil_types.stmt -> tag
val if_else : Cil_types.stmt -> tag
val mark : Cil_types.stmt -> tag
val call : Cil_types.stmt -> Cil_types.kernel_function -> tag
module Tags: Qed.Listset.Make(sig
type t = Splitter.tag 
val compare : Splitter.tag -> Splitter.tag -> int
val equal : Splitter.tag -> Splitter.tag -> bool
end)
module M: Qed.Listmap.Make(Tags)
module I: FCMap.Make(Tags)
type 'a t = 'a M.t 
val compact : ('a list -> 'a) -> (Tags.t * 'a) list -> (Tags.t * 'a) list
val collect : ('a list -> 'a) ->
Tags.t ->
'a list -> (Tags.t * 'a) list -> (Tags.t * 'a) list
val bytags : Tags.t * 'a -> Tags.t * 'b -> int
val group : Tags.elt ->
('a list -> 'a) -> (Tags.t * 'a) list -> (Tags.t * 'a) list
val length : 'a list -> int
val empty : 'a list
val singleton : 'a -> ('b list * 'a) list
val union : ('a -> 'a -> 'a) -> 'a M.t -> 'a M.t -> 'a M.t
val merge : left:('a -> 'b) ->
both:('a -> 'c -> 'b) ->
right:('c -> 'b) ->
(Tags.t * 'a) list ->
(Tags.t * 'c) list -> (Tags.t * 'b) list
val merge_all : ('a list -> 'a) -> 'a M.t list -> 'a M.t
val map : ('a -> 'b) -> 'a M.t -> 'b M.t
val iter : (M.key -> 'a -> unit) -> 'a M.t -> unit
val fold : (M.key -> 'a -> 'b -> 'b) -> 'a M.t -> 'b -> 'b
val exists : ('a -> bool) -> ('b * 'a) list -> bool
val for_all : ('a -> bool) -> ('b * 'a) list -> bool
val filter : ('a -> bool) -> ('b * 'a) list -> ('b * 'a) list