package frama-c-e-acsl

  1. Overview
  2. Docs
This package contains the Frama-C's E-ACSL plug-in.

Install

Dune Dependency

Authors

Maintainers

Sources

e-acsl-0.5.tar.gz
sha256=f31230143af885aee73f907c2cf0d167a8c71103efb763909b7fb2f1f88b08f7
md5=73842963dfa22548a571c5ccca757bc9

Description

It takes as input an annotated C program and returns the same program in which annotations have been converted into C code dedicated to runtime assertion checking: this code fails at runtime if the annotation is violated at runtime.

Annotations must be written in a subset of ACSL (ANSI/ISO C Specification Language), namely E-ACSL (Executable ANSI/ISO C Specification Language). E-ACSL is fully described at http://frama-c.com/download/e-acsl/e-acsl.pdf

Dependencies (3)

  1. conf-autoconf
  2. frama-c-base >= "11.0"
  3. ocaml >= "3.12" & != "4.02.0"

Dev Dependencies

None

Used by

None

Conflicts

None

OCaml

Innovation. Community. Security.