package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-e-acsl.core/E_ACSL/Translate_utils/index.html

Module `E_ACSL.Translate_utils`

Utility functions for generating C implementations.

val must_translate : Frama_c_kernel.Property.t -> bool

returns
true if the given property must be translated (ie. if the valid properties must be translated or if its status is not True), false otherwise.

val must_translate_opt : Frama_c_kernel.Property.t option -> bool

Same 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.t

Translate 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 : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Env.t ->
  Analyses_types.number_ty ->
  Frama_c_kernel.Cil_types.binop ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.exp ->
  ?name:string ->
  Frama_c_kernel.Cil_types.term option ->
  Frama_c_kernel.Cil_types.exp * Env.t

comparison_to_exp ~loc kf env ity ?name bop e1 e2 topt generates the C code equivalent to e1 bop e2 in the given environment. ity is the number type of the comparison when comparing scalar numbers. 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.t

conditional_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.t

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

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