Hi.  With the following code

#include "vcc.h"

void get(int a[])
    _(requires \thread_local_array(a, 3) )
    _(writes \array_range(a,3) )
    _(ensures \thread_local_array(a, 3 ) )    
{
    a[0] = 1 ; a[1] = 2; a[2] = 3 ;
}

void looper() {
    int b[3] ;
    int i ;
    for( i=0 ; i < 100 ; ++i )
        _(invariant \thread_local_array(b, 3 ) )
    {
        get(b) ; /* Line 17 */
    }
}

I get error

                snip(17,3) : error VC8510: Assertion '\array_range(a,3) is writable in call to get(b)' did not verify.

I'm fairly sure I need a stronger invariant, but as \writable is not a predicate, I'm not sure how to express it.

To partially answer my own question, I replaced \thread_local_array with \mutable_array in 3 places.  The only errors now are

Verification of looper failed. [0.16]
C:\Users\theo\Documents\Visual Studio 2010\Projects\TimeOfDay\TimeOfDay\looper.c(11,1) : error VC9502: Call 'stack_free(&#stackframe#0)' did not verify.
C:\Program Files (x86)\Microsoft Research\Vcc\Headers\VccPrelude.bpl(1798,3) : error VC9599: (related information) Precondition: 'the extent of the object being reclaimed is mutable'.

Which I really don't understand at all.

Internally, the local array b[3] is embedded in a hidden object, which VCC checks for being mutable before returning from the function (the "stack-free check"). It fails to do so, because the loop with its current annotations loses information on the object. Here are some working variants:

#include "vcc.h"

void get(int a[])
  _(writes \array_range(a, 3))
{
  a[0] = 1;
  a[1] = 2;
  a[2] = 3;
}

void looper1()
{
  int b[3];
  int i;
  for (i = 0; i < 100; ++i)
    _(invariant \mutable(\embedding(&b[0])))
    _(writes \extent(\embedding(&b[0])))
  {
    get(b);
  }
}

void looper2()
{
  int b[3];
  int i;
  for (i = 0; i < 100; ++i)
    _(writes \array_range(b, 3))
  {
    get(b);
  }
}

void looper3()
{
  _(as_array) int b[3];
  int i;
  for (i = 0; i < 100; ++i)
    _(invariant \mutable(_(int[3]) b))
    _(writes \extent(_(int[3]) b))
  {
    get(b);
  }
}

Hope this helps, Mark

Thanks Mark: That helps a lot.  I didn't realize one can annotate a loop with a "writes" clause.  It makes sense if you think of a loop as a subroutine.

This made me wonder, why not allow subroutines to be annotated with "invariant" as a shorthand for "requires" and "ensures"?

Hi Theodore,

  note that _(maintains x) is already a short-hand for _(requires x) _(ensures x).

  Best, Mark

Note that _(invariant) is not the same as just adding _(requires) + _(ensures) on the loop body, because a loop invariant is asserted only at the top of the loop, whereas an _(ensures) is required to hold even if the loop exits in some other way (e.g., via a goto).