In SPARK 2005, it is not permitted to have a call to a subprogram
in the same unit as the subprogram if the body occurs later on.
This implements that rule if restriction SPARK_05 is active as
shown by the following example:
1. pragma Restrictions (SPARK_05);
2. package SPARKRec2 is
3. function P1 return Integer;
4. X : Integer := P1;
|
>>> violation of restriction "SPARK_05" at line 1
call to subprogram cannot appear before its
body
>>> violation of restriction "SPARK_05" at line 1
initialization expression is not appropriate
>>> warning: cannot call "P1" before body seen,
Program_Error will be raised at run time
5. function P2 return Integer;
6. pragma Import (C, P2);
7. Y : Integer := P2;
|
>>> violation of restriction "SPARK_05" at line 1
initialization expression is not appropriate
8. package SPARKRecP is
|
>>> violation of restriction "SPARK_05" at line 1
package specification cannot contain a package
declaration
9. end SPARKRecP;
10. end SPARKRec2;
1. pragma Restrictions (SPARK_05);
2. package body SPARKRec2 is
3.
4. XXX : Integer;
5.
6. function P3 return Integer is
7. begin
8. return P1;
|
>>> violation of restriction "SPARK_05" at
sparkrec2.ads:1
call to subprogram cannot appear before its
body
9. end P3;
10.
11. package body SPARKRecP is separate;
12.
13. function P1 return Integer is
14. begin
15. return 13;
16. end P1;
17.
18. function P2a return Integer;
19. pragma Import (C, P2a);
20. begin
21. XXX := P1;
22. XXX := P2;
23. XXX := P2a;
24. end SPARKRec2;
1. pragma Restrictions (SPARK_05);
2. separate (SPARKRec2)
3. package body SPARKRecP is
4. function JJ return Integer is
5. begin
6. return P1;
|
>>> violation of restriction "SPARK_05" at line 1
call to subprogram cannot appear before its
body
7. end JJ;
8. end SPARKRecP;
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-22 Robert Dewar <de...@adacore.com>
* lib.adb (In_Extended_Main_Code_Unit): Return False for
Standard_Location.
(In_Extended_Main_Source_Unit): Return False for Standard_Location.
* lib.ads (In_Extended_Main_Code_Unit): Add documentation on
treatment of Slocs No_Location and Standard_Location.
* restrict.adb (Check_Restriction_No_Dependence): Explicitly
check for entity with Standard_Location Sloc, rather than relying
on Lib routines to do that.
* sem_res.adb (Resolve_Call): Implement SPARK_05 restriction
that a call cannot occur before a later occuring body within
the same unit.
Index: lib.adb
===================================================================
--- lib.adb (revision 206918)
+++ lib.adb (working copy)
@@ -718,7 +718,7 @@
is
begin
if Sloc (N) = Standard_Location then
- return True;
+ return False;
elsif Sloc (N) = No_Location then
return False;
@@ -750,7 +750,7 @@
function In_Extended_Main_Code_Unit (Loc : Source_Ptr) return Boolean is
begin
if Loc = Standard_Location then
- return True;
+ return False;
elsif Loc = No_Location then
return False;
@@ -787,7 +787,7 @@
-- Special value cases
elsif Nloc = Standard_Location then
- return True;
+ return False;
elsif Nloc = No_Location then
return False;
@@ -826,7 +826,7 @@
-- Special value cases
elsif Loc = Standard_Location then
- return True;
+ return False;
elsif Loc = No_Location then
return False;
Index: lib.ads
===================================================================
--- lib.ads (revision 206918)
+++ lib.ads (working copy)
@@ -520,6 +520,14 @@
-- instantiations are included in the extended main unit for this call.
-- If the main unit is itself a subunit, then the extended main code unit
-- includes its parent unit, and the parent unit spec if it is separate.
+ --
+ -- This routine (and the following three routines) all return False if
+ -- Sloc (N) is No_Location or Standard_Location. In an earlier version,
+ -- they returned True for Standard_Location, but this was odd, and some
+ -- archeology indicated that this was done for the sole benefit of the
+ -- call in Restrict.Check_Restriction_No_Dependence, so we have moved
+ -- the special case check to that routine. This avoids some difficulties
+ -- with some other calls that malfunctioned with the odd return of True.
function In_Extended_Main_Code_Unit (Loc : Source_Ptr) return Boolean;
-- Same function as above, but argument is a source pointer rather
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 206929)
+++ sem_res.adb (working copy)
@@ -5468,6 +5468,30 @@
end if;
end if;
+ -- If the SPARK_05 restriction is active, we are not allowed
+ -- to have a call to a subprogram before we see its completion.
+
+ if not Has_Completion (Nam)
+ and then Restriction_Check_Required (SPARK_05)
+
+ -- Don't flag strange internal calls
+
+ and then Comes_From_Source (N)
+ and then Comes_From_Source (Nam)
+
+ -- Only flag calls in extended main source
+
+ and then In_Extended_Main_Source_Unit (Nam)
+ and then In_Extended_Main_Source_Unit (N)
+
+ -- Exclude enumeration literals from this processing
+
+ and then Ekind (Nam) /= E_Enumeration_Literal
+ then
+ Check_SPARK_Restriction
+ ("call to subprogram cannot appear before its body", N);
+ end if;
+
-- Check that this is not a call to a protected procedure or entry from
-- within a protected function.
Index: restrict.adb
===================================================================
--- restrict.adb (revision 206918)
+++ restrict.adb (working copy)
@@ -625,8 +625,12 @@
begin
-- Ignore call if node U is not in the main source unit. This avoids
-- cascaded errors, e.g. when Ada.Containers units with other units.
+ -- However, allow Standard_Location here, since this catches some cases
+ -- of constructs that get converted to run-time calls.
- if not In_Extended_Main_Source_Unit (U) then
+ if not In_Extended_Main_Source_Unit (U)
+ and then Sloc (U) /= Standard_Location
+ then
return;
end if;
