--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on February 2011 ---
/*@ inductive is_sum{L}(integer i, int* t, int s) { case is_sum_base{L}: \forall integer i, int* t, int s; i <= 0 ==> \at(*t,L) == s; case is_sum_left{L}: \forall integer i, int* t, int s; i > 0 && is_sum(i, t, s) ==> is_sum(i-1,t,s-\at(*(t + i),L)); } */ gives me the error foo.h:6:[kernel] user error: Error during annotations analysis: invalid implicit conversion from ? to int What am I doing wrong?