Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Subject: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: virgile.prevosto at cea.fr (Virgile Prevosto)
- Date: Tue, 3 Mar 2009 09:28:41 +0100
- In-reply-to: <3d13dcfc0903020827x7f097cfen65198f80f920db48@mail.gmail.com>
- References: <3d13dcfc0903020703h71d0de3au20312f6464a6116e@mail.gmail.com> <49AC04BC.20303@inria.fr> <3d13dcfc0903020827x7f097cfen65198f80f920db48@mail.gmail.com>
Hello, Le lun 02 mar 2009 17:27:47 CET, David MENTRE <dmentre at linux-france.org> a ?crit : > > >> First of all, what does exactly mean "No code for function xxxxxx, > >> default assigns generated"? > > > > You can look at ACSL manual, section 2.3.5. The point is that since a > > function like read() has no code given, nor contract, then it could be > > possible that it modifies every location in the heap. So it should be > > given a contract. > > Thank you for the precise reference to ACSL manual. I'll look at it. > Maybe this should be given in the error message? > To be completely clear, the warning says that Frama-C's kernel is generating an assigns clause based on the function prototype, because supposing that every location in the heap might be changed by a function call would prevent the analyses saying something useful. The issue is that this generated clause is not guaranteed to be correct. For instance, given the prototype void f(int* x,int l), there's no way to know if x is a pointer to a single int (which could be assigned l for instance), or to a block of several ints (whose length could be l for instance). It is thus important to review the generated clauses (e.g. with the -print option. They are also visible in the GUI), or better to give an appropriate contract to each prototype which has no associated definition. -- E tutto per oggi, a la prossima volta. Virgile
- Follow-Ups:
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- References:
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Prev by Date: [Frama-c-discuss] Issue with non terminating function
- Next by Date: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Previous by thread: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Next by thread: [Frama-c-discuss] Best approach when specifying regular C functions from stdlib?
- Index(es):