--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on July 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Nested loops



Can you tell me why the assert at the end of the following pair of nested loops is required to complete the proof.  (Try running “frama-c -wp test.c on the attached file test.c.)

/*@
  requires \valid(dst + (0 .. dstLen-1));
  assigns dst[0 .. dstLen-1];
*/
void copy2(unsigned * const dst, unsigned const dstLen) {

  unsigned i = 0;
  /*@
    loop invariant 0 <= i <= dstLen;
    loop assigns dst[0 .. dstLen-1], i;
  */
  while (i < dstLen) {
    unsigned j = 0;

    /*@
      loop invariant 0 <= i <= dstLen;
      loop invariant 0 <= j <= 10;
      loop assigns dst[0 .. dstLen-1], i, j;
    */
    while (j < 10 && i < dstLen) {
      dst[i] = 0;
      i++;
      j++;
    }
    //@ assert \at(dst, Pre) == \at(dst, Here);
  }
}

The pointer dst is declared to be a constant pointer.  I think it is possible to remove the const-ness with casts, so const doesn’t necessarily mean const.  But I was surprised that nesting loop invariants of the form “dst == \at(dst, Pre)” or “dst == \at(dst, LoopEntry)” did not solve the problem.  The final assert was the only way I could find to complete the proof.

Thanks,
Mark
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200726/43a05102/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.c
Type: application/octet-stream
Size: 558 bytes
Desc: test.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200726/43a05102/attachment-0001.obj>