CODEWITHSUNDEEP
frama-c
user3675417
user3675417

Reputation: 13

Value analysis module and extensions options

I have some questions on options of value analysis module and some extensions options.

I use the command : frama-c-gui -val -slevel 100 -plevel 300 -absolute-valid-range 0x00000000-0xffffffff -metrics -metrics-value-cover -scope-def-interproc -main MYMAIN CODE/*.c

So I need to verify all of 62 warning or just 32 got by this options ?

Upvotes: 1

Views: 142

Answers (2)

byako
byako

Reputation: 3422

What is "Coverage estimation = 100.0%" with -metrics-value-cover I get a value between 80 and 100%, at the beginning I thought get <100% when I had dead code, but I had dead code when I get 100%, so I think get 100% if all functions in sources files are analysed ?

Let's take an example.

[metrics] Value coverage statistics
      =========================
      Syntactically reachable functions = 3 (out of 3)
      Semantically reached functions = 1
      Coverage estimation = 33.3% 

      Unseen functions (2) =
        <tests/metrics/reach.c>: baz; foo;

The first line, Syntactically reachable functions is an over-approximation of the number of functions of your program that may be eventually be called, starting from main. For example, a function whose address is never taken and which is never called directly won't be inside this set.

Semantically reached functions is the number of functions of your program indeed analyzed by the Value analysis.

Coverage estimation is the ratio between those two numbers. For small programs, in which all functions are reachable, it is usually 100%.

Unseen functions is the list of functions that were expected to be reached (syntactically), but were never analyzed by Value.

Notice that none of these numbers talk about instructions, so you may still get 100% with dead code.

Upvotes: 2

Pascal Cuoq
Pascal Cuoq

Reputation: 80276

On a single file, -metrics [introduces] 3 goto on a function [that doesn't have any]

The C constructs &&, || and break; can be “normalized” into goto constructs.

I suppose so 157 stmts in analyzed functions, 148 stmts analyzed (94.3%) that means I have dead code on my projet, it's that ?

Yes. For the inputs visible to the value analysis, only 148 out of 157 statements are reachable. Note that if, for instance, main() has arguments argc and argv, the abstract values built for these arguments may not encompass all the values that should be considered. The best way to determine whether these 9 statements are really unreachable is to look at them (they are displayed in red in Frama-C's GUI).

With option -scope-def-interproc I get me 32 warning (62 without) but on website, we can read (in scope documentation)

It is not very clear what you are asking. It would help if you provided an example with full information (source code, commandline(s)) so that one can reproduce your steps and clarify the meaning of the emitted messages for you. Produce a small, reduced example if it is impossible to get the complete example out: it is also (nearly) impossible to answer you with the information provided so far.

Upvotes: 2

Related Questions