--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : RE : The Capabilities of Frama-C



CUOQ Pascal wrote:
>> Let's consider a program that builds a large graph (tree or linked list) 
>> in dynamic memory. Each element of the graph is a structure containing 
>> fields with data. Will the implemented analysis be able to define right 
>> and precise values for each member of this graph on the heap?
> 
> Warning: long answer coming up.
> 
> While it can theoretically be useful to run the value analysis on deterministic
> programs that always execute the same computation and return the
> same result every time, it is most useful in practice when there is
> non-determinism in the execution -- for instance, the program
> accepts some inputs that are subsequently used for computing
> something. This non-determinism is typically introduced with
> built-ins provided for this purpose (there are other ways too).
> One of these built-ins is for instance 
> called Frama_C_interval(int, int); This is useful to specify
> expected ranges for inputs, values from sensors, ...
> 
> The answer to your question completely depends whether there
> is non-determinism in the shape of the allocated blocks (the way
> they point to one another). If there isn't
> (say, the non-determinism is only in the integer values of the
> data fields), then it is likely possible to make a precise analysis.
> An example of such a program is used as a benchmark in
> the article there:
> http://portal.acm.org/citation.cfm?doid=1411304.1411308
> I'll send you a copy if you do not have the necessary subscription.

Thank you, I have the subscription to ACM.

> This example uses a modelization of malloc where each invocation
> of malloc creates a new variable. This breaks the widening
> mechanism, so if there are some calls to malloc inside a loop,
> this loop needs to be completely unrolled. Apart from that,
> this modelization works very well when the "no non-determinism
> in the shape" restriction applies. It even detects out-of-bound
> accesses to a dynamically allocated block.
> 
> If there is non-determinism in the shape of the allocated blocks,
> you may still get a result that is good enough for you with
> one of the other malloc modelizations, but even if one of them
> work, you shouldn't expect the results to be as precise.
> 
>> What are 
>> approximate memory requirements for conducting analysis on such a small 
>> program building large complex structures in dynamic memory?
> 
> The benchmark in the above article is a small program
> that allocates many blocks. Thousands of calls to malloc
> translated in hundreds of megabytes of memory used by the
> analyzer.
> 
>> Many existing algorithms use widening and other techniques leading to 
>> precision loss and even wrong information. As far as I could understand 
>> Frama-C framework is based on abstract interpretation approach, so it 
>> bounds the size of programs being analyzed. Especially if each path in 
>> the program is considered separately. How could you estimate resources 
>> needed for conducting the analysis depending on the size of the program 
>> being analyzed?
> 
> The figures I gave for the resources earlier and now are only
> typical figures for resource use. It all depends on the analyzed program.
> Execution paths are merged by default, with an option to keep
> a number of them separated. This gives the user control over the
> compromise between precision and resources use. 
> Even when this option is used, execution paths are automatically merged
> when the values of the variables are identical to (or included in) 
> the values of another path. With this and other techniques (e.g. hashconsing,
> described in the article), resource use is kept to the minimum possible
> for representing the final results.
> 
> The "final results" are tables indicating the values of variables in each
> statement of the analyzed program. If you don't need these tables,
> we can show you how to omit updating them during the analysis,
> which will greatly reduce memory use.
> 
> Regards,
> 
> Pascal

Thank you for your answer. It makes things clearer.

By the way, aren't Binary Decision Diagrams used in Frama-C?

Best regards,
	Vadim TSES'KO