[http://frama-c.com/eacsl.html E-ACSL] is both a formal specification language and a [http://frama-c.com Frama-C] plugin for runtime assertion checking of C code.

[http://frama-c.com/eacsl.html E-ACSL] is both a formal specification language and a [http://frama-c.com Frama-C] plugin for runtime assertion checking of C code.

The [http://frama-c.com/download/e-acsl/e-acsl.pdf E-ACSL] specification language is an executable subset of the behavioral specification language for C programs called [http://frama-

The [http://frama-c.com/download/e-acsl/e-acsl.pdf E-ACSL] specification language is an executable subset of the behavioral specification language for C programs called [http://frama-c.com/acsl.html ACSL].  E-ACSL supports function contracts, assertions, user-defined predicates and built-in predicates.

c.com/acsl.html ACSL].  E-ACSL supports function contracts, assertions, user-defined predicates and built-in predicates (like '''\valid(p)''' indicating that reading from or writing to a memory location pointed to by a pointer '''p''' is safe).

The E-ACSL Frama-C plugin [http://frama-c.com/download/e-acsl/e-acsl-0.6.tar.gz E-ACSL Frama-C plugin] automatically converts a given C program (say '''P''') containing E-ACSL annotations into a program '''P'''' instrumented with assertions that verify E-ACSL properties at runtime.

The E-ACSL Frama-C plugin [http://frama-c.com/download/e-acsl/e-acsl-0.6.tar.gz E-ACSL Frama-C plugin] automatically converts a given C program (say '''P''') containing E-ACSL annotations into a program '''P'''' instrumented with assertions that verify E-ACSL properties at runtime.

Further information about E-ACSL can be found [http://frama-c.com/eacsl.html here].

Further information about E-ACSL can be found [http://frama-c.com/eacsl.html here].