This patch fixes a compiler abort (or an infinite loop in a compiler whose
internal assertions are not enabled) when the subtype indication in an object
declaration does not denote a type. Syntactically this may happen when the
subtype indication is missing altogether and the expression in the declaration
is analyzed as if it were one.
Compiling aida-ling_float_random.adb must yield:
aida-long_float_random.adb:51:23: subtype mark required in this context
aida-long_float_random.adb:53:07: assignment to "in" mode parameter
not allowed
aida-long_float_random.adb:59:07: "Temp" is undefined
(more references follow)
aida-long_float_random.adb:66:07: "Ni" is undefined (more references follow)
aida-long_float_random.adb:71:07: "Nj" is undefined (more references follow)
aida-long_float_random.adb:76:30: no selector "Cd" for type "T" defined
at aida-long_float_random.ads:57
aida-long_float_random.adb:77:10: "C" is undefined (more references follow)
aida-long_float_random.ads:27:06: warning: postcondition does not mention
function result
---
package body Aida.Long_Float_Random with SPARK_Mode is
function Make (New_I : Seed_Range_1 := Default_I;
New_J : Seed_Range_1 := Default_J;
New_K : Seed_Range_1 := Default_K;
New_L : Seed_Range_2 := Default_L
) return T
is
S : Real;
R : Real;
M : Range_1;
begin -- Set_Seed
return This : T do
This.I := New_I;
This.J := New_J;
This.K := New_K;
This.L := New_L;
This.Ni := Range_3'Last;
This.Nj := Range_3'Last / 3 + 1;
This.C := Init_C;
Fill_U : for Ii in Range_3'Range loop
S := 0.0;
R := 0.5;
pragma Loop_Invariant (S = 0.0 and R = 0.5);
Calc_S : for Jj in 1 .. 24 loop
M := (This.J * This.I) mod M1;
M := (M * This.K) mod M1;
This.I := This.J;
This.J := This.K;
This.K := M;
This.L := (53 * This.L + 1) mod M2;
pragma Loop_Invariant (R <= 0.5 and R >= 0.0);
if (This.L * M) mod 64 >= 32 then
S := S + R;
end if;
R := 0.5 * R;
end loop Calc_S;
This.U (Ii) := S;
end loop Fill_U;
end return;
end Make;
function Random (This : T) return Real is
Temp : This.Temp.Value;
begin
This.Temp := (Exists => False);
return Temp;
end Random;
procedure Calculate (This : in out T) is
begin
Temp := This.U (This.Ni) - This.U (This.Nj);
if Temp < 0.0 then
Temp := Temp + 1.0;
end if;
This.U (This.Ni) := Temp;
Ni := Ni - 1;
if Ni = 0 then
Ni := Range_3'Last;
end if;
Nj := Nj - 1;
if Nj = 0 then
Nj := Range_3'Last;
end if;
This.C := This.C - This.Cd;
if C < 0.0 then
C := C + Cm;
end if;
Temp := Temp - C;
if Temp < 0.0 then
Temp := Temp + 1.0;
end if;
end Calculate;
end Aida.Long_Float_Random;
---
package Aida.Long_Float_Random with SPARK_Mode is
type T (<>) is tagged limited private;
subtype Real is Long_Float;
M1 : constant := 179;
M2 : constant := M1 - 10;
subtype Seed_Range_1 is Integer range 2 .. M1 - 1;
subtype Seed_Range_2 is Integer range 0 .. M2 - 1;
Default_I : constant Seed_Range_1 := 12;
Default_J : constant Seed_Range_1 := 34;
Default_K : constant Seed_Range_1 := 56;
Default_L : constant Seed_Range_2 := 78;
function Make (New_I : Seed_Range_1 := Default_I;
New_J : Seed_Range_1 := Default_J;
New_K : Seed_Range_1 := Default_K;
New_L : Seed_Range_2 := Default_L
) return T;
function Random (This : T) return Real with
Global => null,
Pre => This.Is_Calculated,
Post => not This.Is_Calculated;
function Is_Calculated (This : T) return Boolean with
Global => null;
procedure Calculate (This : in out T) with
Global => null,
Post => This.Is_Calculated;
private
M3 : constant := 97;
Divisor : constant := 16777216.0;
Init_C : constant := 362436.0 / Divisor;
Cd : constant := 7654321.0 / Divisor;
Cm : constant := 16777213.0 / Divisor;
subtype Range_1 is Integer range 0 .. M1 - 1;
subtype Range_2 is Integer range 0 .. M2 - 1;
subtype Range_3 is Integer range 1 .. M3;
type U_Array_T is array (Range_3) of Real;
type Optional_Temp_T (Exists : Boolean := False) is record
case Exists is
when True => Value : Real;
when False => null;
end case;
end record;
type T is tagged limited record
I : Range_1;
J : Range_1;
K : Range_1;
Ni : Integer;
Nj : Integer;
L : Range_2;
C : Real;
U : U_Array_T;
Temp : Optional_Temp_T;
end record;
function Is_Calculated (This : T) return Boolean is (This.Temp.Exists);
end Aida.Long_Float_Random;
--
package Aida is
end Aida;
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-16 Ed Schonberg <schonb...@adacore.com>
* sem_ch3.adb (Process_Subtype): If the subtype indication does not
syntactically denote a type, return Any_Type to prevent subsequent
compiler crashes or infinite loops.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 254802)
+++ sem_ch3.adb (working copy)
@@ -21338,6 +21338,16 @@
if Nkind (S) /= N_Subtype_Indication then
Find_Type (S);
+
+ -- No way to proceed if the subtype indication is malformed.
+ -- This will happen for example when the subtype indication in
+ -- an object declaration is missing altogether and the expression
+ -- is analyzed as if it were that indication.
+
+ if not Is_Entity_Name (S) then
+ return Any_Type;
+ end if;
+
Check_Incomplete (S);
P := Parent (S);
