--- 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



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