--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Queries regarding WP plugin



Le 15/12/2014 10:04, Lo?c Correnson a ?crit :
> Indeed, for simple PO discharged by Qed, there is actually no other proof obligation but ? goal PO : true ? !
> You can try to deactivate the advanced simplifications of WP with `-wp-no-let` and other options of the same group, but most very low-level simplifications such as ? 1+2 ? into ? 3 ? or ? a+0 = a ? are always applied and can not be deactivated.

OK, thanks.

Best regards,
david