Clever Geek Handbook

Frama-c metrics are output to a file for tagging by function

I am trying to output metrics results to a file. I know I can call -metrics-output

and output the analysis of the global metrics to a file, but I am also trying to get the results of each function.

Vocation:

frama-c -metrics -metrics-output test.txt -metrics-by-function example.c

or

frama-c -metrics -metrics-by-function -metrics-output test.txt example.c

It just outputs a file with global metrics.

+3


source to share


1 answer


I have looked at the plugin code and it seems that the output for each function is only available to the console and .html

only to .txt

. So you can

  • discard completely -metrics-output test.txt

    and pipe the Frama-C output to a file. You get a different subsection for each function

  • use -metrics-output test.html

    . Function information is available as html array.



As an aside, the order of the options doesn't matter in Frama-C. The operator -then

can be used for sequencing if needed. Hence your two commands are equivalent.

+3


source






More articles:


All Articles