--- layout: fc_discuss_archives title: Message 76 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?



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