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] Is there any method not to initalize all global variables while doing value analysis?

  • Subject: [Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 30 Oct 2012 22:57:03 +0100
  • In-reply-to: <000001cdb6c3$abbed260$033c7720$@gmail.com>
  • References: <000001cdb6c3$abbed260$033c7720$@gmail.com>
> 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