From 9534ab171e71fa56c4b384c5984d0d457f2eb55d Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 4 Aug 2011 10:18:13 +0200 Subject: [PATCH] [multiple changes] 2011-08-04 Yannick Moy * einfo.adb, einfo.ads (Formal_Proof_On): new flag set on subprogram entities whose body contains an Annotate pragma which forces formal proof on this body. * sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch9.adb, sem_res.adb: Adapt call to Mark_Non_ALFA_Subprogram to pass in a message and node. * sem_prag.adb (Analyze_Pragma): add treatment of pragma Annotate (Forma_Proof, On) which sets the flag Formal_Proof_On in the surrounding subprogram. * sem_util.adb, sem_util.ads (Mark_Non_ALFA_Subprogram, Mark_Non_ALFA_Subprogram_Unconditional): if the subprogram being marked as not in ALFA is annotated with Formal_Proof being On, then an error is issued based on the additional parameters for message and node. * snames.ads-tmpl (Name_Formal_Proof): new name for annotation. * gcc-interface/Make-lang.in: Update dependencies. 2011-08-04 Hristian Kirtchev * exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate Finalize_Address when CodePeer is enabled. 2011-08-04 Pascal Obry * adaint.c (__gnat_tmp_name): Use _tempnam() instead of tempnam() as the latter returns a pointer to a static buffer which is deallocated at the end of the routine. From-SVN: r177328 --- gcc/ada/ChangeLog | 29 +++++++++++ gcc/ada/adaint.c | 2 +- gcc/ada/einfo.adb | 15 +++++- gcc/ada/einfo.ads | 8 ++++ gcc/ada/exp_ch3.adb | 18 ++++--- gcc/ada/gcc-interface/Make-lang.in | 77 +++++++++++++++++------------- gcc/ada/sem_ch11.adb | 2 +- gcc/ada/sem_ch2.adb | 2 +- gcc/ada/sem_ch3.adb | 8 ++-- gcc/ada/sem_ch4.adb | 35 +++++++------- gcc/ada/sem_ch5.adb | 27 +++++++---- gcc/ada/sem_ch6.adb | 7 +-- gcc/ada/sem_ch9.adb | 52 ++++++++++---------- gcc/ada/sem_prag.adb | 47 ++++++++++++++++++ gcc/ada/sem_res.adb | 15 ++++-- gcc/ada/sem_util.adb | 35 ++++++++++---- gcc/ada/sem_util.ads | 25 ++++++---- gcc/ada/snames.ads-tmpl | 1 + 18 files changed, 282 insertions(+), 123 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index aa77d3df316..09f342334e1 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2011-08-04 Yannick Moy + + * einfo.adb, einfo.ads (Formal_Proof_On): new flag set on subprogram + entities whose body contains an Annotate pragma which forces formal + proof on this body. + * sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, + sem_ch6.adb, sem_ch9.adb, sem_res.adb: Adapt call to + Mark_Non_ALFA_Subprogram to pass in a message and node. + * sem_prag.adb (Analyze_Pragma): add treatment of pragma Annotate + (Forma_Proof, On) which sets the flag Formal_Proof_On in the + surrounding subprogram. + * sem_util.adb, sem_util.ads (Mark_Non_ALFA_Subprogram, + Mark_Non_ALFA_Subprogram_Unconditional): if the subprogram being marked + as not in ALFA is annotated with Formal_Proof being On, then an error + is issued based on the additional parameters for message and node. + * snames.ads-tmpl (Name_Formal_Proof): new name for annotation. + * gcc-interface/Make-lang.in: Update dependencies. + +2011-08-04 Hristian Kirtchev + + * exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate + Finalize_Address when CodePeer is enabled. + +2011-08-04 Pascal Obry + + * adaint.c (__gnat_tmp_name): Use _tempnam() instead of tempnam() as + the latter returns a pointer to a static buffer which is deallocated + at the end of the routine. + 2011-08-04 Yannick Moy * sem_ch3.adb (Array_Type_Declaration): move test for type in ALFA diff --git a/gcc/ada/adaint.c b/gcc/ada/adaint.c index 3d4c50a979c..b0fd8c590ec 100644 --- a/gcc/ada/adaint.c +++ b/gcc/ada/adaint.c @@ -1183,7 +1183,7 @@ __gnat_tmp_name (char *tmp_filename) directory specified by P_tmpdir in stdio.h if c:\temp does not exist. The filename will be created with the prefix "gnat-". */ - pname = (char *) tempnam ("c:\\temp", "gnat-"); + pname = (char *) _tempnam ("c:\\temp", "gnat-"); /* if pname is NULL, the file was not created properly, the disk is full or there is no more free temporary files */ diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index e1b63f03d77..be0081684dc 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -522,7 +522,7 @@ package body Einfo is -- Body_Is_In_ALFA Flag251 -- Is_Processed_Transient Flag252 -- Is_Postcondition_Proc Flag253 - -- (unused) Flag254 + -- Formal_Proof_On Flag254 ----------------------- -- Local subprograms -- @@ -1126,6 +1126,12 @@ package body Einfo is return Node6 (Id); end First_Rep_Item; + function Formal_Proof_On (Id : E) return B is + begin + pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); + return Flag254 (Id); + end Formal_Proof_On; + function Freeze_Node (Id : E) return N is begin return Node7 (Id); @@ -3606,6 +3612,12 @@ package body Einfo is Set_Uint10 (Id, UI_From_Int (F'Pos (V))); end Set_Float_Rep; + procedure Set_Formal_Proof_On (Id : E; V : B := True) is + begin + pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); + Set_Flag254 (Id, V); + end Set_Formal_Proof_On; + procedure Set_Freeze_Node (Id : E; V : N) is begin Set_Node7 (Id, V); @@ -7430,6 +7442,7 @@ package body Einfo is W ("Entry_Accepted", Flag152 (Id)); W ("Can_Use_Internal_Rep", Flag229 (Id)); W ("Finalize_Storage_Only", Flag158 (Id)); + W ("Formal_Proof_On", Flag254 (Id)); W ("From_With_Type", Flag159 (Id)); W ("Has_Aliased_Components", Flag135 (Id)); W ("Has_Alignment_Clause", Flag46 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 9a96e8c8d95..10f7c78f30d 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1272,6 +1272,10 @@ package Einfo is -- Float_Rep_Kind. Together with the Digits_Value uniquely defines -- the floating-point representation to be used. +-- Formal_Proof_On (Flag254) +-- Present in subprogram entities. Set for subprograms whose body +-- contains an Annotate pragma which forces formal proof on this body. + -- Freeze_Node (Node7) -- Present in all entities. If there is an associated freeze node for -- the entity, this field references this freeze node. If no freeze @@ -6068,6 +6072,7 @@ package Einfo is function First_Private_Entity (Id : E) return E; function First_Rep_Item (Id : E) return N; function Float_Rep (Id : E) return F; + function Formal_Proof_On (Id : E) return B; function Freeze_Node (Id : E) return N; function From_With_Type (Id : E) return B; function Full_View (Id : E) return E; @@ -6657,6 +6662,7 @@ package Einfo is procedure Set_First_Private_Entity (Id : E; V : E); procedure Set_First_Rep_Item (Id : E; V : N); procedure Set_Float_Rep (Id : E; V : F); + procedure Set_Formal_Proof_On (Id : E; V : B := True); procedure Set_Freeze_Node (Id : E; V : N); procedure Set_From_With_Type (Id : E; V : B := True); procedure Set_Full_View (Id : E; V : E); @@ -7354,6 +7360,7 @@ package Einfo is pragma Inline (First_Optional_Parameter); pragma Inline (First_Private_Entity); pragma Inline (First_Rep_Item); + pragma Inline (Formal_Proof_On); pragma Inline (Freeze_Node); pragma Inline (From_With_Type); pragma Inline (Full_View); @@ -7798,6 +7805,7 @@ package Einfo is pragma Inline (Set_First_Optional_Parameter); pragma Inline (Set_First_Private_Entity); pragma Inline (Set_First_Rep_Item); + pragma Inline (Set_Formal_Proof_On); pragma Inline (Set_Freeze_Node); pragma Inline (Set_From_With_Type); pragma Inline (Set_Full_View); diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index 0e409466083..a5038a992a6 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -5576,6 +5576,12 @@ package body Exp_Ch3 is if Restriction_Active (No_Finalization) then return; + -- Do not create TSS routine Finalize_Address when dispatching calls are + -- disabled since the core of the routine is a dispatching call. + + elsif Restriction_Active (No_Dispatching_Calls) then + return; + -- Do not create TSS routine Finalize_Address for concurrent class-wide -- types. Ignore C, C++, CIL and Java types since it is assumed that the -- non-Ada side will handle their destruction. @@ -5588,17 +5594,17 @@ package body Exp_Ch3 is then return; - -- Do not create TSS routine Finalize_Address when dispatching calls are - -- disabled since the core of the routine is a dispatching call. - - elsif Restriction_Active (No_Dispatching_Calls) then - return; - -- Do not create TSS routine Finalize_Address for .NET/JVM because these -- targets do not support address arithmetic and unchecked conversions. elsif VM_Target /= No_VM then return; + + -- Do not create TSS routine Finalize_Address when compiling in CodePeer + -- mode since the routine contains an Unchecked_Conversion. + + elsif CodePeer_Mode then + return; end if; -- Generate the body of Finalize_Address. This routine is accessible diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index c418482aff0..1f119ee6fcc 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -1297,16 +1297,20 @@ ada/a-ioexce.o : ada/ada.ads ada/a-except.ads ada/a-ioexce.ads \ ada/ada.o : ada/ada.ads ada/system.ads ada/alfa.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ - ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads ada/atree.ads \ - ada/einfo.ads ada/snames.ads ada/interfac.ads ada/namet.ads \ - ada/s-conca2.ads ada/sinfo.ads ada/table.ads ada/uintp.ads \ - ada/urealp.ads ada/gnat.ads ada/g-table.ads \ - ada/g-table.adb ada/hostparm.ads ada/output.ads ada/output.adb \ - ada/put_alfa.ads ada/put_alfa.adb ada/system.ads ada/s-exctab.ads \ - ada/s-memory.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-soflin.ads \ - ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads ada/s-stoele.adb \ - ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads ada/types.ads \ - ada/unchconv.ads ada/unchdeal.ads + ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads \ + ada/aspects.ads ada/atree.ads ada/atree.adb ada/casing.ads \ + ada/debug.ads ada/einfo.ads ada/gnat.ads ada/g-htable.ads \ + ada/g-table.ads ada/g-table.adb ada/hostparm.ads ada/interfac.ads \ + ada/namet.ads ada/namet.adb ada/nlists.ads ada/nlists.adb ada/opt.ads \ + ada/output.ads ada/output.adb ada/put_alfa.ads ada/put_alfa.adb \ + ada/sinfo.ads ada/sinfo.adb ada/sinput.ads ada/snames.ads \ + ada/system.ads ada/s-exctab.ads ada/s-htable.ads ada/s-imenne.ads \ + ada/s-memory.ads ada/s-os_lib.ads ada/s-parame.ads ada/s-secsta.ads \ + ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \ + ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \ + ada/s-wchcon.ads ada/table.ads ada/table.adb ada/tree_io.ads \ + ada/types.ads ada/uintp.ads ada/uintp.adb ada/unchconv.ads \ + ada/unchdeal.ads ada/urealp.ads ada/widechar.ads ada/ali-util.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/a-uncdea.ads ada/ali.ads ada/ali.adb ada/ali-util.ads \ @@ -2094,16 +2098,15 @@ ada/exp_ch7.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/sem_ch8.ads ada/sem_ch9.ads ada/sem_dist.ads ada/sem_eval.ads \ ada/sem_prag.ads ada/sem_res.ads ada/sem_type.ads ada/sem_util.ads \ ada/sinfo.ads ada/sinfo.adb ada/sinput.ads ada/snames.ads ada/stand.ads \ - ada/stringt.ads ada/stringt.adb ada/stylesw.ads ada/system.ads \ - ada/s-exctab.ads ada/s-htable.ads ada/s-imenne.ads ada/s-memory.ads \ - ada/s-os_lib.ads ada/s-parame.ads ada/s-rident.ads ada/s-secsta.ads \ - ada/s-soflin.ads ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads \ - ada/s-stoele.adb ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads \ - ada/s-wchcon.ads ada/table.ads ada/table.adb ada/targparm.ads \ - ada/tbuild.ads ada/tbuild.adb ada/tree_io.ads ada/ttypes.ads \ - ada/types.ads ada/uintp.ads ada/uintp.adb ada/uname.ads \ - ada/unchconv.ads ada/unchdeal.ads ada/urealp.ads ada/validsw.ads \ - ada/widechar.ads + ada/stringt.ads ada/stylesw.ads ada/system.ads ada/s-exctab.ads \ + ada/s-htable.ads ada/s-imenne.ads ada/s-memory.ads ada/s-os_lib.ads \ + ada/s-parame.ads ada/s-rident.ads ada/s-secsta.ads ada/s-soflin.ads \ + ada/s-stache.ads ada/s-stalib.ads ada/s-stoele.ads ada/s-stoele.adb \ + ada/s-string.ads ada/s-traent.ads ada/s-unstyp.ads ada/s-wchcon.ads \ + ada/table.ads ada/table.adb ada/targparm.ads ada/tbuild.ads \ + ada/tbuild.adb ada/tree_io.ads ada/ttypes.ads ada/types.ads \ + ada/uintp.ads ada/uintp.adb ada/uname.ads ada/unchconv.ads \ + ada/unchdeal.ads ada/urealp.ads ada/validsw.ads ada/widechar.ads ada/exp_ch8.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/a-uncdea.ads ada/alloc.ads ada/aspects.ads ada/atree.ads \ @@ -2745,13 +2748,17 @@ ada/g-u3spch.o : ada/gnat.ads ada/g-spchge.ads ada/g-spchge.adb \ ada/g-u3spch.ads ada/g-u3spch.adb ada/system.ads ada/s-wchcnv.ads \ ada/s-wchcon.ads -ada/get_alfa.o : ada/ada.ads ada/a-ioexce.ads ada/a-unccon.ads \ - ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/get_alfa.ads \ - ada/get_alfa.adb ada/gnat.ads ada/g-table.ads ada/g-table.adb \ - ada/hostparm.ads ada/output.ads ada/put_alfa.ads ada/system.ads \ - ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads ada/s-stalib.ads \ - ada/s-string.ads ada/s-unstyp.ads ada/types.ads ada/unchconv.ads \ - ada/unchdeal.ads +ada/get_alfa.o : ada/ada.ads ada/a-except.ads ada/a-ioexce.ads \ + ada/a-unccon.ads ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb \ + ada/alloc.ads ada/atree.ads ada/debug.ads ada/einfo.ads \ + ada/get_alfa.ads ada/get_alfa.adb ada/gnat.ads ada/g-table.ads \ + ada/g-table.adb ada/hostparm.ads ada/namet.ads ada/opt.ads \ + ada/output.ads ada/put_alfa.ads ada/sinfo.ads ada/snames.ads \ + ada/system.ads ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads \ + ada/s-parame.ads ada/s-stalib.ads ada/s-string.ads ada/s-traent.ads \ + ada/s-unstyp.ads ada/s-wchcon.ads ada/table.ads ada/table.adb \ + ada/tree_io.ads ada/types.ads ada/uintp.ads ada/unchconv.ads \ + ada/unchdeal.ads ada/urealp.ads ada/get_scos.o : ada/ada.ads ada/a-ioexce.ads ada/a-unccon.ads \ ada/get_scos.ads ada/get_scos.adb ada/gnat.ads ada/g-table.ads \ @@ -3303,12 +3310,16 @@ ada/prepcomp.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ ada/uintp.adb ada/uname.ads ada/unchconv.ads ada/unchdeal.ads \ ada/urealp.ads ada/widechar.ads -ada/put_alfa.o : ada/ada.ads ada/a-unccon.ads ada/a-uncdea.ads \ - ada/alfa.ads ada/alfa.adb ada/gnat.ads ada/g-table.ads ada/g-table.adb \ - ada/hostparm.ads ada/output.ads ada/put_alfa.ads ada/put_alfa.adb \ - ada/system.ads ada/s-exctab.ads ada/s-memory.ads ada/s-os_lib.ads \ - ada/s-stalib.ads ada/s-string.ads ada/s-unstyp.ads ada/types.ads \ - ada/unchconv.ads ada/unchdeal.ads +ada/put_alfa.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \ + ada/a-uncdea.ads ada/alfa.ads ada/alfa.adb ada/alloc.ads ada/atree.ads \ + ada/debug.ads ada/einfo.ads ada/gnat.ads ada/g-table.ads \ + ada/g-table.adb ada/hostparm.ads ada/namet.ads ada/opt.ads \ + ada/output.ads ada/put_alfa.ads ada/put_alfa.adb ada/sinfo.ads \ + ada/snames.ads ada/system.ads ada/s-exctab.ads ada/s-memory.ads \ + ada/s-os_lib.ads ada/s-parame.ads ada/s-stalib.ads ada/s-string.ads \ + ada/s-traent.ads ada/s-unstyp.ads ada/s-wchcon.ads ada/table.ads \ + ada/table.adb ada/tree_io.ads ada/types.ads ada/uintp.ads \ + ada/unchconv.ads ada/unchdeal.ads ada/urealp.ads ada/put_scos.o : ada/ada.ads ada/a-unccon.ads ada/gnat.ads ada/g-table.ads \ ada/g-table.adb ada/put_scos.ads ada/put_scos.adb ada/scos.ads \ diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 68f3d17225f..4ae09e1d14e 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -434,7 +434,7 @@ package body Sem_Ch11 is P : Node_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("raise statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("raise statement is not allowed", N); Check_Unreachable_Code (N); diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb index f2c915b06aa..d6db4d96bef 100644 --- a/gcc/ada/sem_ch2.adb +++ b/gcc/ada/sem_ch2.adb @@ -81,7 +81,7 @@ package body Sem_Ch2 is and then Is_Object (Entity (N)) and then not Is_In_ALFA (Entity (N)) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("object is not in 'A'L'F'A", N); end if; end if; end Analyze_Identifier; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 081b7fa10b0..401436db2b8 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3052,10 +3052,12 @@ package body Sem_Ch3 is -- The object is in ALFA if-and-only-if its type is in ALFA and it is -- not aliased. - if Is_In_ALFA (T) and then not Aliased_Present (N) then - Set_Is_In_ALFA (Id); + if not Is_In_ALFA (T) then + Mark_Non_ALFA_Subprogram ("object type is not in 'A'L'F'A", N); + elsif Aliased_Present (N) then + Mark_Non_ALFA_Subprogram ("ALIASED is not in 'A'L'F'A", N); else - Mark_Non_ALFA_Subprogram; + Set_Is_In_ALFA (Id); end if; -- These checks should be performed before the initialization expression diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index e04773a1a44..44cda4092be 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -350,7 +350,7 @@ package body Sem_Ch4 is procedure Analyze_Aggregate (N : Node_Id) is begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("aggregate is not in 'A'L'F'A", N); if No (Etype (N)) then Set_Etype (N, Any_Composite); @@ -371,7 +371,7 @@ package body Sem_Ch4 is C : Node_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("allocator is not in 'A'L'F'A", N); Check_SPARK_Restriction ("allocator is not allowed", N); -- Deal with allocator restrictions @@ -988,10 +988,10 @@ package body Sem_Ch4 is -- If this is an indirect call, or the subprogram called is not in -- ALFA, then the call is not in ALFA. - if not Is_Subprogram (Nam_Ent) - or else not Is_In_ALFA (Nam_Ent) - then - Mark_Non_ALFA_Subprogram; + if not Is_Subprogram (Nam_Ent) then + Mark_Non_ALFA_Subprogram ("indirect call is not in 'A'L'F'A", N); + elsif not Is_In_ALFA (Nam_Ent) then + Mark_Non_ALFA_Subprogram ("call to subprogram not in 'A'L'F'A", N); end if; Analyze_One_Call (N, Nam_Ent, True, Success); @@ -1370,7 +1370,7 @@ package body Sem_Ch4 is L : Node_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("concatenation is not in 'A'L'F'A", N); Candidate_Type := Empty; @@ -1540,7 +1540,8 @@ package body Sem_Ch4 is -- resolution. if Present (Else_Expr) and then not In_Pre_Post_Expression then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("this form of conditional expression is not in 'A'L'F'A", N); end if; if Comes_From_Source (N) then @@ -1739,7 +1740,7 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Explicit_Dereference begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("explicit dereference is not in 'A'L'F'A", N); Check_SPARK_Restriction ("explicit dereference is not allowed", N); Analyze (P); @@ -2622,7 +2623,7 @@ package body Sem_Ch4 is procedure Analyze_Null (N : Node_Id) is begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("null is not in 'A'L'F'A", N); Check_SPARK_Restriction ("null is not allowed", N); Set_Etype (N, Any_Access); @@ -3254,7 +3255,7 @@ package body Sem_Ch4 is T : Entity_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("qualified expression is not in 'A'L'F'A", N); Analyze_Expression (Expr); @@ -3314,7 +3315,7 @@ package body Sem_Ch4 is Iterator : Node_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("quantified expression is not in 'A'L'F'A", N); Check_SPARK_Restriction ("quantified expression is not allowed", N); Set_Etype (Ent, Standard_Void_Type); @@ -3480,7 +3481,7 @@ package body Sem_Ch4 is Acc_Type : Entity_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("reference is not in 'A'L'F'A", N); Analyze (P); @@ -4346,7 +4347,7 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Slice begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("slice is not in 'A'L'F'A", N); Check_SPARK_Restriction ("slice is not allowed", N); Analyze (P); @@ -4416,7 +4417,8 @@ package body Sem_Ch4 is -- type conversions are not allowed. if not (Is_Scalar_Type (Etype (Expr)) and then Is_Scalar_Type (T)) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("only type conversion between scalar types is in 'A'L'F'A", N); end if; -- Only remaining step is validity checks on the argument. These @@ -4528,7 +4530,8 @@ package body Sem_Ch4 is procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("unchecked type conversion is not in 'A'L'F'A", N); Find_Type (Subtype_Mark (N)); Analyze_Expression (Expression (N)); Set_Etype (N, Entity (Subtype_Mark (N))); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 239f9fe35bf..b9c03c02932 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1113,7 +1113,8 @@ package body Sem_Ch5 is if Others_Present and then List_Length (Alternatives (N)) = 1 then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("OTHERS as unique case alternative is not in 'A'L'F'A", N); Check_SPARK_Restriction ("OTHERS as unique case alternative is not allowed", N); end if; @@ -1195,7 +1196,9 @@ package body Sem_Ch5 is else if Has_Loop_In_Inner_Open_Scopes (U_Name) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("exit label must name the closest enclosing loop" + & " in 'A'L'F'A", N); Check_SPARK_Restriction ("exit label must name the closest enclosing loop", N); end if; @@ -1242,23 +1245,29 @@ package body Sem_Ch5 is if Present (Cond) then if Nkind (Parent (N)) /= N_Loop_Statement then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("exit with when clause must be directly in loop" + & " in 'A'L'F'A", N); Check_SPARK_Restriction ("exit with when clause must be directly in loop", N); end if; else if Nkind (Parent (N)) /= N_If_Statement then - Mark_Non_ALFA_Subprogram; if Nkind (Parent (N)) = N_Elsif_Part then + Mark_Non_ALFA_Subprogram + ("exit must be in IF without ELSIF in 'A'L'F'A", N); Check_SPARK_Restriction ("exit must be in IF without ELSIF", N); else + Mark_Non_ALFA_Subprogram + ("exit must be directly in IF in 'A'L'F'A", N); Check_SPARK_Restriction ("exit must be directly in IF", N); end if; elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("exit must be in IF directly in loop in 'A'L'F'A", N); Check_SPARK_Restriction ("exit must be in IF directly in loop", N); @@ -1266,14 +1275,16 @@ package body Sem_Ch5 is -- leads to an error mentioning the ELSE. elsif Present (Else_Statements (Parent (N))) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("exit must be in IF without ELSE in 'A'L'F'A", N); Check_SPARK_Restriction ("exit must be in IF without ELSE", N); -- An exit in an ELSIF does not reach here, as it would have been -- detected in the case (Nkind (Parent (N)) /= N_If_Statement). elsif Present (Elsif_Parts (Parent (N))) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("exit must be in IF without ELSIF in 'A'L'F'A", N); Check_SPARK_Restriction ("exit must be in IF without ELSIF", N); end if; end if; @@ -1302,7 +1313,7 @@ package body Sem_Ch5 is Label_Ent : Entity_Id; begin - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("goto statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("goto statement is not allowed", N); -- Actual semantic checks diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 854810f1562..4eaaaa6ab9b 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -649,13 +649,14 @@ package body Sem_Ch6 is (Nkind (Parent (Parent (N))) /= N_Subprogram_Body or else Present (Next (N))) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("RETURN should be the last statement in 'A'L'F'A", N); Check_SPARK_Restriction ("RETURN should be the last statement in function", N); end if; else - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("extended RETURN is not in 'A'L'F'A", N); Check_SPARK_Restriction ("extended RETURN is not allowed", N); -- Analyze parts specific to extended_return_statement: @@ -8886,7 +8887,7 @@ package body Sem_Ch6 is if Is_In_ALFA (Formal_Type) then Set_Is_In_ALFA (Formal); else - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("formal is not in 'A'L'F'A", Formal); end if; Default := Expression (Param_Spec); diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index f535f7e331d..204ecadd02a 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -101,7 +101,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("abort statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("abort statement is not allowed", N); T_Name := First (Names (N)); @@ -140,7 +140,7 @@ package body Sem_Ch9 is procedure Analyze_Accept_Alternative (N : Node_Id) is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("accept is not in 'A'L'F'A", N); if Present (Pragmas_Before (N)) then Analyze_List (Pragmas_Before (N)); @@ -174,7 +174,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("accept statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("accept statement is not allowed", N); -- Entry name is initialized to Any_Id. It should get reset to the @@ -406,7 +406,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (Max_Asynchronous_Select_Nesting, N); Check_Restriction (No_Select_Statements, N); @@ -453,7 +453,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); @@ -500,7 +500,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("delay is not in 'A'L'F'A", N); Check_Restriction (No_Delay, N); if Present (Pragmas_Before (N)) then @@ -552,7 +552,7 @@ package body Sem_Ch9 is E : constant Node_Id := Expression (N); begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("delay statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Relative_Delay, N); Check_Restriction (No_Delay, N); @@ -571,7 +571,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("delay statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Delay, N); Check_Potentially_Blocking_Operation (N); @@ -600,7 +600,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N); -- Entry_Name is initialized to Any_Id. It should get reset to the -- matching entry entity. An error is signalled if it is not reset @@ -833,7 +833,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N); if Present (Index) then Analyze (Index); @@ -861,7 +861,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("entry call is not in 'A'L'F'A", N); Check_SPARK_Restriction ("entry call is not allowed", N); if Present (Pragmas_Before (N)) then @@ -897,7 +897,7 @@ package body Sem_Ch9 is begin Generate_Definition (Def_Id); Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N); -- Case of no discrete subtype definition @@ -967,7 +967,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("entry is not in 'A'L'F'A", N); Analyze (Def); -- There is no elaboration of the entry index specification. Therefore, @@ -1009,7 +1009,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("protected body is not in 'A'L'F'A", N); Set_Ekind (Body_Id, E_Protected_Body); Spec_Id := Find_Concurrent_Spec (Body_Id); @@ -1128,7 +1128,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("protected definition is not in 'A'L'F'A", N); Check_SPARK_Restriction ("protected definition is not allowed", N); Analyze_Declarations (Visible_Declarations (N)); @@ -1182,7 +1182,7 @@ package body Sem_Ch9 is end if; Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("protected type is not in 'A'L'F'A", N); Check_Restriction (No_Protected_Types, N); T := Find_Type_Name (N); @@ -1324,7 +1324,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("requeue statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("requeue statement is not allowed", N); Check_Restriction (No_Requeue_Statements, N); Check_Unreachable_Code (N); @@ -1599,7 +1599,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); @@ -1720,7 +1720,7 @@ package body Sem_Ch9 is begin Generate_Definition (Id); Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("protected object is not in 'A'L'F'A", N); -- The node is rewritten as a protected type declaration, in exact -- analogy with what is done with single tasks. @@ -1782,7 +1782,7 @@ package body Sem_Ch9 is begin Generate_Definition (Id); Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("task is not in 'A'L'F'A", N); -- The node is rewritten as a task type declaration, followed by an -- object declaration of that anonymous task type. @@ -1860,7 +1860,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("task body is not in 'A'L'F'A", N); Set_Ekind (Body_Id, E_Task_Body); Set_Scope (Body_Id, Current_Scope); Spec_Id := Find_Concurrent_Spec (Body_Id); @@ -1981,7 +1981,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("task definition is not in 'A'L'F'A", N); Check_SPARK_Restriction ("task definition is not allowed", N); if Present (Visible_Declarations (N)) then @@ -2016,7 +2016,7 @@ package body Sem_Ch9 is begin Check_Restriction (No_Tasking, N); Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("task type is not in 'A'L'F'A", N); T := Find_Type_Name (N); Generate_Definition (T); @@ -2122,7 +2122,7 @@ package body Sem_Ch9 is procedure Analyze_Terminate_Alternative (N : Node_Id) is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("terminate is not in 'A'L'F'A", N); if Present (Pragmas_Before (N)) then Analyze_List (Pragmas_Before (N)); @@ -2144,7 +2144,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("select statement is not in 'A'L'F'A", N); Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); @@ -2181,7 +2181,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram ("triggering statement is not in 'A'L'F'A", N); if Present (Pragmas_Before (N)) then Analyze_List (Pragmas_Before (N)); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 4ce7ec5a61a..e9923157b14 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6103,6 +6103,53 @@ package body Sem_Prag is Exp : Node_Id; begin + if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then + if No (Arg2) then + Error_Pragma_Arg + ("missing second argument for pragma%", Arg1); + end if; + + Check_Arg_Is_Identifier (Arg2); + Check_Arg_Count (2); + + if Chars (Get_Pragma_Arg (Arg2)) /= Name_On + and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off + then + Error_Pragma_Arg + ("wrong second argument for pragma%", Arg2); + end if; + + if Chars (Get_Pragma_Arg (Arg2)) = Name_On then + declare + Cur_Subp : constant Entity_Id := Current_Subprogram; + + begin + if Present (Cur_Subp) + and then (Is_Subprogram (Cur_Subp) + or else Is_Generic_Subprogram (Cur_Subp)) + then + -- Notify user if some ALFA violation occurred + -- before this point in Cur_Subp. These violations + -- are not precisly located, but this is better + -- than ignoring them. + + if not Is_In_ALFA (Cur_Subp) + or else not Body_Is_In_ALFA (Cur_Subp) + then + Error_Pragma + ("pragma% is placed after violation" + & " of 'A'L'F'A"); + end if; + + Set_Formal_Proof_On (Cur_Subp); + + else + Error_Pragma ("wrong placement for pragma%"); + end if; + end; + end if; + end if; + -- Second unanalyzed parameter is optional if No (Arg2) then diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 3286e3aa57c..241abd622aa 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5796,12 +5796,14 @@ package body Sem_Res is -- types or array types except String. if Is_Boolean_Type (T) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("ordering operator on boolean type is not in 'A'L'F'A", N); Check_SPARK_Restriction ("comparison is not defined on Boolean type", N); elsif Is_Array_Type (T) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("ordering operator on array type is not in 'A'L'F'A", N); if Base_Type (T) /= Standard_String then Check_SPARK_Restriction @@ -5861,7 +5863,8 @@ package body Sem_Res is end if; if Root_Type (Typ) /= Standard_Boolean then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("non-boolean conditional expression is not in 'A'L'F'A", N); end if; Set_Etype (N, Typ); @@ -6664,7 +6667,8 @@ package body Sem_Res is -- operands have equal static bounds. if Is_Array_Type (T) then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("equality operator on array is not in 'A'L'F'A", N); -- Protect call to Matching_Static_Array_Bounds to avoid costly -- operation if not needed. @@ -7214,7 +7218,8 @@ package body Sem_Res is if Is_Array_Type (B_Typ) and then Nkind (N) in N_Binary_Op then - Mark_Non_ALFA_Subprogram; + Mark_Non_ALFA_Subprogram + ("binary operator on array is not in 'A'L'F'A", N); declare Left_Typ : constant Node_Id := Etype (Left_Opnd (N)); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index e62d013e9ed..2a90f677811 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -141,9 +141,13 @@ package body Sem_Util is -- T is a derived tagged type. Check whether the type extension is null. -- If the parent type is fully initialized, T can be treated as such. - procedure Mark_Non_ALFA_Subprogram_Unconditional; + procedure Mark_Non_ALFA_Subprogram_Unconditional + (Msg : String; + N : Node_Id); -- Perform the action for Mark_Non_ALFA_Subprogram_Body, which allows the - -- latter to be small and inlined. + -- latter to be small and inlined. If the subprogram being marked as not in + -- ALFA is annotated with Formal_Proof being On, then an error is issued + -- with message Msg on node N. ------------------------------ -- Abstract_Interface_List -- @@ -2323,13 +2327,13 @@ package body Sem_Util is -- Mark_Non_ALFA_Subprogram -- ------------------------------ - procedure Mark_Non_ALFA_Subprogram is + procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id) is begin -- Isolate marking of the current subprogram body so that the body of -- Mark_Non_ALFA_Subprogram is small and inlined. if ALFA_Mode then - Mark_Non_ALFA_Subprogram_Unconditional; + Mark_Non_ALFA_Subprogram_Unconditional (Msg, N); end if; end Mark_Non_ALFA_Subprogram; @@ -2337,7 +2341,10 @@ package body Sem_Util is -- Mark_Non_ALFA_Subprogram_Unconditional -- -------------------------------------------- - procedure Mark_Non_ALFA_Subprogram_Unconditional is + procedure Mark_Non_ALFA_Subprogram_Unconditional + (Msg : String; + N : Node_Id) + is Cur_Subp : constant Entity_Id := Current_Subprogram; begin @@ -2345,12 +2352,22 @@ package body Sem_Util is and then (Is_Subprogram (Cur_Subp) or else Is_Generic_Subprogram (Cur_Subp)) then + -- If the subprogram has been annotated with Formal_Proof being On, + -- then an error must be issued to notify the user that this + -- subprogram unexpectedly falls outside the ALFA subset. + + if Formal_Proof_On (Cur_Subp) then + Error_Msg_F (Msg, N); + end if; + -- If the non-ALFA construct is in a precondition or postcondition, - -- then mark the subprogram as not in ALFA. Otherwise, mark the - -- subprogram body as not in ALFA. + -- then mark the subprogram as not in ALFA, because neither the + -- subprogram nor its callers can be proved formally. - -- This comment just says what is done, but not why ??? and it - -- just repeats what is in the spec ??? + -- If the non-ALFA construct is in a regular piece of code inside the + -- body of the subprogram, then mark the subprogram body as not in + -- ALFA, because the subprogram cannot be proved formally, but its + -- callers could. if In_Pre_Post_Expression then Set_Is_In_ALFA (Cur_Subp, False); diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index d50dc5f7037..e8773a44a28 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -277,17 +277,22 @@ package Sem_Util is -- Current_Scope is returned. The returned value is Empty if this is called -- from a library package which is not within any subprogram. - procedure Mark_Non_ALFA_Subprogram; + procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id); -- If Current_Subprogram is not Empty, mark either its specification or its - -- body as not being in ALFA. This procedure may be called during the - -- analysis of a precondition or postcondition, as indicated by the flag - -- In_Pre_Post_Expression, or during the analysis of a subprogram's body. - -- In the first case, the specification of Current_Subprogram must be - -- marked as not being in ALFA, as the contract is considered to be part of - -- the specification, so that calls to this subprogram are not in ALFA. In - -- the second case, mark the body as not being in ALFA, which does not - -- prevent the subprogram's specification, and calls to the subprogram, - -- from being in ALFA. + -- body as not being in ALFA. + + -- This procedure may be called during the analysis of a precondition or + -- postcondition, as indicated by the flag In_Pre_Post_Expression, or + -- during the analysis of a subprogram's body. In the first case, the + -- specification of Current_Subprogram must be marked as not being in ALFA, + -- as the contract is considered to be part of the specification, so that + -- calls to this subprogram are not in ALFA. In the second case, mark the + -- body as not being in ALFA, which does not prevent the subprogram's + -- specification, and calls to the subprogram, from being in ALFA. + + -- If the subprogram being marked as not in ALFA is annotated with + -- Formal_Proof being On, then an error is issued with message Msg on node + -- N. function Defining_Entity (N : Node_Id) return Entity_Id; -- Given a declaration N, returns the associated defining entity. If the diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 818cc8b6708..c3c7bead3b6 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -629,6 +629,7 @@ package Snames is Name_External_Name : constant Name_Id := N + $; Name_First_Optional_Parameter : constant Name_Id := N + $; Name_Form : constant Name_Id := N + $; + Name_Formal_Proof : constant Name_Id := N + $; Name_G_Float : constant Name_Id := N + $; Name_Gcc : constant Name_Id := N + $; Name_Gnat : constant Name_Id := N + $; -- 2.30.2