comp.lang.ada
 help / color / mirror / Atom feed
* ALI Files Cross-References Inconsistency?
@ 2020-08-13 15:24 Leandro Ribeiro
  2020-08-13 15:55 ` Dennis Lee Bieber
                   ` (3 more replies)
  0 siblings, 4 replies; 15+ messages in thread
From: Leandro Ribeiro @ 2020-08-13 15:24 UTC (permalink / raw)


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;

^ permalink raw reply	[flat|nested] 15+ messages in thread

end of thread, other threads:[~2020-09-30  9:53 UTC | newest]

Thread overview: 15+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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 is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox