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] introducing hypothesis with ACSL on sets of array elements witk Frama-C/Value

  • Subject: [Frama-c-discuss] introducing hypothesis with ACSL on sets of array elements witk Frama-C/Value
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Mon, 22 Jul 2013 10:17:11 +0200
  • In-reply-to: <CABbVA-AM9BV6X14rAEu=AGJ-=9zx_URUjj-3GSEtikXpNowctg@mail.gmail.com>
  • References: <569C6D7D26484241A530B87F45ADE1F80CBD5C40@AOFRWMBXRSC004.resources.atosorigin.local> <7fzjtlnlvu.fsf@cea.fr> <569C6D7D26484241A530B87F45ADE1F80CBD5FB6@AOFRWMBXRSC004.resources.atosorigin.local> <CABbVA-DnL8p6ResAQMLyJ919ZG-6sf-_zKAR-zDZ4Bf1dAWK1Q@mail.gmail.com> <569C6D7D26484241A530B87F45ADE1F80CBD69B6@AOFRWMBXRSC004.resources.atosorigin.local> <CABbVA-AM9BV6X14rAEu=AGJ-=9zx_URUjj-3GSEtikXpNowctg@mail.gmail.com>
2013/7/21 Boris Yakobowski <boris at yakobowski.org>:
> I just noticed that Frama-C's parser accepts t[0..1] < 10 and t[0..1]
>> 10 for some mysterious reason. However, 10 > t[0..1] and 10 <
> t[0..1] are (correctly) rejected. Both WP and Value choke on the first
> form, so I guess the type-checker should be made more agressive,
> unless Jessie understands this form?

This is more probably a bug.  I can't see any good reason why
t[0..1]<10 would be accepted and not 10>t[0..1].

--
E tutto per oggi, a la prossima volta
Virgile