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

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