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 <de...@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.
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 206918)
+++ sem_res.adb (working copy)
@@ -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.
Index: restrict.ads
===================================================================
--- restrict.ads (revision 206918)
+++ restrict.ads (working copy)
@@ -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.
