frama-c-e-acsl

AuthorsJulien Signoles and Guillaume Petiot
LicenseLGPL-2.1
Homepagehttp://frama-c.com/eacsl.html
Issue Trackerhttps://bts.frama-c.com/
Tagsprogram verification, formal specification, runtime assertion checking, monitoring, C, plugins, ACSL and E-ACSL
Maintainerjulien.signoles@cea.fr
Dependencies
&conf-autoconf
frama-c-base>= 20150201
Availableocaml-version >= "3.12" & ocaml-version != "4.02.0"
PublishedJun 9, 2015
Source [http] http://frama-c.com/download/e-acsl/e-acsl-0.5.tar.gz
73842963dfa22548a571c5ccca757bc9
StatisticsNot installed in the last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/frama-c-e-acsl/frama-c-e-acsl.0.5/opam

This package contains the Frama-C's E-ACSL plug-in.

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

No package is dependent