[multiple changes]

2017-04-27  Gary Dismukes  <dismukes@adacore.com>

	* sem_ch4.adb: Minor reformatting.

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb (Analyze_Associations): minor reformatting.
	(Check_Fixed_Point_Actual): Do not emit a warning on a fixed
	point type actual that has user-defined arithmetic primitives,
	when there is a previous actual for a formal package that defines
	a fixed-point type with the parent user-defined operator.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* checks.adb (Generate_Range_Check): Reinstate part of previous change.
	* sem_attr.adb (Resolve_Attribute): Generate a range check when
	the component type allows range checks.

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_aux.adb (Is_Generic_Formal): Use original node to locate
	corresponding declaration, because formal derived types are
	rewritten as private extensions.

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_dim.adb (Analyze_Dimension_Binary_Op): Do not check
	dimensions of operands if node has been analyzed already, because
	previous analysis and dimension checking will have removed the
	dimension information from the operands.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* debug.adb: Document the use of switch -gnatd.s.
	* einfo.ads Update the documentation on attribute
	Sec_Stack_Needed_For_Return and attribute Uses_Sec_Stack. Remove
	the uses of these attributes from certain entities.
	* exp_ch7.adb (Make_Transient_Block): Reimplement the circuitry
	which determines whether the block should continue to manage
	the secondary stack.
	(Manages_Sec_Stack): New routine.

2017-04-27  Bob Duff  <duff@adacore.com>

	* atree.ads: Minor edit.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sinfo.ads: Update the section on Ghost mode. Add
	a section on SPARK mode. Update the placement of section on
	expression functions.

2017-04-27  Bob Duff  <duff@adacore.com>

	* sinput.adb (Get_Source_File_Index): Don't
	assert that S is in the right range in the case where this is
	a .dg file under construction.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Check_Result_And_Post_State):
	Handle more precisely each conjunct in expressions formed by
	and'ing sub-expressions.

From-SVN: r247295
This commit is contained in:
Arnaud Charlet 2017-04-27 10:51:18 +02:00
parent 0c3ef0cc2a
commit f32eb59134
14 changed files with 445 additions and 144 deletions

View File

@ -1,3 +1,67 @@
2017-04-27 Gary Dismukes <dismukes@adacore.com>
* sem_ch4.adb: Minor reformatting.
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* sem_ch12.adb (Analyze_Associations): minor reformatting.
(Check_Fixed_Point_Actual): Do not emit a warning on a fixed
point type actual that has user-defined arithmetic primitives,
when there is a previous actual for a formal package that defines
a fixed-point type with the parent user-defined operator.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* checks.adb (Generate_Range_Check): Reinstate part of previous change.
* sem_attr.adb (Resolve_Attribute): Generate a range check when
the component type allows range checks.
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* sem_aux.adb (Is_Generic_Formal): Use original node to locate
corresponding declaration, because formal derived types are
rewritten as private extensions.
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* sem_dim.adb (Analyze_Dimension_Binary_Op): Do not check
dimensions of operands if node has been analyzed already, because
previous analysis and dimension checking will have removed the
dimension information from the operands.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* debug.adb: Document the use of switch -gnatd.s.
* einfo.ads Update the documentation on attribute
Sec_Stack_Needed_For_Return and attribute Uses_Sec_Stack. Remove
the uses of these attributes from certain entities.
* exp_ch7.adb (Make_Transient_Block): Reimplement the circuitry
which determines whether the block should continue to manage
the secondary stack.
(Manages_Sec_Stack): New routine.
2017-04-27 Bob Duff <duff@adacore.com>
* atree.ads: Minor edit.
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* sinfo.ads: Update the section on Ghost mode. Add
a section on SPARK mode. Update the placement of section on
expression functions.
2017-04-27 Bob Duff <duff@adacore.com>
* sinput.adb (Get_Source_File_Index): Don't
assert that S is in the right range in the case where this is
a .dg file under construction.
2017-04-27 Yannick Moy <moy@adacore.com>
* sem_util.adb (Check_Result_And_Post_State):
Handle more precisely each conjunct in expressions formed by
and'ing sub-expressions.
2017-04-27 Gary Dismukes <dismukes@adacore.com>
* exp_ch4.adb, sem_ch4.adb: Minor typo fix and reformatting.

View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2017, 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- --
@ -3931,7 +3931,7 @@ package Atree is
-- The nodes of the tree are stored in a table (i.e. an array). In the
-- case of extended nodes six consecutive components in the array are
-- used. There are thus two formats for array components. One is used
-- for non-extended nodes, and for the first component of extended
-- for nonextended nodes, and for the first component of extended
-- nodes. The other is used for the extension parts (second, third,
-- fourth, fifth, and sixth components) of an extended node. A variant
-- record structure is used to distinguish the two formats.
@ -4021,7 +4021,7 @@ package Atree is
-- Pflag2 used as Flag63,Flag64,Flag151,Flag238,Flag309
Nkind : Node_Kind;
-- For a non-extended node, or the initial section of an extended
-- For a nonextended node, or the initial section of an extended
-- node, this field holds the Node_Kind value. For an extended node,
-- The Nkind field is used as follows:
--
@ -4032,11 +4032,11 @@ package Atree is
-- Sixth entry: holds 8 additional flags (Flag310-317)
-- Seventh entry: currently unused
-- Now finally (on an 32-bit boundary) comes the variant part
-- Now finally (on a 32-bit boundary) comes the variant part
case Is_Extension is
-- Non-extended node, or first component of extended node
-- Nonextended node, or first component of extended node
when False =>
@ -4070,7 +4070,7 @@ package Atree is
Field10 : Union_Id;
Field11 : Union_Id;
Field12 : Union_Id;
-- Seven additional general fields available only for entities
-- Seven additional general fields available only for entities.
-- See package Einfo for details of their use (which depends
-- on the value in the Ekind field).

View File

@ -6697,9 +6697,20 @@ package body Checks is
Set_Etype (N, Target_Base_Type);
end Convert_And_Check_Range;
-- Local variables
Checks_On : constant Boolean :=
not Index_Checks_Suppressed (Target_Type)
or else
not Range_Checks_Suppressed (Target_Type);
-- Start of processing for Generate_Range_Check
begin
if not Expander_Active or not Checks_On then
return;
end if;
-- First special case, if the source type is already within the range
-- of the target type, then no check is needed (probably we should have
-- stopped Do_Range_Check from being set in the first place, but better

View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2017, 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- --
@ -109,7 +109,7 @@ package body Debug is
-- d.p Use original Ada 95 semantics for Bit_Order (disable AI95-0133)
-- d.q Suppress optimizations on imported 'in'
-- d.r Enable OK_To_Reorder_Components in non-variant records
-- d.s
-- d.s Minimize secondary stack Mark and Release calls
-- d.t Disable static allocation of library level dispatch tables
-- d.u Enable Modify_Tree_For_C (update tree for c)
-- d.v Enable OK_To_Reorder_Components in variant records
@ -572,6 +572,11 @@ package body Debug is
-- d.r Forces the flag OK_To_Reorder_Components to be set in all record
-- base types that have no discriminants.
-- d.s The compiler does not generate calls to secondary stack management
-- routines SS_Mark and SS_Release for a transient block when there is
-- an enclosing scoping construct which already manages the secondary
-- stack.
-- d.t The compiler has been modified (a fairly extensive modification)
-- to generate static dispatch tables for library level tagged types.
-- This debug switch disables this modification and reverts to the

View File

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2017, 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- --
@ -4163,10 +4163,10 @@ package Einfo is
-- needed, since returns an invalid value in this case.
-- Sec_Stack_Needed_For_Return (Flag167)
-- Defined in scope entities (blocks, functions, procedures, tasks,
-- entries). Set to True when secondary stack is used to hold the
-- returned value of a function and thus should not be released on
-- scope exit.
-- Defined in scope entities (blocks, entries, entry families, functions,
-- and procedures). Set to True when secondary stack is used to hold the
-- returned value of a function and thus should not be released on scope
-- exit.
-- Shadow_Entities (List14)
-- Defined in package and generic package entities. Points to a list
@ -4522,9 +4522,10 @@ package Einfo is
-- Protection object (see System.Tasking.Protected_Objects).
-- Uses_Sec_Stack (Flag95)
-- Defined in scope entities (block, entry, function, loop, procedure,
-- task). Set to True when secondary stack is used in this scope and must
-- be released on exit unless Sec_Stack_Needed_For_Return is set.
-- Defined in scope entities (blocks, entries, entry families, functions,
-- loops, and procedures). Set to True when the secondary stack is used
-- in this scope and must be released on exit unless flag
-- Sec_Stack_Needed_For_Return is set.
-- Validated_Object (Node36)
-- Defined in variables. Contains the object whose value is captured by
@ -6442,11 +6443,9 @@ package Einfo is
-- SPARK_Pragma (Node40)
-- SPARK_Aux_Pragma (Node41)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- Uses_Lock_Free (Flag188)
-- Uses_Sec_Stack (Flag95) ???
-- First_Component (synth)
-- First_Component_Or_Discriminant (synth)
-- Has_Entries (synth)
@ -6597,10 +6596,8 @@ package Einfo is
-- Has_Master_Entity (Flag21)
-- Has_Storage_Size_Clause (Flag23) (base type only)
-- Ignore_SPARK_Mode_Pragmas (Flag301)
-- Sec_Stack_Needed_For_Return (Flag167) ???
-- SPARK_Aux_Pragma_Inherited (Flag266)
-- SPARK_Pragma_Inherited (Flag265)
-- Uses_Sec_Stack (Flag95) ???
-- First_Component (synth)
-- First_Component_Or_Discriminant (synth)
-- Has_Entries (synth)

View File

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2017, 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- --
@ -8266,83 +8266,115 @@ package body Exp_Ch7 is
Action : Node_Id;
Par : Node_Id) return Node_Id
is
Decls : constant List_Id := New_List;
Instrs : constant List_Id := New_List (Action);
function Manages_Sec_Stack (Id : Entity_Id) return Boolean;
-- Determine whether scoping entity Id manages the secondary stack
-----------------------
-- Manages_Sec_Stack --
-----------------------
function Manages_Sec_Stack (Id : Entity_Id) return Boolean is
begin
-- An exception handler with a choice parameter utilizes a dummy
-- block to provide a declarative region. Such a block should not be
-- considered because it never manifests in the tree and can never
-- release the secondary stack.
if Ekind (Id) = E_Block
and then Uses_Sec_Stack (Id)
and then not Is_Exception_Handler (Id)
then
return True;
-- Loops are intentionally excluded because they undergo special
-- treatment, see Establish_Transient_Scope.
elsif Ekind_In (Id, E_Entry,
E_Entry_Family,
E_Function,
E_Procedure)
and then Uses_Sec_Stack (Id)
then
return True;
else
return False;
end if;
end Manages_Sec_Stack;
-- Local variables
Decls : constant List_Id := New_List;
Instrs : constant List_Id := New_List (Action);
Trans_Id : constant Entity_Id := Current_Scope;
Block : Node_Id;
Insert : Node_Id;
Scop : Entity_Id;
-- Start of processing for Make_Transient_Block
begin
-- Case where only secondary stack use is involved
-- Even though the transient block is tasked with managing the secondary
-- stack, the block may forgo this functionality depending on how the
-- secondary stack is managed by enclosing scopes.
if Uses_Sec_Stack (Current_Scope)
and then Nkind (Action) /= N_Simple_Return_Statement
and then Nkind (Par) /= N_Exception_Handler
then
declare
S : Entity_Id;
if Manages_Sec_Stack (Trans_Id) then
begin
S := Scope (Current_Scope);
loop
-- At the outer level, no need to release the sec stack
-- Determine whether an enclosing scope already manages the secondary
-- stack.
if S = Standard_Standard then
Set_Uses_Sec_Stack (Current_Scope, False);
exit;
Scop := Scope (Trans_Id);
while Present (Scop) loop
if Scop = Standard_Standard then
exit;
-- In a function, only release the sec stack if the function
-- does not return on the sec stack otherwise the result may
-- be lost. The caller is responsible for releasing.
-- The transient block must manage the secondary stack when the
-- block appears within a loop in order to reclaim the memory at
-- each iteration.
elsif Ekind (S) = E_Function then
Set_Uses_Sec_Stack (Current_Scope, False);
elsif Ekind (Scop) = E_Loop then
exit;
if not Requires_Transient_Scope (Etype (S)) then
Set_Uses_Sec_Stack (S, True);
Check_Restriction (No_Secondary_Stack, Action);
end if;
-- The transient block is within a function which returns on the
-- secondary stack. Take a conservative approach and assume that
-- the value on the secondary stack is part of the result. Note
-- that it is not possible to detect this dependency without flow
-- analysis which the compiler does not have. Letting the object
-- live longer than the transient block will not leak any memory
-- because the caller will reclaim the total storage used by the
-- function.
exit;
elsif Ekind (Scop) = E_Function
and then Sec_Stack_Needed_For_Return (Scop)
then
Set_Uses_Sec_Stack (Trans_Id, False);
exit;
-- In a loop or entry we should install a block encompassing
-- all the construct. For now just release right away.
-- When requested, the transient block does not need to manage the
-- secondary stack when there exists an enclosing block, entry,
-- entry family, function, or a procedure which already does that.
-- This optimization saves on SS_Mark and SS_Release calls but may
-- allow objects to live a little longer than required.
elsif Ekind_In (S, E_Entry, E_Loop) then
exit;
elsif Debug_Flag_Dot_S and then Manages_Sec_Stack (Scop) then
Set_Uses_Sec_Stack (Trans_Id, False);
exit;
end if;
-- In a procedure or a block, release the sec stack on exit
-- from the construct. Note that an exception handler with a
-- choice parameter requires a declarative region in the form
-- of a block. The block does not physically manifest in the
-- tree as it only serves as a scope. Do not consider such a
-- block because it will never release the sec stack.
-- ??? Memory leak can be created by recursive calls
elsif Ekind (S) = E_Procedure
or else (Ekind (S) = E_Block
and then not Is_Exception_Handler (S))
then
Set_Uses_Sec_Stack (Current_Scope, False);
Set_Uses_Sec_Stack (S, True);
Check_Restriction (No_Secondary_Stack, Action);
exit;
else
S := Scope (S);
end if;
end loop;
end;
Scop := Scope (Scop);
end loop;
end if;
-- Create the transient block. Set the parent now since the block itself
-- is not part of the tree. The current scope is the E_Block entity
-- that has been pushed by Establish_Transient_Scope.
-- is not part of the tree. The current scope is the E_Block entity that
-- has been pushed by Establish_Transient_Scope.
pragma Assert (Ekind (Trans_Id) = E_Block);
pragma Assert (Ekind (Current_Scope) = E_Block);
Block :=
Make_Block_Statement (Loc,
Identifier => New_Occurrence_Of (Current_Scope, Loc),
Identifier => New_Occurrence_Of (Trans_Id, Loc),
Declarations => Decls,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc, Statements => Instrs),
@ -8357,8 +8389,9 @@ package body Exp_Ch7 is
(Action, Clean => False, Manage_SS => False);
Insert := Prev (Action);
if Present (Insert) then
Freeze_All (First_Entity (Current_Scope), Insert);
Freeze_All (First_Entity (Trans_Id), Insert);
end if;
-- Transfer cleanup actions to the newly created block

View File

@ -11611,6 +11611,7 @@ package body Sem_Attr is
if Is_Scalar_Type (Component_Type (Typ))
and then not Is_OK_Static_Expression (Expr)
and then not Range_Checks_Suppressed (Component_Type (Typ))
then
if Is_Entity_Name (Expr)
and then Etype (Expr) = Component_Type (Typ)
@ -11682,6 +11683,8 @@ package body Sem_Attr is
if Is_Scalar_Type (Etype (Entity (Comp)))
and then not Is_OK_Static_Expression (Expr)
and then not Range_Checks_Suppressed
(Etype (Entity (Comp)))
then
Set_Do_Range_Check (Expr);
end if;

View File

@ -1041,11 +1041,16 @@ package body Sem_Aux is
function Is_Generic_Formal (E : Entity_Id) return Boolean is
Kind : Node_Kind;
begin
if No (E) then
return False;
else
Kind := Nkind (Parent (E));
-- Formal derived types are rewritten as private extensions, so
-- examine original node.
Kind := Nkind (Original_Node (Parent (E)));
return
Nkind_In (Kind, N_Formal_Object_Declaration,
N_Formal_Package_Declaration,

View File

@ -1074,7 +1074,7 @@ package body Sem_Ch12 is
F_Copy : List_Id) return List_Id
is
Actuals_To_Freeze : constant Elist_Id := New_Elmt_List;
Assoc : constant List_Id := New_List;
Assoc_List : constant List_Id := New_List;
Default_Actuals : constant List_Id := New_List;
Gen_Unit : constant Entity_Id :=
Defining_Entity (Parent (F_Copy));
@ -1204,6 +1204,7 @@ package body Sem_Ch12 is
Prims : constant Elist_Id := Collect_Primitive_Operations (Typ);
Elem : Elmt_Id;
Formal : Node_Id;
Op : Entity_Id;
begin
-- Locate primitive operations of the type that are arithmetic
@ -1218,12 +1219,54 @@ package body Sem_Ch12 is
-- to justify a warning.
Formal := First_Non_Pragma (Formals);
Op := Alias (Node (Elem));
while Present (Formal) loop
if Nkind (Formal) = N_Formal_Concrete_Subprogram_Declaration
and then Chars (Defining_Entity (Formal)) =
Chars (Node (Elem))
then
exit;
elsif Nkind (Formal) = N_Formal_Package_Declaration then
declare
Assoc : Node_Id;
Ent : Entity_Id;
begin
-- Locate corresponding actual, and check whether it
-- includes a fixed-point type.
Assoc := First (Assoc_List);
while Present (Assoc) loop
exit when
Nkind (Assoc) = N_Package_Renaming_Declaration
and then Chars (Defining_Unit_Name (Assoc)) =
Chars (Defining_Identifier (Formal));
Next (Assoc);
end loop;
if Present (Assoc) then
-- If formal package declares a fixed-point type,
-- and the user-defined operator is derived from
-- a generic instance package, the fixed-point type
-- does not use the corresponding predefined op.
Ent := First_Entity (Entity (Name (Assoc)));
while Present (Ent) loop
if Is_Fixed_Point_Type (Ent)
and then Present (Op)
and then Is_Generic_Instance (Scope (Op))
then
return;
end if;
Next_Entity (Ent);
end loop;
end if;
end;
end if;
Next (Formal);
@ -1414,7 +1457,7 @@ package body Sem_Ch12 is
Set_Defining_Identifier (Decl, Id);
end if;
Append (Decl, Assoc);
Append (Decl, Assoc_List);
if No (Found_Assoc) then
Default :=
@ -1610,7 +1653,7 @@ package body Sem_Ch12 is
else
Append_List
(Instantiate_Object (Formal, Match, Analyzed_Formal),
Assoc);
Assoc_List);
-- For a defaulted in_parameter, create an entry in the
-- the list of defaulted actuals, for GNATProve use. Do
@ -1667,8 +1710,8 @@ package body Sem_Ch12 is
Analyze (Match);
Append_List
(Instantiate_Type
(Formal, Match, Analyzed_Formal, Assoc),
Assoc);
(Formal, Match, Analyzed_Formal, Assoc_List),
Assoc_List);
if Is_Fixed_Point_Type (Entity (Match)) then
Check_Fixed_Point_Actual (Match);
@ -1767,7 +1810,7 @@ package body Sem_Ch12 is
end if;
else
Append_To (Assoc,
Append_To (Assoc_List,
Instantiate_Formal_Subprogram
(Formal, Match, Analyzed_Formal));
@ -1810,7 +1853,8 @@ package body Sem_Ch12 is
if No (Match) and then Box_Present (Formal) then
declare
Subp : constant Entity_Id :=
Defining_Unit_Name (Specification (Last (Assoc)));
Defining_Unit_Name
(Specification (Last (Assoc_List)));
begin
Append_To (Default_Actuals,
@ -1849,7 +1893,7 @@ package body Sem_Ch12 is
Append_List
(Instantiate_Formal_Package
(Formal, Match, Analyzed_Formal),
Assoc);
Assoc_List);
end if;
-- For use type and use package appearing in the generic part,
@ -1863,10 +1907,10 @@ package body Sem_Ch12 is
if Nkind (Original_Node (I_Node)) =
N_Formal_Package_Declaration
then
Append (New_Copy_Tree (Formal), Assoc);
Append (New_Copy_Tree (Formal), Assoc_List);
else
Remove (Formal);
Append (Formal, Assoc);
Append (Formal, Assoc_List);
end if;
when others =>
@ -1941,7 +1985,7 @@ package body Sem_Ch12 is
Append_List (Default_Formals, Formals);
end if;
return Assoc;
return Assoc_List;
end Analyze_Associations;
-------------------------------

View File

@ -7661,9 +7661,9 @@ package body Sem_Ch4 is
return True;
end Constant_Indexing_OK;
-----------------------------
-- Expr_Matches_In_Formal --
-----------------------------
----------------------------
-- Expr_Matches_In_Formal --
----------------------------
function Expr_Matches_In_Formal
(Subp : Entity_Id;

View File

@ -1406,6 +1406,14 @@ package body Sem_Dim is
-- Start of processing for Analyze_Dimension_Binary_Op
begin
-- If the node is already analyzed, do not examine the operands. At the
-- end of the analysis their dimensions have been removed, and the node
-- itself may have been rewritten.
if Analyzed (N) then
return;
end if;
if Nkind_In (N_Kind, N_Op_Add, N_Op_Expon, N_Op_Subtract)
or else N_Kind in N_Multiplying_Operator
or else N_Kind in N_Op_Compare

View File

@ -3228,6 +3228,15 @@ package body Sem_Util is
(Prag : Node_Id;
Result_Seen : in out Boolean)
is
procedure Check_Conjunct (Expr : Node_Id);
-- Check an individual conjunct in a conjunctions of Boolean
-- expressions, connected by "and" or "and then" operators.
procedure Check_Conjuncts (Expr : Node_Id);
-- Apply the post-state check to every conjunct in an expression, in
-- case this is a conjunction of Boolean expressions. Otherwise apply
-- it to the expression as a whole.
procedure Check_Expression (Expr : Node_Id);
-- Perform the 'Result and post-state checks on a given expression
@ -3244,6 +3253,103 @@ package body Sem_Util is
procedure Check_Function_Result is
new Traverse_Proc (Is_Function_Result);
--------------------
-- Check_Conjunct --
--------------------
procedure Check_Conjunct (Expr : Node_Id) is
function Adjust_Message (Msg : String) return String;
-- Prepend a prefix to the input message Msg denoting that the
-- message applies to a conjunct in the expression, when this
-- is the case.
function Applied_On_Conjunct return Boolean;
-- Returns True if the message applies to a conjunct in the
-- expression, instead of the whole expression.
--------------------
-- Adjust_Message --
--------------------
function Adjust_Message (Msg : String) return String is
begin
if Applied_On_Conjunct then
return "conjunct in " & Msg;
else
return Msg;
end if;
end Adjust_Message;
-------------------------
-- Applied_On_Conjunct --
-------------------------
function Applied_On_Conjunct return Boolean is
begin
-- Expr is the conjunct of an "and" enclosing expression
return Nkind (Parent (Expr)) in N_Subexpr
-- or Expr is a conjunct of an "and then" enclosing
-- expression in a postcondition aspect, which was split in
-- multiple pragmas. The first conjunct has the "and then"
-- expression as Original_Node, and other conjuncts have
-- Split_PCC set to True.
or else Nkind (Original_Node (Expr)) = N_And_Then
or else Split_PPC (Prag);
end Applied_On_Conjunct;
-- Local variables
Err_Node : Node_Id;
-- Error node when reporting a warning on a (refined)
-- postcondition.
-- Start of processing for Check_Conjunct
begin
if Applied_On_Conjunct then
Err_Node := Expr;
else
Err_Node := Prag;
end if;
if not Is_Trivial_Boolean (Expr)
and then not Mentions_Post_State (Expr)
then
if Pragma_Name (Prag) = Name_Contract_Cases then
Error_Msg_NE (Adjust_Message
("contract case does not check the outcome of calling "
& "&?T?"), Expr, Subp_Id);
elsif Pragma_Name (Prag) = Name_Refined_Post then
Error_Msg_NE (Adjust_Message
("refined postcondition does not check the outcome of "
& "calling &?T?"), Err_Node, Subp_Id);
else
Error_Msg_NE (Adjust_Message
("postcondition does not check the outcome of calling "
& "&?T?"), Err_Node, Subp_Id);
end if;
end if;
end Check_Conjunct;
---------------------
-- Check_Conjuncts --
---------------------
procedure Check_Conjuncts (Expr : Node_Id) is
begin
if Nkind_In (Expr, N_Op_And, N_And_Then) then
Check_Conjuncts (Left_Opnd (Expr));
Check_Conjuncts (Right_Opnd (Expr));
else
Check_Conjunct (Expr);
end if;
end Check_Conjuncts;
----------------------
-- Check_Expression --
----------------------
@ -3252,24 +3358,7 @@ package body Sem_Util is
begin
if not Is_Trivial_Boolean (Expr) then
Check_Function_Result (Expr);
if not Mentions_Post_State (Expr) then
if Pragma_Name (Prag) = Name_Contract_Cases then
Error_Msg_NE
("contract case does not check the outcome of calling "
& "&?T?", Expr, Subp_Id);
elsif Pragma_Name (Prag) = Name_Refined_Post then
Error_Msg_NE
("refined postcondition does not check the outcome of "
& "calling &?T?", Prag, Subp_Id);
else
Error_Msg_NE
("postcondition does not check the outcome of calling "
& "&?T?", Prag, Subp_Id);
end if;
end if;
Check_Conjuncts (Expr);
end if;
end Check_Expression;

View File

@ -589,10 +589,10 @@ package Sinfo is
-- 8. Instantiations - Save as 1) or when the instantiation is partially
-- analyzed and the generic template is Ghost.
-- Routines Mark_And_Set_Ghost_xxx install a new Ghost region and routine
-- Restore_Ghost_Mode ends a Ghost region. A region may be reinstalled
-- similar to scopes for decoupled expansion such as the generation of
-- dispatch tables or the creation of a predicate function.
-- Routines Mark_And_Set_Ghost_xxx and Set_Ghost_Mode install a new Ghost
-- region and routine Restore_Ghost_Mode ends a Ghost region. A region may
-- be reinstalled similarly to scopes for decoupled expansion such as the
-- generation of dispatch tables or the creation of a predicate function.
-- If the mode of a Ghost region is Ignore, any newly created nodes as well
-- as source entities are marked as ignored Ghost. In additon, the marking
@ -686,6 +686,43 @@ package Sinfo is
-- array depending on a discriminant of a unconstrained formal object
-- parameter of a generic.
----------------
-- SPARK Mode --
----------------
-- The SPARK RM 1.6.5 defines a mode of operation called "SPARK mode" which
-- starts a scope where the SPARK language semantics are either On, Off, or
-- Auto, where Auto leaves the choice to the tools. A SPARK mode may be
-- specified by means of an aspect or a pragma.
-- The following entities may be subject to a SPARK mode. Entities marked
-- with * may possess two differente SPARK modes.
-- E_Entry
-- E_Entry_Family
-- E_Function
-- E_Generic_Function
-- E_Generic_Package *
-- E_Generic_Procedure
-- E_Operator
-- E_Package *
-- E_Package_Body *
-- E_Procedure
-- E_Protected_Body
-- E_Protected_Subtype
-- E_Protected_Type *
-- E_Subprogram_Body
-- E_Task_Body
-- E_Task_Subtype
-- E_Task_Type *
-- E_Variable
-- In order to manage SPARK scopes, the compiler relies on global variables
-- SPARK_Mode and SPARK_Mode_Pragma and a mechanism called "SPARK regions."
-- Routines Install_SPARK_Mode and Set_SPARK_Mode create a new SPARK region
-- and routine Restore_SPARK_Mode ends a SPARK region. A region may be
-- reinstalled similarly to scopes.
-----------------------
-- Check Flag Fields --
-----------------------
@ -5364,23 +5401,6 @@ package Sinfo is
-- Was_Expression_Function (Flag18-Sem)
-- Was_Originally_Stub (Flag13-Sem)
-------------------------
-- Expression Function --
-------------------------
-- This is an Ada 2012 extension, we put it here for now, to be labeled
-- and put in its proper section when we know exactly where that is.
-- EXPRESSION_FUNCTION ::=
-- FUNCTION SPECIFICATION IS (EXPRESSION)
-- [ASPECT_SPECIFICATIONS];
-- N_Expression_Function
-- Sloc points to FUNCTION
-- Specification (Node1)
-- Expression (Node3)
-- Corresponding_Spec (Node5-Sem)
-----------------------------------
-- 6.4 Procedure Call Statement --
-----------------------------------
@ -5533,6 +5553,20 @@ package Sinfo is
-- Return_Object_Declarations represents the object being
-- returned. N_Simple_Return_Statement has only the former.
------------------------------
-- 6.8 Expression Function --
------------------------------
-- EXPRESSION_FUNCTION ::=
-- FUNCTION SPECIFICATION IS (EXPRESSION)
-- [ASPECT_SPECIFICATIONS];
-- N_Expression_Function
-- Sloc points to FUNCTION
-- Specification (Node1)
-- Expression (Node3)
-- Corresponding_Spec (Node5-Sem)
------------------------------
-- 7.1 Package Declaration --
------------------------------

View File

@ -512,30 +512,38 @@ package body Sinput is
-- Assert various properties of the result
procedure Assertions is
-- ???The old version using zero-origin array indexing without array
-- bounds checks returned 1 (i.e. system.ads) for these special
-- locations, presumably by accident. We are mimicing that here.
Special : constant Boolean :=
S = No_Location or else S = Standard_Location
or else S = Standard_ASCII_Location or else S = System_Location;
pragma Assert ((S > No_Location) xor Special);
Special : constant Boolean :=
S = No_Location
or else S = Standard_Location
or else S = Standard_ASCII_Location
or else S = System_Location;
pragma Assert ((S > No_Location) xor Special);
pragma Assert (Result in Source_File.First .. Source_File.Last);
SFR : Source_File_Record renames Source_File.Table (Result);
begin
-- SFR.Source_Text = null if and only if this is the SFR for a debug
-- output file (*.dg), and that file is under construction.
-- output file (*.dg), and that file is under construction. S can be
-- slightly past Source_Last in that case because we haven't updated
-- Source_Last.
if not Null_Source_Buffer_Ptr (SFR.Source_Text) then
if Null_Source_Buffer_Ptr (SFR.Source_Text) then
pragma Assert (S >= SFR.Source_First); null;
else
pragma Assert (SFR.Source_Text'First = SFR.Source_First);
pragma Assert (SFR.Source_Text'Last = SFR.Source_Last);
null;
end if;
if not Special then
pragma Assert (S in SFR.Source_First .. SFR.Source_Last);
null;
if not Special then
pragma Assert (S in SFR.Source_First .. SFR.Source_Last);
null;
end if;
end if;
end Assertions;