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

[Frama-c-discuss] termination



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                    |