--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] sums of arrays



Is there any way to reason about the sum of the elements of an array, using Frama-C+Jessie?
I tried below, but I see \lambda is not supported by Jessie.
Maybe there is a way to use an axiomatic and define my own sum?
Or maybe I should use WP?
Thanks,
Steve


/*@
  requires n >= 1 && \valid(t+(0..n-1));
  ensures \result == \sum(0,n-1,\lambda integer k; t[k])/n;
 */
double mean(double t[], int n) {
  int i;
  double s = 0.0;

  for (i=0; i<n; i++) s += t[i];
  return s/n;
}

---

mean$ frama-c -jessie mean.c
[kernel] preprocessing with "gcc -C -E -I.  -dD mean.c"
[jessie] Starting Jessie translation
mean.c:5:[jessie] failure: Jessie plugin does not support lambda abstraction
[jessie] warning: Unsupported feature(s).
                  Jessie plugin can not be used on your code.