--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on November 2013 ---
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>