# 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

**Follow-Ups**:**[Frama-c-discuss] *p and p[0]***From:*hollas at informatik.htw-dresden.de (Boris Hollas)

**[Frama-c-discuss] *p and p[0]***From:*Dillon.Pariente at dassault-aviation.com (Pariente Dillon)

**[Frama-c-discuss] *p and p[0]***From:*jens.gerlach at first.fraunhofer.de (Jens Gerlach)

- Prev by Date:
**[Frama-c-discuss] questions after attempting to use jessie on a matrix library** - Next by Date:
**[Frama-c-discuss] *p and p[0]** - Previous by thread:
**[Frama-c-discuss] questions after attempting to use jessie on a matrix library** - Next by thread:
**[Frama-c-discuss] *p and p[0]** - Index(es):