frama-c にはCFG機能は未実装

[Frama-c-discuss] frama graph plugins

[Frama-c-discuss] frama graph plugins
Julien Signoles Julien.Signoles at cea.fr
Fri May 28 10:18:43 CEST 2010

Previous message: [Frama-c-discuss] frama graph plugins
Next message: [Frama-c-discuss] Non-terminating loops
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

Hello,

Here is just a complement to/synthesis of Pascal's answer.

Davidson Boccardo a écrit :
> Probably I did not express my goal in the right way.
>
> I would like to know if exists some way to interact with the graphs
> provided by Frama, such as
> computing cyclomatic comprexity, function connectitivy.

  • Plug-in "metrics" provides some useful information, but it does not

interact directly with the callgraph (neither the syntactic or the
semantic one).

  • You can interact yourself with the syntactic/semantic callgraph by

writing a plug-in. If some useful functions are missing in the API of
these plug-ins, please fill a "feature request" on the BTS.

> Moreover, Frama provides control flow graph for each function?

  • The control flow graph (cfg) is computed by Frama-C. It is not yet

provided to the user. Though you can interact with it by writing a plug-in.

  • The cfg could be displayed in the GUI in a future version of Frama-C.

Hope this helps,
Julien