--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Semantics of \valid



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