# 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.

*Subject*: [Frama-c-discuss] Inductive definition of reachability in array-implemented list.*From*: Pascal.Cuoq at cea.fr (Pascal Cuoq)*Date*: Mon, 8 Jun 2009 17:47:36 +0200*In-reply-to*: <1244471484.3750.50.camel@guillaume-laptop>*References*: <4A28B8BD.5080509@fr.thalesgroup.com> <4A290576.5010102@fr.thalesgroup.com><4A293B6E.7010806@insa-lyon.fr> <20090605181021.0b3c566f@is005115> <5EFD4D7AC6265F4D9D3A849CEA9219191AB1D7@LAXA.intra.cea.fr> <4A2BC65E.4020202@fr.thalesgroup.com> <1244471484.3750.50.camel@guillaume-laptop>

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

**Follow-Ups**:**[Frama-c-discuss] Inductive definition of reachability inarray-implemented list.***From:*Dillon.Pariente at dassault-aviation.com (Pariente Dillon)

**References**:**[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.***From:*eric.jenn at fr.thalesgroup.com (JENN Eric)

**[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.***From:*nicolas.stouls at insa-lyon.fr (Nicolas Stouls)

**[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.***From:*virgile.prevosto at cea.fr (Virgile Prevosto)

**[Frama-c-discuss] Inductive definition of reachability in an array-implemented list.***From:*Pascal.CUOQ at cea.fr (CUOQ Pascal)

**[Frama-c-discuss] Inductive definition of reachability in array-implemented list.***From:*eric.jenn at fr.thalesgroup.com (JENN Eric)

**[Frama-c-discuss] Inductive definition of reachability in array-implemented list.***From:*guillaume.melquiond at inria.fr (Guillaume Melquiond)

- Prev by Date:
**[Frama-c-discuss] Inductive definition of reachability in array-implemented list.** - Next by Date:
**[Frama-c-discuss] Inductive definition of reachability inarray-implemented list.** - Previous by thread:
**[Frama-c-discuss] Inductive definition of reachability in array-implemented list.** - Next by thread:
**[Frama-c-discuss] Inductive definition of reachability inarray-implemented list.** - Index(es):