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] A variation domain failed to be computed
- Subject: [Frama-c-discuss] A variation domain failed to be computed
- From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
- Date: Wed, 6 May 2009 19:41:22 +0200
- References: <1241624519.21376.229.camel@supelec>
I answered your question in another message, but I should point out that all your problems should go away if your provide an implementation, however simple (you can write it with Frama_C_interval() and other modelization primitives) for the function getpwnam(). We do not want to assume that an unknown pointer-returning function such as getpwnam() always returns the same pointer because that would be too strong an hypothesis to make, but as long as you are calling it only once, you can make it return a fixed address, which will make work easier for the analyzer. Pascal
- References:
- [Frama-c-discuss] A variation domain failed to be computed
- From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
- [Frama-c-discuss] A variation domain failed to be computed
- Prev by Date: [Frama-c-discuss] A variation domain failed to be computed
- Next by Date: [Frama-c-discuss] Logical annotations
- Previous by thread: [Frama-c-discuss] Supported features, Global invariants, and POs
- Next by thread: [Frama-c-discuss] A few (newbye) questions...
- Index(es):