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] interfacing non-OCaml programs with Frama-C

  • Subject: [Frama-c-discuss] interfacing non-OCaml programs with Frama-C
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Tue, 9 Dec 2008 21:33:07 +0100
  • References: <5EFD4D7AC6265F4D9D3A849CEA9219191AB11D@LAXA.intra.cea.fr><bacfeaa40811280930r1b6f0e46xad400ebefbdf4646@mail.gmail.com><5EFD4D7AC6265F4D9D3A849CEA9219191AB120@LAXA.intra.cea.fr> <bacfeaa40812090805p4b41416avf253d905a3ec0d@mail.gmail.com>
>> There is also an option that you may or may not have noticed
>> for dependencies. It is called  -deps and it gives dependencies
>> with respect to the initial values of the variables at the beginning
>> of the function.

>I may be wrong be it seems -deps only gives direct dependencies, it doesn't
>give indirect ones. (At least through the GUI, I still haven't tried to
>directly interact as a plugin)

What you see in the GUI are (roughly) the results of another computation,
called PDG (for program dependency graph).
The PDG is a sophisticated graph between statements (as nodes)
with different kinds of edges (three different kinds, I think, for
data, control and syntactic dependencies, but it may have evolved or I
may misremember altogether).

The dependencies as computed by the option -deps are more synthetic.
They are expressed at the end of the function, the transitive
dependencies are included, and control dependencies are
included as well.

Both exist, use the same basic building blocks, and are displayed
differently because of their different natures. The PDG is the fabric
that the right tailor can turn into either a sober jacket or extravagant
haute couture. Dependencies are a pair of Levi's jeans.

Parts at a time of the PDG are presented interactively
in the GUI because it wouldn't possible to comprehend it if it was 
emitted in the logs anyway. The dependencies are displayed in the logs
of the batch version of Frama-C, and are not presented in the GUI because
we didn't have time to do it yet and because they wouldn't benefit as much
from it than the PDG does.

Pascal