--- layout: fc_discuss_archives title: Message 37 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,

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                    |