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

Install

frama-c.com Edit opam file

Authors

  1. J
    Julien Signoles
  2. G
    Guillaume Petiot

Maintainers

  1. J
    julien.signoles@cea.fr

Sources

e-acsl-0.5.tar.gz
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

Tags

program verification formal specification runtime assertion checking monitoring C plugins ACSL E-ACSL

Published: 28 Jul 2015

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