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

[Frama-c-discuss] termination



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