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

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

type t = Contract_types.contract

val create : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.spec ->
  t

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