--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on April 2009 ---
CUOQ Pascal wrote: > I am not sure I understand the question about > "values of dynamic objects", but if the question is whether > the analyzer can distinguish the different values successively > taken by a variable during the execution, the answer is "yes". I would like to consider an example to make clear "values of dynamic objects": 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? What are approximate memory requirements for conducting analysis on such a small program building large complex structures in dynamic memory? I'm sorry for quite a specific example. 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? I'm very interested in details of Frama-C algorithms and I have many questions. Could you please provide me with the list of major publications (articles) for me to be able to understand Frama-C algorithms, their potential and limitations more deeply. > A tutorial that will double as a > demonstration of the value analysis' capabilities on > "real" software should be available very soon. Looking forward to reading the tutorial! Thank you very much for your expanded answer! Best regards, Vadim TSES'KO