Wp.Splitter
type tag =
| THEN of Frama_c_kernel.Cil_types.stmt |
| ELSE of Frama_c_kernel.Cil_types.stmt |
| CALL of Frama_c_kernel.Cil_types.stmt
* Frama_c_kernel.Cil_types.kernel_function |
| CASE of Frama_c_kernel.Cil_types.stmt * int64 list |
| DEFAULT of Frama_c_kernel.Cil_types.stmt |
| ASSERT of Frama_c_kernel.Cil_types.identified_predicate * int * int |
val loc : tag -> Frama_c_kernel.Cil_types.location
val pretty : Stdlib.Format.formatter -> tag -> unit
val if_then : Frama_c_kernel.Cil_types.stmt -> tag
val if_else : Frama_c_kernel.Cil_types.stmt -> tag
val switch_cases : Frama_c_kernel.Cil_types.stmt -> int64 list -> tag
val switch_default : Frama_c_kernel.Cil_types.stmt -> tag
val cases :
Frama_c_kernel.Cil_types.identified_predicate ->
(tag * Frama_c_kernel.Cil_types.predicate) list option
val call :
Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.kernel_function ->
tag
val empty : 'a t
val singleton : 'a -> 'a t
val length : 'a t -> int
val exists : ( 'a -> bool ) -> 'a t -> bool
val for_all : ( 'a -> bool ) -> 'a t -> bool