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] sums of arrays

  • Subject: [Frama-c-discuss] sums of arrays
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Thu, 31 Oct 2013 08:46:09 -0400
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.