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]

  • Subject: [Frama-c-discuss] *p and p[0]
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Thu, 8 Jul 2010 06:08:37 +0800
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