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

[Frama-c-discuss] Dead code that shouldn't be



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.