--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] loop invariant




On 09/07/2013 10:56 AM, Claude Marche wrote:
>> Alternatively, you can force the computation into float in sum
>> by modifying your axiom:
>>    @   axiom sum2{L} :
>>    @     \forall float *t, integer i, j;
>>    @       sum(t,i,j+1) == (float)(sum(t,i,j) + t[j]);
>> But this is not a very good idea IMHO: as floating point addition is

A very bad idea indeed.

- claude