alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard

New test scripts

Open Halbaroth opened this issue 1 year ago • 1 comments

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:

  1. (optional) add extra tests in the directory tests and run make gentest to regenerate the dune files.
  2. Run make runtest to perform tests.
  3. 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

Halbaroth avatar Sep 21 '22 09:09 Halbaroth

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.

hra687261 avatar Oct 12 '22 09:10 hra687261