ExprKind::NeverToAny => Term::Absurd => Invalid Why3

[dewert99]

When running CI for the Prusti translation I noticed that absurd seem to no longer be valid Why3, but it still can get generated from the THIR never to any expression eg.

#[ensures(match x {Some(x) => x, None => true})]
//                            ^ x is implicitly cast from ! to bool, which generates ExprKind::NeverToAny
fn test(x: Option<!>) {}

[xldenis]

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

[dewert99]

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.

[xldenis]

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...

[jhjourdan]

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.

[xldenis]

Yea that's better than false but the point is: it's fixable