--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2010 ---
[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>