[Ada] Failure to detect trivial infinite recursion
This patch reimplements the detection of trivial infinite recursion to
remove the implicit assumptions concenring the structure and contents of
the enclosing subprogram statements.
------------
-- Source --
------------
-- infinite.adb
procedure Infinite with SPARK_Mode is
function Func_1 (Val : Integer) return Integer;
function Func_2 (Val : Integer) return Integer;
function Func_3 (Val : Integer) return Integer;
function Func_4 (Val : Integer) return Integer;
function Func_5 (Val : Integer) return Integer;
function Func_6 (Val : Integer) return Integer;
function Func_7 (Val : Integer) return Integer;
function Func_8 (Val_1 : Integer; Val_2 : Integer) return Integer;
procedure Proc_1 (Val : Integer);
function Func_1 (Val : Integer) return Integer is
begin
return Func_1 (Val); -- WARN
end Func_1;
function Func_2 (Val : Integer) return Integer is
begin
return Func_2 (123); -- none
end Func_2;
function Func_3 (Val : Integer) return Integer is
Temp : Integer;
begin
Temp := Func_3 (Val); -- WARN
return Temp;
end Func_3;
function Func_4 (Val : Integer) return Integer is
Temp : Integer;
begin
Temp := Func_4 (123); -- none
return Temp;
end Func_4;
function Func_5 (Val : Integer) return Integer is
begin
Proc_1 (Val);
return Func_5 (Val); -- none
end Func_5;
function Func_6 (Val : Integer) return Integer is
begin
Proc_1 (Val);
return Func_6 (123); -- none
end Func_6;
function Func_7 (Val : Integer) return Integer is
begin
raise Program_Error;
return Func_7 (Val); -- none
end Func_7;
function Func_8 (Val_1 : Integer; Val_2 : Integer) return Integer is
begin
return Func_8 (Val_1, 123); -- none
end Func_8;
procedure Proc_1 (Val : Integer) is
begin
Proc_1 (Val); -- WARN
end Proc_1;
begin null; end Infinite;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c infinite.adb
infinite.adb:14:14: infinite recursion
infinite.adb:14:14: Storage_Error would have been raised at run time
infinite.adb:25:15: infinite recursion
infinite.adb:25:15: Storage_Error would have been raised at run time
infinite.adb:61:07: infinite recursion
infinite.adb:61:07: Storage_Error would have been raised at run time
2019-07-05 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* sem_res.adb (Check_Infinite_Recursion): Reimplemented.
(Enclosing_Declaration_Or_Statement,
Invoked_With_Different_Arguments, Is_Conditional_Statement,
Is_Control_Flow_Statement, Is_Immediately_Within_Body,
Is_Raise_Idiom, Is_Raise_Statement, Is_Sole_Statement,
Preceded_By_Control_Flow_Statement,
Within_Conditional_Statement): New routines.
From-SVN: r273116