Why3 error: unexpected 'variant' clause

[sarsko]

When figuring out the proof, it is sometimes useful to add #[trusted] temporarily. If that function has a #[variant] attached, Why3 will give the following error: unexpected 'variant' clause

Example:

#[trusted]
#[variant(0)]
fn ex() {
}

[xldenis]

Ah yes, i understand why this happens but we should just silently swallow the variant instead.

[jhjourdan]

Could we emit a warning instead? I understand that you may want to do this, but having a variant clause on a trusted function is not something that one would do in a final piece of code.

[xldenis]

Could we emit a warning instead? I understand that you may want to do this, but having a variant clause on a trusted function is not something that one would do in a final piece of code.

Yes definitely.