Open dewert99 opened 6 months ago
absurd
was never valid in why's logic but we can provide an encoding for the purposes of verification in vcgen
, it should work the same way as the `let functions did before.
Something like absurd = assert(false); any
I don't think this has to do with vcgen
since the error is from a pre-condition I mentioned you in a comment on the Why3 line giving the error.
Hmmm, yea but that's still incorrect in why3; we should generate false
instead I think. Just need to thin through the consequences of that typing rule...
I don't think we should generated false
here. This does not generalizes to all types. We should really generate any
or something alike. If it's on a piece of code which is not handled by the VCGen (like here), then we won't check this is dead code, but at least we would generate an unpredictable value of the right type.
Yea that's better than false
but the point is: it's fixable
When running CI for the Prusti translation I noticed that
absurd
seem to no longer be validWhy3
, but it still can get generated from the THIR never to any expression eg.