Frama-C API - Translate_utils
Utility functions for generating C implementations.
val must_translate : Frama_c_kernel.Property.t -> boolval must_translate_opt : Frama_c_kernel.Property.t option -> boolSame than must_translate but for Property.t option. Return false if the option is None.
val gmp_to_sizet : adata:Assert.t -> loc:Frama_c_kernel.Cil_types.location -> name:string -> ?check_lower_bound:bool -> ?pp:Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.tTranslate the given GMP integer to an expression of type size_t. RTE checks are generated to ensure that the GMP value holds in this type. The parameter name is used to generate relevant predicate names. If check_lower_bound is set to false, then the GMP value is assumed to be positive. If pp is provided, this term is used in the messages of the RTE checks.
val comparison_to_exp : adata:Assert.t -> loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Analyses_types.number_ty -> ?e1:Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.binop -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.term -> ?name:string -> Frama_c_kernel.Cil_types.term option -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.tcomparison_to_exp ~data ~loc kf env ity ?e1 ?name bop t1 t2 topt generates the C code equivalent to t1 bop t2 in the given environment with the given assertion context. ity is the number type of the comparison when comparing scalar numbers. e1 is the expression representing t1 if the term has already been translated. name is used to generate temporary variable names. topt is the term holding the result of the comparison.
val conditional_to_exp : ?name:string -> loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.term option -> Frama_c_kernel.Cil_types.exp -> (Frama_c_kernel.Cil_types.exp * Env.t) -> (Frama_c_kernel.Cil_types.exp * Env.t) -> Frama_c_kernel.Cil_types.exp * Env.tconditional_to_exp ?name ~loc kf t_opt e1 (e2, env2) (e3, env3) generates the C code equivalent to e1 ? e2 : e3 in the given environment. env2 and env3 are the environment respectively for e2 and e3. t_opt is the term holding the result of the conditional.
val env_of_li : adata:Assert.t -> loc:Frama_c_kernel.Cil_types.location -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.logic_info -> Assert.t * Env.tenv_of_li ~adata ~loc kf env li translates the logic info li in the given environment with the given assertion context.
val term_to_exp_ref : (adata:Assert.t -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.t) Stdlib.refval predicate_to_exp_ref : (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) Stdlib.ref