Remove bug with integers in return values #240
Conversation
There was a problem hiding this comment.
Thank you for this PR!
This looks really good.
I rather have the changes in the tests in the same commit than the changes in the code that cause them. I know that this generate a lot of "noise" in the diff, but we can always give git a path to focus on the part we want to inspect. And that way, we have coherent commits.
I've given some thoughts on how to handle the pretty printing of Gospel.integers.
In your very detailed commit message (ddcdb3d)(thanks for that :-)) you describe two ways:
- Add integer pretty-printers to STM
- Automatically cast integers back to ints when needed
The problem I see with the second option is that integer_of_int can raise an exception that is not caught in the generated code. Even, if we catch it, we are loosing some information when the integer is larger than an int (not sure it will happen that often though).
Gospel.integerss are implemented as Z.t, I think it would be worth it to ask the STM devs whether it could be intersting to add Z.t support. If not, there is also the solution to add them in the generated code (in the Ty module). We can add them by default: there is a rather high probability that the tested module contains some functions returning an int (casted by Gospel as an integer). In the case there is not, the cost is not prohibitive.
nikolaushuber
force-pushed
the
incomplete-comp-warning
branch
from
9779376 to
e7917f6
Compare
Extends STM.ty with a type for Gospel.integer and includes a smart constructor to create a value of type ty_show. Since Gospel.integer is not used in every test we also ignore warning 32 for the unused smart constructor.
nikolaushuber
force-pushed
the
incomplete-comp-warning
branch
from
5085007 to
ed59012
Compare
Co-authored-by: Nicolas Osborne <nicolas.osborne@tarides.com>
nikolaushuber
force-pushed
the
incomplete-comp-warning
branch
from
ed59012 to
76b56ac
Compare
|
Thanks! |
This PR removes a bug/shortcoming within the qcheck-stm plugin when testing functions that return integers.
Gospel has two different types for integers (int & integer), but only int has a pretty-printer defined in STM.
Gospel also automatically adds casting operations for ints to integers where needed.
The code added in this PR dynamically detects where these casts have been added and automatically adds reverse-castings for error pretty-printers where needed.
This responds to #238.