--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] NON TERMINATING FUNCTION when adding specification




Le 16/11/2012 12:39, Boris Yakobowski wrote :
> Using specifications with the standard
> library is quite tricky, as we routinely notice ourselves.

YES : I got it !

Advice for everyone : never forget the property :
   @ assigns \result \from .... ;
in your specifications !

Bye,
-- 
Anne.