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 inarray-implemented list.

  • Subject: [Frama-c-discuss] Inductive definition of reachability inarray-implemented list.
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Tue, 9 Jun 2009 10:27:10 +0200
  • In-reply-to: <A7757625-CA31-47B5-B58D-A0E5CC42A5D9@cea.fr>
Hello,

> >> 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)?

I would like to emphasize the interest in this issue.
To my point of view, this would/should be part of an Integrated Proof Environment (say, an IDE for Proofs, already discussed with some of you).
Consolidating/centralizing results obtained from the different Frama-C's plugins, is absolutely necessary to address large applications.

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

As the slicer is able to slice into annotations, wouldn't it be interesting to embed it in the process?
Wrt a property given by the user, the slicer is intended to do the job of simplifying annotations: keeping only those of "interest", isn't it? Wouldn't it be able to slice ... into the *Value Analysis states* according to user's slicing criteria?
This is not exactly the "'cut' strategy" of course ...

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

I do agree. This is in a certain way what I had in mind, indeed. Except it was more limited:

1?) Suppose that when we annotate a code, at a certain control point we guess that Jessie has to know that "*p==12". 
Suppose that making Jessie validate this assertion "*p==12" is a difficult/long task (because it entails the annotation of the whole application, for instance).
So, in a first step, this might be simply inserted by the user as "//@ assert *p==12;" in a particular control point of the code.

2?) Value Analysis Plugin computes values and validates the assertion "//@ assert *p==12;".
This relevant result is stored into the IPE (let me suppose that it is a kind of database, ... just for the fun!).

3?) When discharging POs generated by Jessie/Why on the whole application, the IPE (say, the part of it related to GWhy) is able to get the validity of POs related to "//@ assert *p==12;" back into the IP+GWhy PO's status "matrix".

This is a "non specialist-end user" picture of how plug-ins might collaborate, of course. 

Hummm! Not sure I'm clear enough. So this is the same idea, expressed differently, to sum up:
PO's validity or annotation's validity (+ their code control point they are attached to)
would be stored by each Frama-C plug-in into a kind of Proof's database.
This Proof's database is requested by the IPE+GWhy in order to ensure that all POs are validated, or at least to provide users with POs' status, whatever the plugin which was used to (in)validate them.

Any comments?

Best regards,
Dillon