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