In the SPARK mode for formal verification, force the instantiation of a
subprogram body, so that the formal verification backend can analyze it.
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-07-05 Yannick Moy <m...@adacore.com>
* sem_ch12.ads, sem_ch12.adb (Need_Subprogram_Instance_Body): Force
instance of subprogram body in SPARK mode, by testing Expander_Active
(set in SPARK mode) instead of Full_Expander_Active (not set in
SPARK mode).
* sem_ch8.adb: Minor reformatting.
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb (revision 200695)
+++ sem_ch12.adb (working copy)
@@ -4367,13 +4367,17 @@
Subp : Entity_Id) return Boolean
is
begin
+ -- This complex conditional requires blow by blow comments ???
+
if (Is_In_Main_Unit (N)
or else Is_Inlined (Subp)
or else Is_Inlined (Alias (Subp)))
and then (Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then ASIS_Mode))
- and then (Full_Expander_Active or else ASIS_Mode)
+ -- The following line definitely requires comments, why do we
+ -- test Expander_Active and not Full_Expander_Active here ???
+ and then (Expander_Active or ASIS_Mode)
and then not ABE_Is_Certain (N)
and then not Is_Eliminated (Subp)
then
Index: sem_ch12.ads
===================================================================
--- sem_ch12.ads (revision 200688)
+++ sem_ch12.ads (working copy)
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -113,7 +113,6 @@
function Need_Subprogram_Instance_Body
(N : Node_Id;
Subp : Entity_Id) return Boolean;
-
-- If a subprogram instance is inlined, indicate that the body of it
-- must be created, to be used in inlined calls by the back-end. The
-- subprogram may be inlined because the generic itself carries the
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 200688)
+++ sem_ch8.adb (working copy)
@@ -2816,7 +2816,7 @@
-- The following is illegal, because F hides whatever other F may
-- be around:
- -- function F (..) renames F;
+ -- function F (...) renames F;
elsif Old_S = New_S
or else (Nkind (Nam) /= N_Expanded_Name
@@ -2824,6 +2824,10 @@
then
Error_Msg_N ("subprogram cannot rename itself", N);
+ -- This is illegal even if we use a selector:
+ -- function F (...) renames Pkg.F;
+ -- because F is still hidden.
+
elsif Nkind (Nam) = N_Expanded_Name
and then Entity (Prefix (Nam)) = Current_Scope
and then Chars (Selector_Name (Nam)) = Chars (New_S)
