---
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
- Subject: [Frama-c-discuss] NON TERMINATING FUNCTION when adding specification
- From: anne.pacalet at free.fr (Anne Pacalet)
- Date: Fri, 16 Nov 2012 13:37:34 +0100
- In-reply-to: <CABbVA-CF=nYi8AiOBUkFPL2Axkgbzv042vd0zz_5FJW1E6izdw@mail.gmail.com>
- References: <50A61AB6.90503@free.fr> <CABbVA-Df7sUHzZ2Bs-gsFKdG1MCmzgfU9NF=YzDDO2dvKwEaTA@mail.gmail.com> <50A624B8.2030609@free.fr> <CABbVA-CF=nYi8AiOBUkFPL2Axkgbzv042vd0zz_5FJW1E6izdw@mail.gmail.com>
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.