Kostyantyn Vorobyov authored 9 years ago and Julien Signoles committed 9 years ago

containing the segment-based memory model.

[tests] fix oracle wrt new pretty-printing of labeled predicates

Compatibility with frama-c/frama-c!638.

See merge request !32

Kostyantyn Vorobyov authored 9 years ago and François Bobot committed 9 years ago

non-regression test simplification

This MR addresses issue #4 by simplifying the E-ACSL non-regression tests. Non-regression tests are now about 3x faster than before

* it improves a bit ```testrun.sh```
* it splits the e-acsl-runtime tests in 2 directories:
- ```e-acsl-runtime```: these tests do not test -e-acsl-gmp-only
- ```gmp```: these tests do test -e-acsl-gmp-only and the normal behavior (was the nominal situation)
* ```testrun.sh``` is used for runtime verification.
* ```tests/print.ml``` is used to filter the output in order than the generated file used by diff does not depend on libc anymore
* directory ```bts``` behaves like the new directory ```e-acsl-runtime```` (no gmp).

See merge request !27

update headers

update headers to 2016 and address issue #3 

See merge request !28

Documentation for the E-ACSL wrapper script

Merge request addressing issue #6 

- Fixed a minor bug in the `e-acsl-gcc.sh` script.
- Added a section on the use of the E-ACSL wrapper script to the E-ACSL user manual. I placed the section at the very end of the manual, this is such that one first explores the available options and then learns how to make simplified runs. I think that the section on the wrapper script can also be placed at the very beginning (e.g., simple use with `e-acsl-gcc.sh` first and the advanced use via custom `frama-c`/`gcc` commands later). Please advise if the latter one is preferred. 
- Added an entry to the Changelog regarding the above change.
- Fixed test failures due to changes in the output of `frama-c`.

See merge request !26

section of the user manual

Minor spelling/stylistic changes (see merge request #26)

as it belongs to doc/userman/changes.tex

wrapper script

e-acsl-gcc.sh

to a Frama-C run

section of the user manual

Minor spelling/stylistic changes (see merge request #26)

as it belongs to doc/userman/changes.tex

wrapper script