--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on October 2012 ---
> 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