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] Understanding slicing results

  • Subject: [Frama-c-discuss] Understanding slicing results
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Wed, 10 Feb 2010 16:17:16 +0100
Hello,

we acknowledge that Frama-C's documentation in general is not all that
it should be.

As Patrick said, the value analysis (one of the passes on the analyzed
code) is context- and flow-sensitive, but the results are recorded
only per statement and not by possible execution path. This may cause
some information that was available during the analysis to cease to
appear. Similarly, for functions, there is a single results table in
which all the results are merged, although the different calls to the
function are analyzed separately during the
analysis. This is necessary for various technical reasons (inquiring
about the possible values of an expression at a statement is simple,
but trying to express what execution path one is interested in would
be terribly complicated, and keeping the results separate would use up
too much memory on large programs).

There is a system of hooks for the plug-ins wishing to make use of all
the information available before it is erased. The -calldeps option
makes the dependencies analysis use these hooks. The dependency
analysis is another pass that comes after the value analysis, whose
results are used by the slicing plug-in, and which is documented in
the value analysis manual. When the -calldeps option is enabled, the
dependencies of a function are stored separately for each calling
statement, which is more precise than the usual way of one table per
function.

When trying to make sense of the slicing plug-in, it may help to look
at the Program Dependency Graph, the last analysis pass before the
slicing.

Saving your program as t.c, inserting /*@ slice pragma stmt; */ in the
right place and using the following commandline in Beryllium 20090902:

frama-c -lib-entry  -quiet t.c -calldeps -val -dot-pdg main -pdg

I get a dot representation of the PDG (snapshot attached). This does
not explain why line 24 is retained, though, because the PDG clearly
shows that it was recognized that main does two completely independent
things, represented on the left and one the right (technically, 3
independent things: two computations, and returning). This also means
that the limitation you encountered is probably a minor one that we
may be able to remove.

The only workaround that we can offer for the moment is to slice again
on the same criterion a second time:

frama-c -lib-entry -slice-pragma main -slice-print -quiet t.c
-calldeps -ocode t2.c
frama-c -lib-entry -slice-pragma main -slice-print -quiet t2.c -calldeps

This removes anything related to s2t_1.

We will look at the behavior you have reported.

Pascal
-------------- next part --------------
A non-text attachment was scrubbed...
Name: main_pdg.png
Type: image/png
Size: 65486 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100210/87fe9543/attachment-0001.png