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

[Frama-c-discuss] how jessie and why platform work to generate a .v output?



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>