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] adding new provers to why3
- Subject: [Frama-c-discuss] adding new provers to why3
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Tue, 12 Nov 2013 01:24:21 +0100
- In-reply-to: <BAY169-W116EB430C1A2883AB4376F197F20@phx.gbl>
- References: <BAY169-W100232DF1943ABFB9A9A5BF97F20@phx.gbl> <BAY169-W116EB430C1A2883AB4376F197F20@phx.gbl>
On 11/08/2013 08:11 AM, Xiao-lei Cui wrote: > Another question arises when I use why3 is that there seems no source > code(ACSL and C) tracing from given proof obligations. You should see the positions of the PO in the lower right part of Why3ide window. If you don't, then there is a problem: look at the standard error if there are some problems reported.
- References:
- [Frama-c-discuss] adding new provers to why3
- From: x_cui at hotmail.com (Xiao-lei Cui)
- [Frama-c-discuss] adding new provers to why3
- From: x_cui at hotmail.com (Xiao-lei Cui)
- [Frama-c-discuss] adding new provers to why3
- Prev by Date: [Frama-c-discuss] JessieIntegerModel question
- Next by Date: [Frama-c-discuss] adding new provers to why3
- Previous by thread: [Frama-c-discuss] adding new provers to why3
- Next by thread: [Frama-c-discuss] adding new provers to why3
- Index(es):