Skip to content
Snippets Groups Projects
Commit bddca667 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by François Bobot
Browse files

Merge branch 'feature/julien/simplify-tests' into 'master'

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
parents 477183a9 b7861837
No related branches found
No related tags found
Loading
Showing
with 46 additions and 151 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment