Module Quantif

module Quantif: sig .. end

Convert quantifiers.

val quantif_to_exp : Cil_types.kernel_function ->
       Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t

The given predicate must be a quantification.

Forward references

val predicate_to_exp_ref : (adata:Assert.t ->
        Cil_types.kernel_function ->
        Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
       Stdlib.ref

Forward reference for Translate_predicates.to_exp.