Skip to content
Snippets Groups Projects
Commit beffbc38 authored by Sebastian Graf's avatar Sebastian Graf
Browse files

PmCheck: Handle ⊥ and strict fields correctly (#18341)

In #18341, we discovered an incorrect digression from Lower Your Guards.
This MR changes what's necessary to support properly fixing #18341.

In particular, bottomness constraints are now properly tracked in the
oracle/inhabitation testing, as an additional field
`vi_bot :: Maybe Bool` in `VarInfo`. That in turn allows us to
model newtypes as advertised in the Appendix of LYG and fix #17725.

For some reason I couldn't follow, this also fixes #18273.

I also added a couple of regression tests that were missing. Most of
them were already fixed before.

In summary, this patch fixes #18341, #17725, #18273.

Metric Decrease:
    T12227
parent 766aa777
Branches wip/T18341
No related tags found
No related merge requests found
Showing
with 675 additions and 500 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment