--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on April 2009 ---
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