--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on May 2009 ---
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