--- layout: fc_discuss_archives title: Message 57 from Frama-C-discuss on September 2013 ---
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