Frama-C:
Plug-ins:
Libraries:

Frama-C API - Translate_terms

Generate C implementations of E-ACSL terms.

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.

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

Convert an untyped ACSL term into a corresponding C expression.