--- layout: fc_discuss_archives title: Message 19 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]



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>