[Ada] Failure to detect trivial infinite recursion
authorHristian Kirtchev <kirtchev@adacore.com>
Fri, 5 Jul 2019 07:02:51 +0000 (07:02 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Fri, 5 Jul 2019 07:02:51 +0000 (07:02 +0000)
commit60a38ae15cbee078c0886720e3ee3d4118593216
treed9385ed8f502e6abd2a8d5a1eb1c57ce9e8d05a3
parent43fa58c26a05f206ac36ab7d0340744c2769424f
[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
gcc/ada/ChangeLog
gcc/ada/sem_res.adb