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: pascal.cuoq at cea.fr (Pascal Cuoq)
  • Date: Wed, 18 Mar 2009 16:35:48 +0100
  • In-reply-to: <1237389365.3508.130.camel@supelec>
  • References: <1237389365.3508.130.camel@supelec>
On Mar 18, 2009, at 4:16 PM, Jonathan-Christofer Demay wrote:

> Hi,
>
> I'm back with this problem.
>
> I managed to patch nullhttpd so that I could perform the analysis I
> wanted to.
>
> Now, I want to use frama-c to analyse something way bigger than
> nullhttpd, so I was wondering if it would be possible (and if it was  
> any
> relevant) to tell frama-c to ignore those probable run-time errors and
> continue the analysis ?

Yes. In fact, this is already what it does.

This is covered in FAQ No 2 and 3 in the manual, excerpted below.

What may be happening to you is that the analyzer is emitting
alarms for a program behavior that is in fact wanted and that you
do not consider dangerous. One example is the analysis of the
function memmove. This function handles overlapping buffers with
a pointer comparison that the value analysis considers
dangerous because the result of this comparison is arguably
unspecified when the two buffers are not in the same base address.
This is the general idea, although not the situation that you are
encountering is not this particular one, because currently the
analyzer does not cut off any execution
paths for this situation (but it could if it wanted to).

Another example is if a function in the analyzed code takes
a partially initialized struct as argument. You could argue that
as long as it does not read it, this is safe, but currently, an
alarm is emitted stating that the struct should be initialized.
We would, in fact, agree with your argument. We only
discovered this aspect recently. Consider it as a kind of
known bug.

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.

Pascal
____________

\question{Alarms that occur after a true alarm in the analyzed code
   are not detected. Is that normal? May I give some information to the
   tool so that it detects those alarms?
}

The answers to these questions are ``yes'' and ``yes''.
[...]
It is unreasonable to expect Frama-C to
perform a choice over what may happen after dereferencing
\lstinline|NULL|. It is possible to give some new information to the  
tool
so that analysis can continue after a true alarm. This technique is  
called
debugging. Once the issue has been corrected in the source code under
analysis ---~more precisely, once the user has convinced emself
that there is no problem at this point in the source code~--- it
becomes possible to trust the alarms that occur after the given point,
or the absence thereof (see next question).

\question{Can I trust the alarms (or the absence of alarms) that occur
   after a false alarm in the analyzed code? May I give some
   information to the tool so that it detects these alarms?}

The answers to these questions are respectively ``yes'' and
``there is nothing special to do''. If an alarm might be spurious, the
value analysis automatically goes on. If the alarm is really a
false alarm, the result given in the rest of the analysis can be
considered with the same level of trust than if Frama-C had not
displayed the false alarm. One should however keep in mind
that this applies only in
the case of a false alarm. Deciding whether the first alarm is a true
or a false one is the responsibility of the user.