search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

Semantics of implicit range bounds (e.g. 0.., ..100, and ..) #24

Open maroneze opened 6 years ago

maroneze commented 6 years ago

It is not clear in the documentation the meaning of implicit bounds in the term? .. term? range construct.

Ideally, looking for "range" in the document should quickly lead to a phrase saying, for instance, that:

.. b

is equivalent to

0 .. b

and

a ..

is equivalent to

a .. \block_length(term_over_which_the_range_operates)-1

or something similar.

vprevosto commented 6 years ago

Unfortunately, this is not the case: .. b indicates the set of all integers less than or equal to b. There has been some internal discussions on allowing something like you suggest in case the range is used as pointer offset, but things aren't as simple as that: if \base_addr(p) != p, p[ .. ] should be at least equivalent to p[ -\offset(p) .. \block_length(p)-\offset(p)-1]. Moreover, the meaning of .. would heavily depend on its context. This is already the case for other constructs, but this might not help making things really clearer.