Skip to content
Snippets Groups Projects
  • Kostyantyn Vorobyov's avatar
    bddca667
    Merge branch 'feature/julien/simplify-tests' into 'master' · bddca667
    Kostyantyn Vorobyov authored and François Bobot's avatar François Bobot committed
    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
    bddca667
    History
    Merge branch 'feature/julien/simplify-tests' into 'master'
    Kostyantyn Vorobyov authored and François Bobot's avatar François Bobot committed
    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