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

[Frama-c-discuss] What is wrong with this inductive sum definition?



/*@ 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?