alt-ergo
alt-ergo copied to clipboard
New test scripts
This PR consists in replacing the old bash scripts used for running the non-regression tests by a mighty Ocaml script.
I moved most of the tests from /non-regression
directory to /tests
. I didn't remove completely the former directory because
I don't know if we should keep some of its tests. For instance, I guess keeping the tests about parsing will not make sense as soon as we have replace the former parser by the one provided by Dolmen.
The new workflow for running non-regression tests is as follow:
- (optional) add extra tests in the directory
tests
and runmake gentest
to regenerate the dune files. - Run
make runtest
to perform tests. - If some tests fail, check if the new output is wrong. You can promote a new expected output by running
make promote
.
I added CI support. Run make runtest-ci
to perform tests for CI.
Any suggestion is very welcome :D
Suggestion (Inspired by what is done in https://git.frama-c.com/pub/colibrics):
As it was done in the older version, tests can be kept in folders which separate them by their expected result (../theory/{sat|unsat|unknown}/*.{ae|smt2}
).
That way, you won't need expect files (which all contain the same stuff anyway), you just need to generate rules in those folders that will tell Alt-Ergo that it should respond with sat, unsat or unkown. It can be done through a command line option that tells AE to expect some result, and if it got a different result, it can print an error message. (You can probably also print the command that led to the error using Sys.argv
).
You can have an executable that will generate a dune file in each folder, the dune file will contain the rules of the tests for all the files in the folder (with the right expect, determined by the folder's name). So adding a new test will simply consist of adding a its file to the right folder.