===================================================================
@@ -5279,8 +5279,7 @@
is
Subp_Alias : constant Entity_Id := Alias (S);
begin
- return S = E
- or else (Present (Subp_Alias) and then Subp_Alias = E);
+ return S = E or else (Present (Subp_Alias) and then Subp_Alias = E);
end Same_Or_Aliased_Subprograms;
-- Start of processing for Resolve_Call
@@ -5630,6 +5629,16 @@
if Comes_From_Source (N) then
Scop := Current_Scope;
+ -- Check violation of SPARK_05 restriction which does not permit
+ -- a subprogram body to contain a call to the subprogram directly.
+
+ if Restriction_Check_Required (SPARK_05)
+ and then Same_Or_Aliased_Subprograms (Nam, Scop)
+ then
+ Check_SPARK_Restriction
+ ("subprogram may not contain direct call to itself", N);
+ end if;
+
-- Issue warning for possible infinite recursion in the absence
-- of the No_Recursion restriction.
===================================================================
@@ -254,7 +254,7 @@
(Msg : String;
N : Node_Id;
Force : Boolean := False);
- -- Node N represents a construct not allowed in formal mode. If this is
+ -- Node N represents a construct not allowed in SPARK_05 mode. If this is
-- a source node, or if the restriction is forced (Force = True), and
-- the SPARK_05 restriction is set, then an error is issued on N. Msg
-- is appended to the restriction failure message.
In SPARK 2005, a subprogram may not contain a direct call to itself. This patch checks this if SPARK_05 restriction is set as shown in the following example: 1. pragma Restrictions (SPARK_05); 2. package SPARKRec is 3. procedure p1 (X : Boolean; Y : Integer); 4. end SPARKRec; 1. pragma Restrictions (SPARK_05); 2. package body SPARKRec is 3. procedure p1 (X : Boolean; Y : Integer) is 4. begin 5. if X then 6. p1 (Y > 10, Y - 1); | >>> violation of restriction "SPARK_05" at sparkrec.ads:1 >>> subprogram may not contain direct call to itself 7. end if; 8. end p1; 9. end SPARKRec; Tested on x86_64-pc-linux-gnu, committed on trunk 2014-01-22 Robert Dewar <dewar@adacore.com> * restrict.ads: Minor reformatting. * sem_res.adb (Resolve_Call): Check for SPARK_05 restriction that forbids a call from within a subprogram to the same subprogram.