package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Forward references

Module `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.

Forward references

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)
    ref

package frama-c

Module E_ACSL.Quantif

Forward references

Module `E_ACSL.Quantif`