--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Inductive definition of reachability in array-implemented list.



Le dimanche 07 juin 2009 ? 15:53 +0200, JENN Eric a ?crit :

> For instance, would it be possible to generate assertions by means of 
> value analysis and back annotate the code before using Jessie? (Even 
> better, could the results of value analysis be used as some kind of 
> "axioms" (I mean something that does not need to be proved but that can 
> be taken as granted)?

This is a feature I was interested in too. Unfortunately, the conclusion
was that the value analysis plugin wouldn't know which axioms to
generate; it would just overload the Jessie plugin if it dumped
everything it knows about the program. But hopefully I'm remembering
incorrectly and someone will say that it actually works.

Regards,

Guillaume