E_ACSL.Quantif
Convert quantifiers.
val quantif_to_exp :
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.exp * Env.t
The given predicate must be a quantification.
val predicate_to_exp_ref :
( adata:Assert.t ->
Frama_c_kernel.Cil_types.kernel_function ->
Env.t ->
Frama_c_kernel.Cil_types.predicate ->
Frama_c_kernel.Cil_types.exp * Assert.t * Env.t )
Stdlib.ref