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] Dead code that shouldn't be

  • Subject: [Frama-c-discuss] Dead code that shouldn't be
  • From: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Mon, 04 May 2009 12:24:01 +0200
  • In-reply-to: <5AC5D91A-C2E4-48B7-AA25-BBDF33045ACA@cea.fr>
  • References: <1237389365.3508.130.camel@supelec> <5AC5D91A-C2E4-48B7-AA25-BBDF33045ACA@cea.fr>
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.