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=-0.4 required=5.0 tests=AC_FROM_MANY_DOTS,BAYES_00, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Received: by 10.66.162.6 with SMTP id xw6mr30996429pab.47.1425374961649; Tue, 03 Mar 2015 01:29:21 -0800 (PST) X-Received: by 10.140.48.97 with SMTP id n88mr397513qga.35.1425374961601; Tue, 03 Mar 2015 01:29:21 -0800 (PST) Path: border1.nntp.dca1.giganews.com!nntp.giganews.com!hl2no3202626igb.0!news-out.google.com!n6ni190qar.0!nntp.google.com!j7no10450784qaq.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Tue, 3 Mar 2015 01:29:21 -0800 (PST) Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=31.186.238.53; posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S NNTP-Posting-Host: 31.186.238.53 User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <56938449-64e8-4e9c-89ef-8d7fa914c9eb@googlegroups.com> Subject: SPARK problem with unconstrained arrays From: Maciej Sobczak Injection-Date: Tue, 03 Mar 2015 09:29:21 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: number.nntp.giganews.com comp.lang.ada:192388 Date: 2015-03-03T01:29:21-08:00 List-Id: I would like to play a bit with unconstrained arrays in SPARK and I found t= he following problem. Consider the package specs: pragma SPARK_Mode; package My_Package is type Index is range 1 .. 10; type My_Array is array (Index range <>) of Integer; =20 procedure Find_Min (A : in My_Array; I : out Index) with Post =3D> (I in A'Range and (for all J in A'Range =3D> A (I) <=3D A (J))); end My_Package; The Find_Min procedure is supposed to find the index of the smallest elemen= t in the array. The package body is: pragma SPARK_Mode; package body My_Package is procedure Find_Min (A : in My_Array; I : out Index) is Last_Min : Integer; begin I :=3D A'First; -- line 8 Last_Min :=3D A (A'First); -- line 9 =20 for J in A'First + 1 .. A'Last loop if A (J) < Last_Min then I :=3D J; Last_Min :=3D A (J); end if; pragma Loop_Invariant (for all K in A'First .. J =3D> I in A'First .. J and Last_Min =3D A (I) and Last_Min <= =3D A (K)); end loop; end Find_Min; =20 end My_Package; GNATprove says: C:\maciej\temp\spark>gnatprove -Ptest -q my_package.adb:8:15: warning: range check might fail my_package.adb:9:25: warning: array index check might fail my_package.ads:10:14: warning: postcondition might fail gprbuild: *** compilation phase failed gnatprove: error during generation and proof of VCs, aborting. How is it possible that VC at line 8 is not discharged? According to ARM: "A'First denotes the lower bound of the first index range; its type is the = corresponding index type." and the index type (Index) happens to be the same on both sides of the assi= gnment [*]. Curiously, VC at line 9 also fails, this time with even more surprising A (= A'First). [*] Or not. The ARM also says that unconstrained array is defined with the = subtype_mark as an index, which might be a hint that the actual type in que= stion is A'Base, which in this case is wider than 1..10. In other words, A'= First is of the type that is wider than A'Range. Adding this just before line 8 helps: pragma Assume (A'First in A'Range); but seems to be an overkill (not because it's a lot of typing, but because = it undermines the trust in the tool) and I would expect it to be deduced au= tomagically. What are your thoughts on this? --=20 Maciej Sobczak * http://www.inspirel.com/