[multiple changes]
2011-08-04 Yannick Moy <moy@adacore.com> * 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 <kirtchev@adacore.com> * exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate Finalize_Address when CodePeer is enabled. 2011-08-04 Pascal Obry <obry@adacore.com> * 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
This commit is contained in:
parent
5c0e97dd35
commit
9534ab171e
|
@ -1,3 +1,32 @@
|
|||
2011-08-04 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* 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 <kirtchev@adacore.com>
|
||||
|
||||
* exp_ch3.adb (Expand_Freeze_Class_Wide_Type): Do not generate
|
||||
Finalize_Address when CodePeer is enabled.
|
||||
|
||||
2011-08-04 Pascal Obry <obry@adacore.com>
|
||||
|
||||
* 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 <moy@adacore.com>
|
||||
|
||||
* sem_ch3.adb (Array_Type_Declaration): move test for type in ALFA
|
||||
|
|
|
@ -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 */
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 \
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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)));
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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 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.
|
||||
-- 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.
|
||||
|
||||
-- This comment just says what is done, but not why ??? and it
|
||||
-- just repeats what is in the spec ???
|
||||
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, because neither the
|
||||
-- subprogram nor its callers can be proved formally.
|
||||
|
||||
-- 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);
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 + $;
|
||||
|
|
Loading…
Reference in New Issue