--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on June 2009 ---
On Jun 8, 2009, at 4:31 PM, Guillaume Melquiond wrote: > 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 [...] But hopefully I'm remembering incorrectly I have the same memories of the discussion, but thinking again about this, it seems to me that someone with knowledge of both Jessie and the value analysis could possibly design an algorithm to insert only those annotations that are unambiguously going to be useful to Jessie (even if that means discarding info that could have been useful). Perhaps the technical details are best discussed outside this list, but Caveat has a mechanism to make a logical "cut" wrt an assertion, during the WP computation, at the point the assertion is encountered. Such a mechanism would be ideal, but I'm worried it's specific to Caveat. Another way to look at this is to use the value analysis to guarantee that a certain statement (say "*p = 12;") is equivalent to a simpler statement (say "x = 12;") and to compute the WP on the second one instead of the first one. This approach seems limited: if p can only be determined to point to x or y, doing the transformation "*p=12;" -> "if (nondet()) x=12; else y=12;" can either be a gain of a loss depending on the property that is to be proved. Providing the information that "p==&x || p===&y" as an assertion would be more robust, as it would give the prover a chance to make use of the property without forcing it to. Pascal