Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [wp] invoke provers from command line

Hello,

Le 09/12/2013 06:22, Xiao-lei Cui a ?crit :
> [wp] Goal typed_max_post : trivial
> [wp] Goal typed_max_post_2 : trivial
> [wp] Goal typed_max_assert : trivial
> ------------------------------------------------------------------------------
> why3IDE did not show up.

My guess is that the VP are so easy that WP does not feed them to Why3. 
I'll let expert confirm this.

Try set-up an unprovable VC (e.g. "assert zz < 0;").

Best regards,
david