frama-c-e-acsl

This package contains the Frama-C's E-ACSL plug-in.
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

Install
Published
28 Jul 2015
Sources
e-acsl-0.5.tar.gz
md5=73842963dfa22548a571c5ccca757bc9
Dependencies
frama-c-base
>= "11.0"
ocaml
>= "3.12" & != "4.02.0"
Reverse Dependencies