--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on February 2011 ---
Hello, Le dim. 27 f?vr. 2011 09:10:59 CET, dclist <dclist at gmail.com> a ?crit : > /*@ inductive is_sum{L}(integer i, int* t, int 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)); > } > */ > foo.h:6:[kernel] user error: Error during annotations analysis: > invalid implicit conversion from ? to int > > What am I doing wrong? The problem is that s-\at(*(t + i),L) has type integer, as all operations on integers. Thus, you can't directly give this expression as third argument to function is_sum, that is expecting a plain int at this place. You either have to cast the result into int, meaning that you either know that your sum stays between INT_MIN and INT_MAX or you're interested in modulo operations, or to declare is_sum as taking an integer as third argument. By the way, the formulation of is_sum_left is a bit strange. Since your base case say something about is_sum(0,...), the inductive case should rather be of the form is_sum(i,..) ==> is_sum(i+1,..). Otherwise, you won't be able to derive information for other things than is_sum(0,..). -- E tutto per oggi, a la prossima volta. Virgile