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]

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>