--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on November 2013 ---
Hi Claude, Thanks for the tips! The work-around solves the problem. I will start playing with WHY3, and working on the ACSL specifications. cheers, xiaolei > Date: Thu, 7 Nov 2013 17:58:22 +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, > > In that case there is nothing wrong with your installation, but you hit > a subtile bug of Jessie in presence of an assert just before a return > statement. > > A simple, although strange I admit, work-around is to add an extra empty > statement ";" after the assert : > > > /*@ assert zz>0; @*/ ; > return y; > > - 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/44496be1/attachment.html>