From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "J-P. Rosen" Newsgroups: comp.lang.ada Subject: Re: How to get Ada to ?cross the chasm?? Date: Sat, 12 May 2018 08:44:42 +0200 Organization: Adalog Message-ID: References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <87in88m43h.fsf@nightsong.com> <87efiuope8.fsf@nightsong.com> <87lgd1heva.fsf@nightsong.com> <87zi1gz3kl.fsf@nightsong.com> <878t8x7k1j.fsf@nightsong.com> <87fu342q1o.fsf@nightsong.com> <87mux9645j.fsf@nightsong.com> <8736yz18e4.fsf@nightsong.com> <87mux62it0.fsf@nightsong.com> <87k1sat1ie.fsf@nightsong.com> NNTP-Posting-Host: TKk5kT01+2w6guVcOjcsiQ.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 Openpgp: preference=signencrypt X-Notice: Filtered by postfilter v. 0.8.3 Content-Language: fr Xref: reader02.eternal-september.org comp.lang.ada:52307 Date: 2018-05-12T08:44:42+02:00 List-Id: 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