--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] problems with plugin-integration



> And than I've got another question.
> I'm interested in the structure of the file metrics.ml
> how does it work?
> it isn't possible to watch the source code of metrics.ml which is used in
> Frama-C.

I am not sure what you mean by "it is not possible to". Surely the
fact that it is released as Open Source definitely makes it possible
to look at the implementation of the plug-in metrics? (in case you
have a hard time to find it, the files src/metrics/*.ml* in the source
distribution).

> But for my analysation, i need to know why the framework Frama-C change
> the C-code in another C-code and then verify the changed code?

In order to save plug-in authors some tedious repetitions, a few
transformations are made: all loops are transformed into while loops,
block-local variable are made function-local, ...

> I must verify the current C-code with all "switch, if, while, for, do
> while, ..." and let it print on the screen.

It depends what you mean by "verify", but if you mean check properties
about what the program does, then you won't care about the
transformation made by Frama-C's front-end CIL
(http://www.cs.berkeley.edu/~necula/cil/ ). These transformations do
not change the meaning of programs. Originally, these transformations
could remove some bugs because that was not an issue in the initial
intentions of CIL's authors, but Frama-C's modified version of CIL
allows all bugs in the original source code to be discovered, even
though the simplifications are still there to simplify plug-in
development.

On the other hand, if by "verify" you mean "do statistics about the
ratio of while loops to for loops", then you may need to work at the
level of the program representation before simplifications, or use
another parser altogether.

Pascal