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

[Frama-c-discuss] integer overflow



>>
>> Running Frama-C's value analysis gives this:
>>
>> Values for function foo:
>>   tmp ? {0; }
>>   __retres ? {0; }
>>
>> If I understand correctly, this means that the function must return  
>> 0.
>
> For test programs that are destined to be both analyzed and executed,
> I agree that our handling of printf is not the best. You can confirm  
> that
> the temporary variable tmp indeeds holds the value of foo(-2) by
> inspecting the normalized source code ("frama-c test.c -print").

And trying my own advice after sending it to the list, I realize
that I got it wrong and that it is __retres that holds the return
value of foo. Facepalm.

Pascal



-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090612/3a4cdf76/attachment.htm