Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] [Jessie] loop invariant
- Subject: [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- Date: Sat, 07 Sep 2013 11:14:57 +0200
- In-reply-to: <522AEA5A.3080809@inria.fr>
- References: <CAEtoXR21n9RPnwGE_UQ7zDjqrNPjhhRMuG5kQdzM=SjH7z+9CA@mail.gmail.com> <52162B8A.4080703@inria.fr> <CAEtoXR2DsVLvtKZM9PiFNPxx-=w11eY0sr2WNQ4ymdv74P-h4A@mail.gmail.com> <5216629A.5080303@inria.fr> <CAEtoXR3XiHDCd49mKyKh4GLL6ozO48u97AmeMc5qSCrhhgthow@mail.gmail.com> <CA+yPOViR89rE7Bg5Zkx5Lu5PQs8xz6RDAhSBZ1m-afYzgdgVAA@mail.gmail.com> <522AEA5A.3080809@inria.fr>
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
- Follow-Ups:
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- References:
- [Frama-c-discuss] [Jessie] loop invariant
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] [Jessie] loop invariant
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] [Jessie] loop invariant
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] [Jessie] loop invariant
- Prev by Date: [Frama-c-discuss] [Jessie] loop invariant
- Next by Date: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Previous by thread: [Frama-c-discuss] [Jessie] loop invariant
- Next by thread: [Frama-c-discuss] [Jessie] loop invariant
- Index(es):