--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2009 ---
On Wed, 2009-03-18 at 16:35 +0100, Pascal Cuoq wrote: > There is no single switch to make the analyzer more lenient > on all those alarms that correspond to behaviors that are not > quite run-time errors. But if you tell us which one is > bothering you, we can make the emission of that particular > alarm optional. The problem I have is with code considered dead by the Value Analysis plugin, because of course in this code a state will be "NOT ACCESSIBLE". For example, when a variable is initialized by another function through a pointer, and the code of the function is not provided to frama-c because it is in a library, the Value Analysis plugin assumes a runtime error the next time the variable is read and from this point code is considered dead. This for example happens with data initialized by 'getaddrinfo' What I would like is preventing data considered uninitialized by frama-c to stop the value analysis because of a potential runtime error. Currently, I'm patching the code I'm analyzing so to fool frama-c to think a pointer is valid or an integer can have every possible value. But it is not very pratical on very large program, so maybe I was hoping it would be possible to force frama-c to have this behavior by default.