package frama-c
Module Wp.SplitterSource
Source
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
Source
val cases :
Frama_c_kernel.Cil_types.identified_predicate ->
(tag * Frama_c_kernel.Cil_types.predicate) list option