Re: How to get Ada to ?cross the chasm??

["J-P. Rosen" <rosen@adalog.fr>]

Le 12/05/2018 à 00:04, Niklas Holsti a écrit :
>> Also note that in the common special case of loop iteration, no checks
>> are
>> needed at all, either at the generation of the index or it's use:
>>
>>      for I in Arr'Range loop
>>           ... Arr(I) ...
>>      end loop;
>>
>> I cannot be outside of it's range by construction, so no checks needed
>> there
>> other than the usual loop termination check, and that being the case, no
>> checks are needed on the array indexing, either.
> 
> Yes, but for the analogous C loop, a bounds-checking C compiler would
> seldom need deep analysis to come to the same conclusion, using perhaps
> one or two checks on the loop limits against the size of the array
> (which a bounds-checking C compiler would have to pass around, to
> simulate the Ada 'Length attribute).
I doubt it, because the loop index can be modified at any time. It might
be provable if the index is local to the loop (is it possible in C, or
is it just C++?), its address is not taken, it is not visible from nor
passed to any function, it can be proven that the upper bound is not
changed by the loop...

Very far away from the general guarantee of Ada!

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr