Most of our tests are expect tests regarding the generated code.
The github workflow includes the dune build @launchtests call that actually run the generated code. This expects the test to be successful.
There is nothing checking the behaviour of the generated code that report an error in the tested module.
248 was indeed spotted relatively late after the introduction of the concerned feature (and the bug) due to the lack of such tests.
We want to test:
the generated code spots the bugs (we are relatively confident about that one)
the display of the explanation of the bug: the Gospel term that is violated
the display of the runnable scenario (the commands, the returned and the expected values)
We should have some expect tests in which generated code for some buggy modules (examples of different failures) is run.
/!\ in order to have a reproducible output, we should run the generated code with a given seed.
Most of our tests are expect tests regarding the generated code. The
githubworkflow includes thedune build @launchtestscall that actually run the generated code. This expects the test to be successful.There is nothing checking the behaviour of the generated code that report an error in the tested module.
248 was indeed spotted relatively late after the introduction of the concerned feature (and the bug) due to the lack of such tests.
We want to test:
We should have some expect tests in which generated code for some buggy modules (examples of different failures) is run.
/!\ in order to have a reproducible output, we should run the generated code with a given seed.