--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Compatibility issue (frama-c-fluorine and why3-0.81)



Hi all,
   I have come across this compatibility issue, as I upgrade from frama-c-carbon/why2.29 to fluorine/why3-0.81. To make the jessie plug-in work, I installed why2.33 after fluorine/why3.
   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 why3IDE. The demo max.c works fine with frama-c-carbon/why2 though:). 
   I am stuck here. Any suggestions?  Thanks a lot.    

 $ 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

xiaolei
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/a5f7535d/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: max.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/a5f7535d/attachment-0001.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max.mlw
Type: application/octet-stream
Size: 20494 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131106/a5f7535d/attachment-0001.obj>