ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
36 stars 10 forks source link

Remove bug with integers in return values #240

Closed nikolaushuber closed 1 month ago

nikolaushuber commented 2 months ago

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.

n-osborne commented 1 month ago

Thanks!