--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?



> The speed is the biggest problem I encountered. Maybe this system (vim-6.2)
> which I analysis is too complicate for frama-c.

Frama-C is a static analysis platform. It can parse and type Vim,
therefore Vim is not too complicated for Frama-C.

You are using Frama-C's value analysis plug-in, a state-of-the-art
static analysis component that has been successfully applied
to large codebases of industrial embedded C code.
Vim is not exactly embedded code. Maybe Frama-C's
value analysis is able to handle it, and maybe it isn't.
If it weren't, it would not mean that Vim is too complicated
for Frama-C, just that it is outside the scope of one of Frama-C's
plug-ins.
But wait! You are not doing a verification of Vim with Frama-C's value
analysis. You are using the value analysis in an
unconventional fashion to obtain results that you
need for something else you want to do.
Would you say that a hammer is unable
to handle nails because you tried to smash it on a hundred nails
at once and it did not do what you expected?

> I have use the following options to speed up value analysis:
> 1.  -slevel 10000

Do you have any reason to think that this makes the analysis faster?
I think that the documentation is rather clear on the fact that
option -slevel improves precision, usually at the cost of time and memory.

> Is there any method to ignore those errors like "length of array size is
> zero" and continue to do value analysis?

The C99 standard says:

6.7.5.2 Array declarators
Constraints

1. [...] If the expression is a constant expression, it shall have a
value greater than zero.

Pascal