--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2010 ---
On Fri, Jul 9, 2010 at 5:18 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > > By the way, I have no idea at all why *p versus p[0] makes a difference. > > Is it reproducible ? > > I had the problem and the students who arrived that far too, so: yes. > There's my code: -------------------------------------------------------------------------------------------------- /*@ requires n > 0; requires \valid(p+ (0..n-1)); assigns \nothing; ensures \forall integer i; 0 <= i <= n-1 ==> \result >= \old(p)[i]; ensures \exists integer e; 0 <= e <= n-1 && \result == \old(p)[e]; */ int max_seq(int* p, int n) { int res = *p; /*@ assert res == p[0]; */ /*@ loop invariant p == \at(p, Pre) + i; loop invariant 0 <= i <= n; loop invariant \forall integer j; 0 <= j < i ==> \at(p, Pre)[j] <= res; loop invariant \exists integer k; (k == 0 || 0 <= k < i) && \at(p, Pre)[k] == res; loop variant n - i; */ for(int i = 0; i < n; i++) { if (res < *p) { res = *p; } p++; } return res; } ---------------------------------------------------------------------------------------- I find out that if we wrote the assertion, then the prover (both alt-ergo and cvc3) are able to prove the assertion and loop invariant. But if we did not do so (remove the assertion to reproduce), both alt-ergo and cvc3 are not able to prove some of the proof obligations. (but different) "Function max_seq Default behavior > 5. loop invariant initially holds" - Alt-Ergo (0.91) gives UNKNOWN - CVC3 (2.2) gives GREEN "Function max_seq Safety > 3. pointer dereferencing" "Function max_seq Safety > 4. pointer dereferencing" - Alt-Ergo (0.91) gives GREEN - CVC3 (2.2) gives TLE On Fri, Jul 9, 2010 at 5:18 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: > Actually, the same student who also reported an alt-ergo soundness bug > also found that using p[0] was no longer enough to help if he inserted > an irrelevant assignment like: > Global = 402; > at the beginning of the function. > This can reproduced by following code, which is written incorrectly intentionally. I am expecting that Frama-C/Jessie will tell me that the function code violate the "assigns" annotation. However, Frama-C/Jessie tells me that loop invariant can't be proved. -------------------------------------------------------------------------------------------------- int global; // Here comes an global /*@ requires n > 0; requires \valid(p+ (0..n-1)); assigns \nothing; // Specify that this function do not assign any non-local or local-static variable. ensures \forall integer i; 0 <= i <= n-1 ==> \result >= \old(p)[i]; ensures \exists integer e; 0 <= e <= n-1 && \result == \old(p)[e]; */ int max_seq(int* p, int n) { global = 402; // Just assign something and VIOLATE the "assigns" annotation. int res = *p; /*@ assert res == p[0]; */ /*@ loop invariant p == \at(p, Pre) + i; // Some of the loop invariant can't be proved loop invariant 0 <= i <= n; loop invariant \forall integer j; 0 <= j < i ==> \at(p, Pre)[j] <= res; loop invariant \exists integer k; (k == 0 || 0 <= k < i) && \at(p, Pre)[k] == res; loop variant n - i; */ for(int i = 0; i < n; i++) { if (res < *p) { res = *p; } p++; } return res; } ---------------------------------------------------------------------------------------- "Function max_seq Default Behavior > 7. loop invariant initially holds" - Alt-Ergo (0.91) gives Unknown - CVC3 (0.22) gives TLE However, if I have remove the assignment or change the "assigns \nothing." annotation to "assigns global;" then both Alt-Ergo and CVC3 gives GREEN. But I have no idea for why the loop invariants will be affected if I violates assigns annotation. Logan (Tzu-hsiang Chien) -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100709/4beebe93/attachment.htm>