===================================================================
@@ -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;
===================================================================
@@ -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
===================================================================
@@ -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.
===================================================================
@@ -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;
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 <dewar@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.