package frama-c

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

Translate a given ACSL contract (function or statement) into the corresponding C statement for runtime assertion checking.

Create a contract from a spec object (either function spec or statement spec)

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

Translate the preconditions of the given contract into the environement

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

Translate the postconditions of the given contract into the environment