--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2013 ---
Ah, I will remember to not ignore the stdout! Thanks, Steve On Apr 15, 2013, at 1:21 AM, Claude March? <Claude.Marche at inria.fr> wrote: > > This is not easy to see, but when running jessie you get > > [jessie] warning: Termination condition(s) ignored > > which means that the clause "terminates is not handled by jessie. Replace it by a requires clause and you will get what you expect. > > - Claude > > > Le 15/04/2013 08:29, Stephen Siegel a ?crit : >> /*@ >> @ terminates c>0; >> @ assigns \nothing; >> @*/ >> void f (int c) { >> /*@ >> @ loop assigns \nothing; >> @*/ >> while(!c) { >> } >> return; >> } > > -- > 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