From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.5-pre1 (2020-06-20) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=0.8 required=3.0 tests=BAYES_50,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.5-pre1
X-Received: by 2002:a05:620a:1645:: with SMTP id c5mr1700751qko.357.1601459584546;
        Wed, 30 Sep 2020 02:53:04 -0700 (PDT)
X-Received: by 2002:ac8:75d2:: with SMTP id z18mr1368198qtq.346.1601459584350;
 Wed, 30 Sep 2020 02:53:04 -0700 (PDT)
Path: eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 30 Sep 2020 02:53:03 -0700 (PDT)
In-Reply-To: <1ab5413e-ac60-4fb7-b3bd-930de3f0fe0do@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: google-groups.googlegroups.com; posting-host=167.172.61.174; posting-account=R-DQkAoAAAACrgngBXk4Yl9YUy8Nd09M
NNTP-Posting-Host: 167.172.61.174
References: <1ab5413e-ac60-4fb7-b3bd-930de3f0fe0do@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a179ce04-0d1e-4249-8fa3-8eaba5f31a00o@googlegroups.com>
Subject: Re: ALI Files Cross-References Inconsistency?
From: wj46633@gmail.com
Injection-Date: Wed, 30 Sep 2020 09:53:04 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:60335
List-Id: <comp.lang.ada>

On Thursday, August 13, 2020 at 8:54:47 PM UTC+5:30, Leandro Ribeiro wrote:
> Hello, everyone 
> 
> I recently started to take a better look into Ada.
> 
> I am currently analyzing .ali files.
> 
> In the code snippets below (.ads and .adb), I wrote "|" to show where the ALI file claims a given symbol is.
> The (line X) just tells which line number the line had in my local text editor.
> 
> I would expect every reference to point to the beginning of the symbol, as it is the case with "3K9*excep2".
> However, all other references to the symbols from excep2.ads are exactly 4 columns ahead of the "expected point".
> And all the references to the symbols from excep2.adb are exactly 12 columns ahead of the "expected point".
> 
> 
> Question:
> Is this a bug?
> Or did a miss any rule about adding offsets to the references?
> 
> 
> 
> ======== excep2.ali
> ...
> X 1 excep2.ads
> 3K9*excep2 13l5 13e11 2|3b14 22l5 22t11
> 6U19*excep 7>10 8>9 8>12 9<9 10<9 2|5b19 20l13 20t18
> 7a10 S{string} 2|6b10 10r30 11r28 13r31
> 8e9 C{character} 2|6b22 13r38
> 8e12 Delim{character} 2|6b25 11r35
> 9b9 Found{boolean} 2|6b44 9m17 15m33
> 10i9 Position{positive} 2|6b64 14m38
> X 2 excep2.adb
> 10i25 J{integer} 11r30 13r33 14r50
> ...
> 
> ======== excep2.ads
> pragma SPARK_Mode;
> 
> package |excep2 
> is
> (line 5)-- procedure finds first occurence of char C before char Delim
>         procedure exce|p 
> 	(S : |String; 
> 	C, D|eli|m : Character; 
> 	Foun|d: out Boolean; 
> (line10)Posi|tion : out Positive)
>         with Annotate => (GNATprove, Intentional,
>                "might not be initialized in", "reviewed by Leandro: If it can be used (Found=True), it is surely initialized");
> end excep2;
> 
> 
> ======== excep2.adb
> pragma SPARK_Mode;
> 
> package body excep2 is
> 	-- procedure finds first occurence of char C before char Delim
> (line 5)procedure excep 
> 	(S : String; C, Delim : Character; Found: out Boolean; Position : out Positive)
>  is
> 	begin
> 		Found := False;
> (line 10)	for	J in S'Range| loop
> 			if S(J) = Delim then
> 				return;
> 			elsif S(J) = C
> 				then Position := J;
> (line 15)				Found := True;
> 				return;
> 			end if;
> 		end loop;
> 		return;
> (line 20)end excep;
> 
> end excep2;