--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on September 2010 ---
> 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