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 Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Module `E_ACSL.Translate_annots`

Functions that translate a given ACSL annotation into the corresponding C statements (if any) for runtime assertion checking. These C statements are part of the resulting environment.

val pre_funspec : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Env.t ->
  Frama_c_kernel.Cil_types.funspec ->
  Env.t

Translate the preconditions of the given function contract in the environment. The contract is attached to the kernel_function.

The function contract is pushed in the environment, some care should be taken to call post_funspec at the right time to pop the right contract.

val post_funspec : Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Env.t

Translate the postconditions of the current function contract in the environment.

The function contract previously built by pre_funspec is popped from the environment. Some care should be taken to call this function at the right time to pop the right contract.

val pre_code_annotation : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Env.t ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Env.t

Translate the preconditions of the given code annotation in the environment.

If available, the statement contract is pushed in the environment, some care should be taken to call post_code_annotation at the right time to pop the right contract.

val post_code_annotation : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Env.t ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Env.t

Translate the postconditions of the current code annotation in the environment.

If necessarry, the statement contract previously built by pre_code_annotation is popped from the environment. Some care should be taken to call this function at the right time to pop the right contract.