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-27.0-beta-Cobalt.tar.gz

sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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

comparison_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.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