+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.
-- --
-- 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- --
-- 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.
-- 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:
--
-- 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 =>
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).
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
-- --
-- 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- --
-- 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
-- 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
-- --
-- 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- --
-- 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
-- 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
-- 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)
-- 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)
-- --
-- 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- --
Action : Node_Id;
Par : Node_Id) return Node_Id
is
- Decls : constant List_Id := New_List;
- Instrs : constant List_Id := New_List (Action);
- Block : Node_Id;
- Insert : Node_Id;
+ function Manages_Sec_Stack (Id : Entity_Id) return Boolean;
+ -- Determine whether scoping entity Id manages the secondary stack
- begin
- -- Case where only secondary stack use is involved
+ -----------------------
+ -- Manages_Sec_Stack --
+ -----------------------
- 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;
+ 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;
- begin
- S := Scope (Current_Scope);
- loop
- -- At the outer level, no need to release the sec stack
+ -- Loops are intentionally excluded because they undergo special
+ -- treatment, see Establish_Transient_Scope.
- if S = Standard_Standard then
- Set_Uses_Sec_Stack (Current_Scope, False);
- exit;
+ elsif Ekind_In (Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Procedure)
+ and then Uses_Sec_Stack (Id)
+ then
+ return True;
- -- 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.
+ else
+ return False;
+ end if;
+ end Manages_Sec_Stack;
- elsif Ekind (S) = E_Function then
- Set_Uses_Sec_Stack (Current_Scope, False);
+ -- Local variables
- if not Requires_Transient_Scope (Etype (S)) then
- Set_Uses_Sec_Stack (S, True);
- Check_Restriction (No_Secondary_Stack, Action);
- end if;
+ Decls : constant List_Id := New_List;
+ Instrs : constant List_Id := New_List (Action);
+ Trans_Id : constant Entity_Id := Current_Scope;
- exit;
+ Block : Node_Id;
+ Insert : Node_Id;
+ Scop : Entity_Id;
- -- In a loop or entry we should install a block encompassing
- -- all the construct. For now just release right away.
+ -- Start of processing for Make_Transient_Block
- elsif Ekind_In (S, E_Entry, E_Loop) then
- exit;
+ begin
+ -- 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.
- -- 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.
+ if Manages_Sec_Stack (Trans_Id) then
- -- ??? Memory leak can be created by recursive calls
+ -- Determine whether an enclosing scope already manages the secondary
+ -- stack.
- 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;
+ Scop := Scope (Trans_Id);
+ while Present (Scop) loop
+ if Scop = Standard_Standard then
+ exit;
- else
- S := Scope (S);
- end if;
- end loop;
- end;
+ -- 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 (Scop) = E_Loop then
+ exit;
+
+ -- 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.
+
+ elsif Ekind (Scop) = E_Function
+ and then Sec_Stack_Needed_For_Return (Scop)
+ then
+ Set_Uses_Sec_Stack (Trans_Id, False);
+ exit;
+
+ -- 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 Debug_Flag_Dot_S and then Manages_Sec_Stack (Scop) then
+ Set_Uses_Sec_Stack (Trans_Id, False);
+ exit;
+ end if;
+
+ 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),
(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
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)
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;
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,
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));
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
-- 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);
Set_Defining_Identifier (Decl, Id);
end if;
- Append (Decl, Assoc);
+ Append (Decl, Assoc_List);
if No (Found_Assoc) then
Default :=
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
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);
end if;
else
- Append_To (Assoc,
+ Append_To (Assoc_List,
Instantiate_Formal_Subprogram
(Formal, Match, Analyzed_Formal));
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,
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,
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 =>
Append_List (Default_Formals, Formals);
end if;
- return Assoc;
+ return Assoc_List;
end Analyze_Associations;
-------------------------------
return True;
end Constant_Indexing_OK;
- -----------------------------
- -- Expr_Matches_In_Formal --
- -----------------------------
+ ----------------------------
+ -- Expr_Matches_In_Formal --
+ ----------------------------
function Expr_Matches_In_Formal
(Subp : Entity_Id;
-- 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
(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
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 --
----------------------
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;
-- 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
-- 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 --
-----------------------
-- 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 --
-----------------------------------
-- 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 --
------------------------------
-- 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);
+ 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;
projects / gcc.git / commitdiff