frama-c-e-acslversion
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
| Tags | program verification formal specification runtime assertion checking monitoring C plugins ACSL E-ACSL |
|---|---|
| Authors | Julien Signoles and Guillaume Petiot |
| License | LGPL-2.1-only |
| Published | |
| Homepage | http://frama-c.com/eacsl.html |
| Issue Tracker | https://bts.frama-c.com/ |
| Maintainer | julien.signoles@cea.fr |
| Dependencies |
|
| Source [http] | http://frama-c.com/download/e-acsl/e-acsl-0.5.tar.gz sha256=f31230143af885aee73f907c2cf0d167a8c71103efb763909b7fb2f1f88b08f7 md5=73842963dfa22548a571c5ccca757bc9 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/frama-c-e-acsl/frama-c-e-acsl.0.5/opam |
No package is dependent
