diff mbox

[Ada] Force instantiation of subprogram body in SPARK mode

Message ID 20130705102529.GA29290@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet July 5, 2013, 10:25 a.m. UTC 
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  <moy@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.
diff mbox

Patch

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)