--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] A variation domain failed to be computed



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