# 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*: jens.gerlach at first.fraunhofer.de (Jens Gerlach)*Date*: Thu, 8 Jul 2010 11:08:26 +0200*References*: <AANLkTilI3kkIGKj5HpnwxXImAet3adtBhsWbaXop7m-c@mail.gmail.com>

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>

**References**:**[Frama-c-discuss] *p and p[0]***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

- Prev by Date:
**[Frama-c-discuss] *p and p[0]** - Next by Date:
**[Frama-c-discuss] *p and p[0]** - Previous by thread:
**[Frama-c-discuss] *p and p[0]** - Next by thread:
**[Frama-c-discuss] *p and p[0]** - Index(es):