You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
Most of our tests are expect tests regarding the generated code.
The
github
workflow includes thedune 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:
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.
The text was updated successfully, but these errors were encountered: