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] [Why-discuss] make ... coq-goals question

  • Subject: [Frama-c-discuss] [Why-discuss] make ... coq-goals question
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 06 Jan 2009 09:41:48 +0100
  • In-reply-to: <4625952C-F7FD-4CBB-BB88-8BED2E72BCE1@di.uminho.pt>
  • References: <4625952C-F7FD-4CBB-BB88-8BED2E72BCE1@di.uminho.pt>

Jorge Sousa Pinto wrote:
> Hi,
> 
> In the context of using gwhy for discharging POs with an automatic  
> prover and then using Coq for the remaining goals, it is useful to  
> have a distinct .v file for each PO.
> 
> In the latest release of Why the commands
> 
> make -f xxx.makefile project
> make -f xxx.makefile coq-goals
> 
> seem to do this.
> 
> (by the way there seems to be a small bug here, one has to add  
> "Require Export WhyReal" manually at the beginning of the file  
> xxx_ctx_why.v in order for the second make to work properly).
> 
> My questions are:
> 
> 1) Is this the right way to do it?

Almost right: indeed doing just one of them just suffice. the 'project' 
target is intended to replace the 'coq-goals' target in the future. the 
'project' target also produce an XML database file to be used by the 
Eclipse plugin

> 2) Since there is a Coq button in gwhy that I can't seem to get to  
> work, what is the intended functionality of that button?

It is an highly experimental support for Coq which indeed does not work 
yet. It should have been hidden for the release, to avoid 
misunderstanding...

You can give a try to the Eclipse plugin, which offer similar 
functionalities as the GWhy interface, but where the Coq support is 
operational there.


> 3) [Frama-c question] is there a way to produce the same effect as the  
> two make commands above, directly from a frama-c invocation?

something like

frama-c -jessie-analysis xxx.c
cd xxx.jessie
make -f xxx.makefile project

should work.


> 
> Thank you in advance!
> Jorge
> 
> 
> _______________________________________________
> Why-discuss mailing list
> Why-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why-discuss

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |