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
- Subject: [Frama-c-discuss] [wp] invoke provers from command line
- From: dmentre at linux-france.org (David MENTRE)
- Date: Mon, 09 Dec 2013 09:00:12 +0100
- In-reply-to: <BAY169-W107B5408EA227609E7A68097D30@phx.gbl>
- References: <BAY169-W107B5408EA227609E7A68097D30@phx.gbl>
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
- References:
- [Frama-c-discuss] [wp] invoke provers from command line
- From: x_cui at hotmail.com (Xiao-lei Cui)
- [Frama-c-discuss] [wp] invoke provers from command line
- Prev by Date: [Frama-c-discuss] [wp] type conversion check is less strict than Jessie?
- Next by Date: [Frama-c-discuss] JFLA14 - Dernier appel à participation
- Previous by thread: [Frama-c-discuss] [wp] invoke provers from command line
- Next by thread: [Frama-c-discuss] [wp] type conversion check is less strict than Jessie?
- Index(es):