framac sample

framac_sample.c

#include <stdio.h>


/*@
 requires \forall int i; 0<=i<=9 ==> x[i] == 0 || x[i] == 1;
 requires 0 <= offset <= n;
 assigns \nothing;

 ensures 0 <= offset <= \result <=n;
 ensures \result < n ==>
      (offset <= \result && x[\result] == 1
      && ! (\exists integer i; offset <= i < \result && x[i] == 1 ));
 ensures \result == n ==>
      ! \exists integer i; offset <= i < n && x[i] == 1;
*/
int get_next(int x[], int offset, int n)
{

  /*@
    loop invariant offset <= i <= n;
    loop invariant !\exists int j; offset <= j < i && x[j] == 1;
    loop assigns i;
    loop variant n -i;
  */
  for(int i = offset; i < n; i++) {
    if (x[i] == 1)
      return i;
  }
  return n;
}

/*@
 requires \forall int i; 0<=i<=9 ==> b[i] == 0 || b[i] == 1;
 requires \forall int i; 0<=i<=9 ==> c[i] == 0 || c[i] == 1;
 assigns a[0 .. 9];

 ensures \forall integer i;  0<=i<=9 ==>
          ((\old(b[i]) == 1) && (\old(c[i]) == 1)) ==> a[i] == 1;
 ensures \forall integer i; 0<=i<=9 ==>
          ! ((\old(b[i]) == 1) && (\old(c[i]) == 1)) ==> a[i] == 0;
 ensures \forall int i; 0<=i<=9 ==> a[i] == 0 || a[i] == 1;
*/
void and(int a[], int b[], int c[])
{
  /*@
    loop invariant 0<= i <=10;
    loop invariant \forall integer j; 0<= j < i ==>
              a[j] == ((\at(b[j], Pre)== 1 && \at(c[j], Pre) == 1)? 1 :0);
    loop assigns i, a[0..9];
    loop variant 10-i;
  */
  for (int i = 0; i < 10; i ++) {
    a[i] = (b[i] == 1 && c[i] == 1)? 1 : 0;
  }
}

/*@
  requires \valid(x);
  requires \forall int i; 0<=i<=9 ==> x[i] == 0 || x[i] == 1;
  assigns x[0..9];
*/
void f(int x[])
{
  int y[10];

  /*@
    loop invariant 0<=i <=10;
    loop assigns i, x[0..9], y[0..9];
    loop invariant \forall int l; 0<=l<=9 ==> x[l] == 0 || x[l] == 1;
    loop invariant \forall int l; 0<=l< i ==> x[i] == 0;
    loop variant 10-i;
  */
  for(int i = 0; i = get_next(x, i, 10), i < 10; i++) {

    // create mask s.t. ~ (1 << i) but for an array
    /*@
      loop invariant 0<=j <=10;
      loop invariant \forall int l; 0<= l < j ==>  y[l] == 1 || y[l] == 0;
      loop invariant \forall int l; 0<= l < j ==> ( i == l  <==> y[l] == 0);
      loop assigns j, y[0..9];
      loop variant 10-j;
    */
    for (int j = 0; j < 10; j ++) {
      if (j == i)
        y[j] = 0;
      else
        y[j] = 1;
    }

    and(x, x, y);
  }

}

/*
int main() {
  int x[10];
  // init
  for (int i = 0; i < 10; i ++) {
    x[i] = 0;
  }
  //@ assert \forall int i; 0<=i<=9 ==> x[i] == 0 || x[i] == 1;

  x[2] = 1;
  x[5] = 1;
  x[9] = 1;

  f(x);
}
*/

sample2.c

/*@
  //requires \separated(a+(0..10-1), b+(0..10-1), b+(0..10-1));

  //requires \separated(a + (0..), b + (0..)) || a == b;
  //requires \separated(a + (0..), c + (0..)) || a == c;

  assigns a[0..9] \from \old(b[0..9]), \old(c[0..9]);
  // Should I write assigns for b, and c? i.e. how to care about the case a == b?

  ensures \forall integer i; 0<= i < 10 ==> a[i] == \old(b[i]) + \old(c[i]);
*/
void f(int a[], int b[], int c[])
{
  /*@
    loop invariant 0<= i <=10;
    loop invariant \forall integer j; 0<= j < i ==>
              a[j] == \at(b[j], Pre) + \at(c[j], Pre);
    loop assigns i, a[0..9];
    loop variant 10-i;
  */
  for(int i = 0; i < 10; i++) {
    a[i] = b[i] + c[i];
  }
}


void g() {
  int a[100];
  int b[100];
  int c[100];

  for (int i = 0; i < 10; i++) {
    a[i] = i;
    b[i] = i;
    c[i] = i;
  }

  f(a, b, c);
  f(a, a, a); // I want this type of call.
  //f(&a[1], a, &a[2]); // This should not be allowed.
}