--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on March 2009 ---
Hello, Frama-c reports a fatal error when I run it on the following code: /*@ requires n >= 0; ensures \result == \sum(0,n, \lambda integer i; i); */ int sum(int n) { if(n==0) return 0; else return n + sum(n-1); } This is the output: ~/progs/fc/sum> frama-c -jessie-analysis sum.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD sum.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Fatal error: exception Assert_failure("src/jessie/interp.ml", 564, 19) Is this a bug in Jessie? -Boris