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.

Pariente Dillon wrote:
> 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 totally agree with that, but it is not easy to do...
I am trying for instance to write a WP computation where the user
can define quite precisely what he wants to do at one point.
That means which properties to prove, and which hypotheses to use to do so.

Pariente Dillon wrote:
> 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.

Exactly : the user adds an assert, but should the tool use
all the assertions, or should it be the user who tells it to do so ?

Pascal Cuoq wrote :
> 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.

I don't think it is really specific to Caveat, and one of my goal
is to be able to do the same in Frama-C, but my 2 problems are :
1- how to tell the tool what we want to compute/prove (user GUI...) ?
2- how to define and to manage the database of the links between
the properties (called  Integrated Proof Environment by Dillon) ?

The problem is that I don't think that we can "guess" what the user 
strategy is to study a problem (when the tool is not able to discharge 
it automatically). That is why we have to provide him a way to specify 
what he wants, but this mustn't be to painful...

User wishes are welcome.

Regards,
Anne.