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 : The Capabilities of Frama-C

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