--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on June 2009 ---
As a minor remark about \valid_range, I would like to add that I find it always a bit odd that I have to specify \valid_range(a, 0, n-1) to express an array of length n. I would prefer "\valid_range(a, 0, n)" or even shorter "\valid_range(a, n)". In other words, I think that right open ranges fit better to C. Regards Jens > > > Concerning \valid_range, I don't see why this predicate is > necessary. I think it just makes it more difficult for the user as > he has to read both the definitions of \valid and \valid_range and > ponder what the difference is. > > How about removing \valid_range? In this case, the user can define > his own predicate, eg \valid_range(a,l,r) <==> l < r && \valid(a+ > (l..r)) > > Regards, > Boris > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Dr.-Ing. Jens Gerlach Eingebettete Systeme - EST Tel.: +49 (0)30 6392 1841 Fax.: +49 (0)30 6392 1805 E-Mail: jens.gerlach at first.fraunhofer.de Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST Kekul?stra?e 7 12489 Berlin Germany http://www.first.fraunhofer.de -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090615/d38380e3/attachment.htm