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] 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