--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on March 2009 ---
You can fill a bug report, but a simple answer is that the \sum construct is not yet supported by Jessie yet, so it might be related. You can design your own definition of \sum, specific to this instance, in a similar way I proposed a definition of \product in an answer to one of your previous mails. - Claude Hollas Boris (CR/AEY1) wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |