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] Inductive definition of reachability in array-implemented list.

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