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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.140.144.17 with SMTP id 17mr8205906qhq.6.1439943094999; Tue, 18 Aug 2015 17:11:34 -0700 (PDT) X-Received: by 10.182.60.130 with SMTP id h2mr64222obr.28.1439943094967; Tue, 18 Aug 2015 17:11:34 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!y105no1462715qge.1!news-out.google.com!nt1ni8675igb.0!nntp.google.com!se8no6169738igc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 18 Aug 2015 17:11:34 -0700 (PDT) In-Reply-To: <6cd2abfc-63e4-4821-b8d3-143ec25f4619@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=149.32.224.36; posting-account=Qh2kiQoAAADpCLlhT_KTYoGO8dU3n4I6 NNTP-Posting-Host: 149.32.224.36 References: <6cd2abfc-63e4-4821-b8d3-143ec25f4619@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: SPARK - strange range check with array assignment From: Anh Vo Injection-Date: Wed, 19 Aug 2015 00:11:34 +0000 Content-Type: text/plain; charset=ISO-8859-1 Xref: news.eternal-september.org comp.lang.ada:27499 Date: 2015-08-18T17:11:34-07:00 List-Id: On Tuesday, August 18, 2015 at 1:06:47 PM UTC-7, Maciej Sobczak wrote: > Consider (extracted from a bigger problem): > > -- p.ads: > pragma SPARK_Mode; > > package P is > > procedure Foo (S : in out String) > with Pre => S'Length > 3; > > end P; > > -- p.adb: > pragma SPARK_Mode; > > package body P is > > procedure Foo (S : in out String) > is > begin > S (S'First .. S'First + 2) := "abc"; -- HERE > end Foo; > > end P; > > > Foo is intended to overwrite the beginning of the given string. > GNATProve (2014) says: > > p.adb:8:37: warning: range check might fail > > Curiously, the assertion added just before the failing line: > > pragma Assert (S'First + 2 in S'Range); > > passes without any warning. > > What value or expression above is subject to a range check that might fail? it went through gnatprove (2015) happily. I tested it on Windows. Anh Vo