From 3cc0fae4334466cc8da40e454455b08e83c9e932 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 4 Jul 2019 08:06:45 +0000 Subject: [PATCH] [Ada] SPARK_Mode Off now allowed inside subprogram The rule on SPARK_Mode have been modified so that it is now possible to have a subprogram or package declared with SPARK_Mode Off inside a subprogram. 2019-07-04 Yannick Moy gcc/ada/ * sem_prag.adb (Check_Library_Level_Entity): Update for new rule on SPARK_Mode. gcc/testsuite/ * gnat.dg/spark3.adb: New testcase. From-SVN: r273064 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_prag.adb | 11 ++++++++++- gcc/testsuite/ChangeLog | 4 ++++ gcc/testsuite/gnat.dg/spark3.adb | 20 ++++++++++++++++++++ 4 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 gcc/testsuite/gnat.dg/spark3.adb diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e476413..f5c2927 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-04 Yannick Moy + + * sem_prag.adb (Check_Library_Level_Entity): Update for new rule + on SPARK_Mode. + 2019-07-04 Justin Squirek * sem_disp.adb (Check_Controlling_Formals): Obtain the full view diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b499dbd..d841426 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23189,7 +23189,16 @@ package body Sem_Prag is -- Start of processing for Check_Library_Level_Entity begin - if not Is_Library_Level_Entity (E) then + -- A SPARK_Mode of On shall only apply to library-level + -- entities, except for those in generic instances, which are + -- ignored (even if the entity gets SPARK_Mode pragma attached + -- in the AST, its effect is not taken into account unless the + -- context already provides SPARK_Mode of On in GNATprove). + + if Get_SPARK_Mode_From_Annotation (N) = On + and then not Is_Library_Level_Entity (E) + and then Instantiation_Location (Sloc (N)) = No_Location + then Error_Msg_Name_1 := Pname; Error_Msg_N (Fix_Error (Msg_1), N); diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 6873356..3502e68 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2019-07-04 Yannick Moy + + * gnat.dg/spark3.adb: New testcase. + 2019-07-04 Justin Squirek * gnat.dg/tagged2.adb, gnat.dg/tagged2.ads: New testcase. diff --git a/gcc/testsuite/gnat.dg/spark3.adb b/gcc/testsuite/gnat.dg/spark3.adb new file mode 100644 index 0000000..3c9908a --- /dev/null +++ b/gcc/testsuite/gnat.dg/spark3.adb @@ -0,0 +1,20 @@ +-- { dg-do compile } + +procedure SPARK3 (X : in out Integer) with SPARK_Mode is + + procedure Q (X : in out Integer) with SPARK_Mode => Off is + begin + X := X + 1; + end Q; + + procedure R (X : in out Integer); + + procedure R (X : in out Integer) with SPARK_Mode => Off is + begin + Q (X); + end R; + +begin + R (X); + X := X + 1; +end SPARK3; -- 2.7.4