---
layout: fc_discuss_archives
title: Message 15 from Frama-C-discuss on July 2013
---
[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