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