From: wj46633@gmail.com
Subject: Re: ALI Files Cross-References Inconsistency?
Date: Wed, 30 Sep 2020 02:53:03 -0700 (PDT) [thread overview]
Message-ID: <a179ce04-0d1e-4249-8fa3-8eaba5f31a00o@googlegroups.com> (raw)
In-Reply-To: <1ab5413e-ac60-4fb7-b3bd-930de3f0fe0do@googlegroups.com>
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;
prev parent reply other threads:[~2020-09-30 9:53 UTC|newest]
Thread overview: 15+ messages / expand[flat|nested] mbox.gz Atom feed top
2020-08-13 15:24 ALI Files Cross-References Inconsistency? Leandro Ribeiro
2020-08-13 15:55 ` Dennis Lee Bieber
2020-08-13 21:18 ` Simon Wright
2020-08-14 19:45 ` Dennis Lee Bieber
2020-08-13 17:17 ` Egil H H
2020-08-14 8:11 ` Leandro Ribeiro
2020-08-14 16:35 ` Per Sandberg
2020-08-14 17:23 ` Simon Wright
2020-08-15 7:56 ` J-P. Rosen
2020-08-14 19:47 ` Dennis Lee Bieber
2020-09-25 16:16 ` Stephen Leake
2020-09-25 19:35 ` Dmitry A. Kazakov
2020-09-25 22:33 ` Stephen Leake
2020-09-26 8:03 ` Dmitry A. Kazakov
2020-09-30 9:53 ` wj46633 [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox