package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

OCaml

Innovation. Community. Security.