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] *p and p[0]

Hi,

I cannot comment on the issue *p vs p[0] but I would like to refer to our
treatment of max_seq and the
slightly more general max_element algorithm in our "ACSL by Example"
tutorial (Sections 3.7 and 3.8 in
http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf). 

Here max_element was completely verified using alt-ergo, Z3, CVC3, Yices,
and Simplify.

Regards

Jens




-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Pascal Cuoq
Sent: Thu 7/8/2010 12:08 AM
To: Frama-C public discussion
Subject: [Frama-c-discuss] *p and p[0]
 
Hello all,

working with the example from chapter 6 in the ACSL mini-tutorial,
I arrived (after what I believe are changes that make it simpler to
understand for both provers and students) at:

/*@ requires n > 0;
    requires \valid(p+ (0..n-1));
    assigns \nothing;
    ensures \forall int i;
                 0 <= i <= n-1 ==> \result >= p[i];
    ensures \exists int e;
                 0 <= e <= n-1 && \result == p[e];
*/
int max_seq(int* p, int n)
 {
  int res = *p;
 /*@
  loop invariant \forall integer j ;
                (0 <= j < i) ==> (res >= p[j]) ;
  loop invariant 0 <= i <= n;
  loop invariant \exists integer j ;
                (0 <= j <= n-1) && (res == p[j]) ;
  loop variant n-i ;
    */
  for(int i = 0; i < n; i++) {
    if (res < p[i]) { res = p[i]; }
  }
  return res;
}

Good news! Almost everything is proved (alt-ergo 0.91)
And what is not proved such as the establishment
of the invariant with the existential quantifier is a
good opportunity to explain how these are usually
difficult for automatic provers to handle.

Then as a last change to make the source code more
readable, I changed the *p to p[0] in the first line of
the function.

And then, better news! Everything is proved now.
I didn't even know that it was possible to distinguish
between *p and p[0] after normalization by CIL.

So my questions are:

- are the proof obligations generated when the program
uses *p provable (sorry for this naive question but I only
have alt-ergo for technical reasons)?

- should one of the various translations between C and
the proof obligations have the same results whether
*p or p[0] is used, or would that be likely to cause
more issues than it solves?

Pascal

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 4018 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100708/ec646564/attachment-0001.bin>