--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on October 2013 ---
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.