Closed Lucccyo closed 1 month ago
Thanks for raising this issue :-)
Indeed we haven't tackle the question of the cleanup function asked for the STM.Spec
module. For now, we are generating a dummy one as it is the most used when testing data structures.
This fall under the user-provided information, as we can't guess the body of the cleanup function.
So I would suggest to do something similar to the init_state
function, but with an optional argument (as most of the time, the user will want the dummy function).
In this case, the user can add the cleanup
function in the configuration module. If present, the generated code will use it, if absent ortac will generate the dummy one.
We use Ortac to test the implementation of
Mirage_kv
, a key-value store existing on a disk. To establish a connection to this disk, we utilise the interface ofMirage_block
. If we highthen the number of QCheck tests, an excessive number of operations are sent to the disk, leading to blockages. We would like Ortac to generate a cleanup function incorporating our cleanup function,Mirage_block.disconnect
. This will allow the disk to take a breath and enable us to continue testing with a fresh disk.