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] Need help on C-code slicing

  • Subject: [Frama-c-discuss] Need help on C-code slicing
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 14 Jun 2011 16:49:31 +0200
  • In-reply-to: <BANLkTinfq4jDchFdOVDy49UsOBXtfL=8Ng@mail.gmail.com>
  • References: <BANLkTi=eKHMSg8Sdq88OwqqO890tjdg+Cw@mail.gmail.com> <BANLkTikG=kiiqsZCCZvic1FW=Vc2cn2J6w@mail.gmail.com> <BANLkTinFUUT9m_9ek2nd7V7_-T-OY9UTjQ@mail.gmail.com> <BANLkTi=NVuC01B4Cm88qxpATpUqTC2JQqQ@mail.gmail.com> <BANLkTinfq4jDchFdOVDy49UsOBXtfL=8Ng@mail.gmail.com>
> I've made some progress: I solved my "degeneration" issue by #ifdef'ing out
> a few lines. Anyhow, they were of interest to me. The value analysis seems
> now to reach the end without trouble.

I would be interested in the lines that cause the completely unknown
value {‌{ ANYTHING}‌}.

> However, for some reason I have not fully discovered yet, some of the code
> I'm interested in is marked as dead by the value analysis (strike through
> and red background in the GUI).

You are right, this color code is for lines that seems unreachable to
the value analysis.

>? By simplifying some of the original code,
> I've made some progress to provide conditions which somehow prevent frama-c
> to believe code is dead. But I can't succeed circumventing my current
> problem, where a function is tagged as "NON TERMINATING FUNCTION". As far as
> I can understand, Frama-C seems to stop right after. (Naive?) usage of
> Frama_C_dump_each (with -slevel 1000) has not yet sched any light...

The four reasons you may get unreachable code that surprises you:

- the code is actually unreachable with the initial conditions that you
specified, and the solution is to make the analysis more general, with
such primitives as Frama_C_interval(min,max) that models an unknown
value between min and max;

- a bug in the analyzer;

- an infinite loop in the analyzed program;

- an alarm is emitted to warn about dangerous conditions that should not
happen. After suppressing the values for which the dangerous condition
happens, there is nothing left to propagate. An example is "x = 100 / 0;",
which the value analysis will say does not terminate.
You can recognize this case by the word "assert" in
the log produced by the batch version. Also, the way the GUI colors
the innermost non-terminating function may provide a clue.

In the worst case, the value analysis and you disagree about what
is dangerous. For instance, by default, the value analysis treats
x = &a < &b; as dangerous, same as the division by 0.
The value analysis has the standard on its side
(this is undefined behavior) but you may wish it propagated {0; 1}
instead of stopping. In the last version, there is an option for doing so.

Pascal