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