package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Generate C implementations of E-ACSL predicates.

val generalized_untyped_to_exp : adata:Assert.t -> ?name:string -> Frama_c_kernel.Cil_types.kernel_function -> ?rte:bool -> Env.t -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

Convert an untyped ACSL predicate into a corresponding C expression.

Translate the given predicate to a runtime check in the given environment. If pred_to_print is set, then the runtime check will use this predicate as message.

exception No_simple_translation of Frama_c_kernel.Cil_types.predicate

Exceptin raised if untyped_to_exp would generate new statements in the environment

Convert an untyped ACSL predicate into a corresponding C expression. This expression is valid only in certain contexts and shouldn't be used.