Frama-C-discuss mailing list archives

x_cui at hotmail.com (Xiao-lei Cui) · Wed, 6 Nov 2013 01:29:50 -0500

Following the why3 manual, as I run :
cuix at berkhoff:~/projects/frama-c/max/max.jessie$  why3 -P alt-ergo max.mlw 
File "max.mlw", line 7, characters 0-46:
Theory not found: jessie3theories.Jessie_memory_model

I also tried some simple input files and example shipped with source, the attached .why and .mlw seems working.

What I did is I upgraded frama-c-carbon/why2.29 to frama-c-fluorine/why3(0.81), re-installed why2(but this time it is why2.33 to be compatible with frama-c-fluorine). 

Thanks!!

Xiaolei
From: x_cui at hotmail.com
To: frama-c-discuss at lists.gforge.inria.fr
Date: Tue, 5 Nov 2013 21:38:28 -0500
Subject: Re: [Frama-c-discuss] how jessie and why platform work to generate a .v output?

Hello, 
  I re-configured why2 and installed it. frama-c now can recognize jessie plugin, however, as I tried a previous demo, why3IDE complains :
   "Error while reading file '../max.mlw': File "max/../max.mlw", line 487, characters 9-36: this expression raises unlisted exception Return_label_exc"
   No proof obligations are shown in the IDE. The demo max.c works fine with frama-c-carbon/why2 though:)
   Thanks again.    

 $ frama-c -jessie -pp-annot max.c
[kernel] preprocessing with "gcc -C -E -I.  -dD max.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir max.jessie
[jessie] File max.jessie/max.jc written.
[jessie] File max.jessie/max.cloc written.
[jessie] Calling Jessie tool in subdir max.jessie
Generating Why function max
Generating Why function main
[jessie] Calling VCs generator.
why3ide --extra-config /usr/local/lib/why/why3/why3.conf max.mlw
[Info] Init the GTK interface... done.
[Info] reading icons... done.
[Info] Creating tree model... done
[Info] found regular file 'max.mlw'
[Info] using 'max' as directory for the project
[Info] Opening session...

[Info] Opening session: update done

[Info] Opening session: done
Adding file '../max.mlw'
[Info] adding file ../max.mlw in database
[Info] saving IDE config file

> Date: Tue, 5 Nov 2013 15:47:36 +0100
> From: Claude.Marche at inria.fr
> 
> 
> You should install Why2 after Why3. So in your case, reconfigure why2
> (check that frama-c support will be compiled), compile and install it.
> 
> - Claude
> 
> Le 05/11/2013 15:10, Xiao-lei Cui a ?crit :
> > hello, thanks for tip!!
> > I now upgraded  frama-c from frama-c-carbon to
> > frama-c-Fluorine-20130401. And installed why3(0.81). However, as I try
> > out frama-c:
> > $ frama-c -jessie file.c
> > 
> > It complains "option -jessie is unknown".
> > Running
> >  $ frama-c -help
> > the -jessie option is not shown.
> > 
> > Any ideas? :)
> > 
> > xiaolei
> >  
> > 
> > 
> > 
> >> Date: Tue, 5 Nov 2013 14:31:35 +0100
> >> From: Claude.Marche at inria.fr
> >> To: frama-c-discuss at lists.gforge.inria.fr
> >> Subject: Re: [Frama-c-discuss] how jessie and why platform work to
> > generate a .v output?
> >>
> >>
> >> Hi,
> >>
> >> Le 02/11/2013 05:45, Xiao-lei Cui a ?crit :
> >> > Hi all,
> >> > I am trying to figure out the workflow from C source(plus
> >> > embeddedACSL spec) to the .v file passed to proof assistant.
> >> > I am using why2. Is the following workflow correct?
> >> > C/ACSL -> (frama-c/jessie)
> >> > -->filename.jc ->(jessie/why)
> >> > -->filename.why->(why)
> >>
> >> more or less
> >>
> >> > from
> >> >> frama-c -jessie -pp-annot max.c
> >> > I got max.why, which is over 300lines of code.
> >> > I then use why command to generate .v output for coq:
> >> >> why --coq max.why
> >> > File "max.why", line 17, characters 29-35:
> >> > Unbound type 'tag_id'
> >> >
> >> > Did I miss something or some step?
> >> > Thanks in advance.
> >>
> >> the "why" command should be giving an additional prelude file as input.
> >> Indeed you should not call why directly but use
> >>
> >> make -f max.makefile coq
> >>
> >> Anyway, the support of Coq in Why2 is known to be painful for the user.
> >> Using Coq to discharge VCs using Why3 is much much easier to do, so I
> >> strongly recommend to use Why3 instead.
> >>
> >> - Claude
> >>
> >>
> >>
> >>
> >>
> >> --
> >> Claude March? | tel: +33 1 72 92 59 69
> >> INRIA Saclay - ?le-de-France |
> >> Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/
> >> F-91405 ORSAY Cedex |
> >>
> >>
> >> _______________________________________________
> >> Frama-c-discuss mailing list
> >> Frama-c-discuss at lists.gforge.inria.fr
> >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> > 
> > 
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> > 
> 
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           |
> Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
> F-91405 ORSAY Cedex                    |
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/6f377d4e/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: binary_search.mlw
Type: application/octet-stream
Size: 3515 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/6f377d4e/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: demo1.why
Type: application/octet-stream
Size: 162 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/6f377d4e/attachment-0001.obj>