--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verifying recursive functions



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