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 (26)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-32.0-beta-Germanium.tar.gz

sha256=868d57ef8007fe6c0836cd151d8c294003af34aa678285eff9547662cad36aa3

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

Module `E_ACSL.Translate_terms`

Generate C implementations of E-ACSL terms.

val to_exp : 
  adata:Assert.t ->
  ?inplace:bool ->
  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

to_exp ~adata ?inplace kf env t converts an ACSL term into a corresponding C expression.

adata: assertion context.
inplace: if the root term has a label, indicates if it should be immediately translated or if Translate_ats should be used to retrieve the translation.
kf: The enclosing function.
env: The current environment.
t: The term to translate.

val to_exp_il : 
  ?inplace:bool ->
  Frama_c_kernel.Cil_types.term ->
  Interlang.exp Interlang_gen.m

a version of to_exp that translates ACSL terms to the intermediate language instead to Cil.

val denominator_zero_guard : 
  loc:Frama_c_kernel.Cil_types.location ->
  ctx:Analyses_types.number_ty ->
  adata:Assert.t ->
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  env:Env.t ->
  name:string ->
  ?root:Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.exp
  * Frama_c_kernel.Cil_types.stmt
  * Assert.t
  * Env.t

denominator_zero_guard ~loc ~ctx ~adata ~kf ~env ~name ?root denom converts the ACSL term denom, representing the denominator of a division or modulo, into a corresponding expression using to_exp and a guard statement checking that denom != 0.

loc: location used for the assertion.
ctx: context used to create the zero term of the guard statement.
adata: assertion context.
kf: enclosing function.
env: current environment.
name: used for temporary variable names.
root: root term containing the original division or modulo.
denom: the term to translate.

exception No_simple_translation of Frama_c_kernel.Cil_types.term

Exceptin raised if untyped_to_exp would generate new statements in the environment

val untyped_to_exp : 
  Frama_c_kernel.Cil_types.typ option ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.exp

Convert an untyped ACSL term into a corresponding C expression.

val translate_rte_exp_ref : 
  (?filter:(Frama_c_kernel.Cil_types.code_annotation -> bool) ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.exp ->
    Env.t)
    ref