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] 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