+2014-02-18 Robert Dewar <dewar@adacore.com>
+
+ * cstand.adb (Build_Signed_Integer_Type): Minor change of formal
+ from Int to Nat (Build_Unsigned_Integer_Type): New procedure
+ (Create_Standard): Create new unsigned types.
+ * exp_ch4.adb (Expand_N_Op_Mod): Expand mod in Modify_Tree_For_C
+ mode (Expand_N_Reference): Removed, problematic and not needed
+ for now.
+ * exp_ch4.ads (Expand_N_Reference): Removed, problematic and
+ not needed for now.
+ * exp_util.ads, exp_util.adb (Power_Of_Two): New function.
+ * expander.adb: Remove call to Expand_N_Reference (problematic,
+ and not needed now).
+ * sem_aux.ads, sem_aux.adb (Corresponding_Unsigned_Type): New function.
+ * stand.adb: Read and write unsigned type entities.
+ * stand.ads: Add new unsigned types.
+
+2014-02-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch4.adb (Analyze_Call): Do not mark a function call
+ as being inside an assertion expression as the flag is now removed.
+ (Check_Ghost_Subprogram_Call): Do not query the
+ In_Assertion_Expression flag as it is now removed, instead use
+ a predicate function.
+ * sem_elab.adb (Check_Internal_Call_Continue): Do not query the
+ In_Assertion_Expression flag as it is now removed, instead use
+ a predicate function.
+ * sem_prag.ads: Add new table Assertion_Expression_Pragma.
+ * sem_util.adb Add with and use clause for Sem_Prag.
+ (In_Assertion_Expression_Pragma): New routine.
+ * sem_util.ads (In_Assertion_Expression_Pragma): New routine.
+ * sinfo.adb (In_Assertion_Expression): Removed.
+ (Set_In_Assertion_Expression): Removed.
+ * sinfo.ads Remove flag In_Assertion_Expression along with its
+ use in nodes.
+ (In_Assertion_Expression): Removed along with
+ pragma Inline. (Set_In_Assertion_Expression): Removed along
+ with pragma Inline.
+
+2014-02-18 Sergey Rybin <rybin@adacore.com frybin>
+
+ * gnat_ugn.texi: gnatpp section: add note that '-j' cannot be
+ used together with '-r', '-rf' or '-rnb' options.
+
+2014-02-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_attr.adb (Analyze_Attribute): Comment
+ and code reformatting. Use separate routines to check the
+ legality of attribute 'Old in certain pragmas. Verify
+ the use of 'Old, 'Result and locally declared entities
+ within the prefix of 'Old.
+ (Check_References_In_Prefix): New routine.
+ (Check_Use_In_Contract_Cases): New routine.
+ (Check_Use_In_Test_Case): New routine.
+
2014-02-18 Vincent Celier <celier@adacore.com>
* sem_aux.adb (Is_By_Reference_Type): For each components of
-- to be used. The fourth parameter is the digits value. Each type
-- is added to the list of predefined floating point types.
- procedure Build_Signed_Integer_Type (E : Entity_Id; Siz : Int);
+ procedure Build_Signed_Integer_Type (E : Entity_Id; Siz : Nat);
-- Procedure to build standard predefined signed integer subtype. The
-- first parameter is the entity for the subtype. The second parameter
-- is the size in bits. The corresponding base type is not built by
-- this routine but instead must be built by the caller where needed.
+ procedure Build_Unsigned_Integer_Type
+ (Uns : Entity_Id;
+ Siz : Nat;
+ Nam : String);
+ -- Procedure to build standard predefined unsigned integer subtype. These
+ -- subtypes are not user visible, but they are used internally. The first
+ -- parameter is the entity for the subtype. The second parameter is the
+ -- size in bits. The third parameter is an identifying name.
+
procedure Copy_Float_Type (To : Entity_Id; From : Entity_Id);
-- Build a floating point type, copying representation details from From.
-- This is used to create predefined floating point types based on
-- Build_Signed_Integer_Type --
-------------------------------
- procedure Build_Signed_Integer_Type (E : Entity_Id; Siz : Int) is
+ procedure Build_Signed_Integer_Type (E : Entity_Id; Siz : Nat) is
U2Siz1 : constant Uint := 2 ** (Siz - 1);
Lbound : constant Uint := -U2Siz1;
Ubound : constant Uint := U2Siz1 - 1;
Set_Size_Known_At_Compile_Time (E);
end Build_Signed_Integer_Type;
+ ---------------------------------
+ -- Build_Unsigned_Integer_Type --
+ ---------------------------------
+
+ procedure Build_Unsigned_Integer_Type
+ (Uns : Entity_Id;
+ Siz : Nat;
+ Nam : String)
+ is
+ Decl : Node_Id;
+ R_Node : Node_Id;
+
+ begin
+ Decl := New_Node (N_Full_Type_Declaration, Stloc);
+ Set_Defining_Identifier (Decl, Uns);
+ Make_Name (Uns, Nam);
+
+ Set_Ekind (Uns, E_Modular_Integer_Type);
+ Set_Scope (Uns, Standard_Standard);
+ Set_Etype (Uns, Uns);
+ Init_Size (Uns, Siz);
+ Set_Elem_Alignment (Uns);
+ Set_Modulus (Uns, Uint_2 ** Siz);
+ Set_Is_Unsigned_Type (Uns);
+ Set_Size_Known_At_Compile_Time (Uns);
+ Set_Is_Known_Valid (Uns, True);
+
+ R_Node := New_Node (N_Range, Stloc);
+ Set_Low_Bound (R_Node, Make_Integer (Uint_0));
+ Set_High_Bound (R_Node, Make_Integer (Modulus (Uns) - 1));
+ Set_Etype (Low_Bound (R_Node), Uns);
+ Set_Etype (High_Bound (R_Node), Uns);
+ Set_Scalar_Range (Uns, R_Node);
+ end Build_Unsigned_Integer_Type;
+
---------------------
-- Copy_Float_Type --
---------------------
Set_Scope (Standard_Integer_64, Standard_Standard);
Build_Signed_Integer_Type (Standard_Integer_64, 64);
- -- Standard_Unsigned is not user visible, but is used internally. It
- -- is an unsigned type with the same length as Standard.Integer.
+ -- Standard_*_Unsigned subtypes are not user visible, but they are
+ -- used internally. They are unsigned types with the same length as
+ -- the correspondingly named signed integer types.
- Standard_Unsigned := New_Standard_Entity;
- Decl := New_Node (N_Full_Type_Declaration, Stloc);
- Set_Defining_Identifier (Decl, Standard_Unsigned);
- Make_Name (Standard_Unsigned, "unsigned");
-
- Set_Ekind (Standard_Unsigned, E_Modular_Integer_Type);
- Set_Scope (Standard_Unsigned, Standard_Standard);
- Set_Etype (Standard_Unsigned, Standard_Unsigned);
- Init_Size (Standard_Unsigned, Standard_Integer_Size);
- Set_Elem_Alignment (Standard_Unsigned);
- Set_Modulus (Standard_Unsigned,
- Uint_2 ** Standard_Integer_Size);
- Set_Is_Unsigned_Type (Standard_Unsigned);
- Set_Size_Known_At_Compile_Time
- (Standard_Unsigned);
- Set_Is_Known_Valid (Standard_Unsigned, True);
+ Standard_Short_Short_Unsigned := New_Standard_Entity;
+ Build_Unsigned_Integer_Type
+ (Standard_Short_Short_Unsigned,
+ Standard_Short_Short_Integer_Size,
+ "short_short_unsigned");
- R_Node := New_Node (N_Range, Stloc);
- Set_Low_Bound (R_Node, Make_Integer (Uint_0));
- Set_High_Bound (R_Node, Make_Integer (Modulus (Standard_Unsigned) - 1));
- Set_Etype (Low_Bound (R_Node), Standard_Unsigned);
- Set_Etype (High_Bound (R_Node), Standard_Unsigned);
- Set_Scalar_Range (Standard_Unsigned, R_Node);
+ Standard_Short_Unsigned := New_Standard_Entity;
+ Build_Unsigned_Integer_Type
+ (Standard_Short_Unsigned,
+ Standard_Short_Integer_Size,
+ "short_unsigned");
+
+ Standard_Unsigned := New_Standard_Entity;
+ Build_Unsigned_Integer_Type
+ (Standard_Unsigned,
+ Standard_Integer_Size,
+ "unsigned");
+
+ Standard_Long_Unsigned := New_Standard_Entity;
+ Build_Unsigned_Integer_Type
+ (Standard_Long_Unsigned,
+ Standard_Long_Integer_Size,
+ "long_unsigned");
+
+ Standard_Long_Long_Unsigned := New_Standard_Entity;
+ Build_Unsigned_Integer_Type
+ (Standard_Long_Long_Unsigned,
+ Standard_Long_Long_Integer_Size,
+ "long_long_unsigned");
-- Standard_Unsigned_64 is not user visible, but is used internally. It
-- is an unsigned type mod 2**64, 64-bits unsigned, size is 64.
Standard_Unsigned_64 := New_Standard_Entity;
- Decl := New_Node (N_Full_Type_Declaration, Stloc);
- Set_Defining_Identifier (Decl, Standard_Unsigned_64);
- Make_Name (Standard_Unsigned_64, "unsigned_64");
-
- Set_Ekind (Standard_Unsigned_64, E_Modular_Integer_Type);
- Set_Scope (Standard_Unsigned_64, Standard_Standard);
- Set_Etype (Standard_Unsigned_64, Standard_Unsigned_64);
- Init_Size (Standard_Unsigned_64, 64);
- Set_Elem_Alignment (Standard_Unsigned_64);
- Set_Modulus (Standard_Unsigned_64, Uint_2 ** 64);
- Set_Is_Unsigned_Type (Standard_Unsigned_64);
- Set_Size_Known_At_Compile_Time
- (Standard_Unsigned_64);
- Set_Is_Known_Valid (Standard_Unsigned_64, True);
-
- R_Node := New_Node (N_Range, Stloc);
- Set_Low_Bound (R_Node, Make_Integer (Uint_0));
- Set_High_Bound (R_Node, Make_Integer (Uint_2 ** 64 - 1));
- Set_Etype (Low_Bound (R_Node), Standard_Unsigned_64);
- Set_Etype (High_Bound (R_Node), Standard_Unsigned_64);
- Set_Scalar_Range (Standard_Unsigned_64, R_Node);
+ Build_Unsigned_Integer_Type (Standard_Unsigned_64, 64, "unsigned_64");
-- Note: universal integer and universal real are constructed as fully
-- formed signed numeric types, with parameters corresponding to the
Determine_Range (Right, ROK, Rlo, Rhi, Assume_Valid => True);
Determine_Range (Left, LOK, Llo, Lhi, Assume_Valid => True);
- -- Convert mod to rem if operands are known non-negative. We do this
- -- since it is quite likely that this will improve the quality of code,
- -- (the operation now corresponds to the hardware remainder), and it
- -- does not seem likely that it could be harmful.
-
- if LOK and then Llo >= 0 and then ROK and then Rlo >= 0 then
+ -- Convert mod to rem if operands are both known to be non-negative, or
+ -- both known to be non-positive (these are the cases in which rem and
+ -- mod are the same, see (RM 4.5.5(28-30)). We do this since it is quite
+ -- likely that this will improve the quality of code, (the operation now
+ -- corresponds to the hardware remainder), and it does not seem likely
+ -- that it could be harmful. It also avoids some cases of the elaborate
+ -- expansion in Modify_Tree_For_C mode below (since Ada rem = C %).
+
+ if (LOK and ROK)
+ and then ((Llo >= 0 and then Rlo >= 0)
+ or else
+ (Lhi <= 0 and then Rhi <= 0))
+ then
Rewrite (N,
Make_Op_Rem (Sloc (N),
Left_Opnd => Left_Opnd (N),
Set_Do_Division_Check (N, DDC);
Expand_N_Op_Rem (N);
Set_Analyzed (N);
+ return;
-- Otherwise, normal mod processing
return;
end if;
- -- Deal with annoying case of largest negative number remainder
- -- minus one. Gigi may not handle this case correctly, because
- -- on some targets, the mod value is computed using a divide
- -- instruction which gives an overflow trap for this case.
+ -- If we still have a mod operator and we are in Modify_Tree_For_C
+ -- mode, and we have a signed integer type, then here is where we do
+ -- the rewrite in terms of Rem. Note this rewrite bypasses the need
+ -- for the special handling of the annoying case of largest negative
+ -- number mod minus one.
+
+ if Nkind (N) = N_Op_Mod
+ and then Is_Signed_Integer_Type (Typ)
+ and then Modify_Tree_For_C
+ then
+ -- In the general case, we expand A mod B as
+
+ -- Tnn : constant typ := A rem B;
+ -- ..
+ -- (if (A >= 0) = (B >= 0) then Tnn
+ -- elsif Tnn = 0 then 0
+ -- else Tnn + B)
+
+ -- The comparison can be written simply as A >= 0 if we know that
+ -- B >= 0 which is a very common case.
+
+ -- An important optimization is when B is known at compile time
+ -- to be 2**K for some constant. In this case we can simply AND
+ -- the left operand with the bit string 2**K-1 (i.e. K 1-bits)
+ -- and that works for both the positive and negative cases.
+
+ declare
+ P2 : constant Nat := Power_Of_Two (Right);
+
+ begin
+ if P2 /= 0 then
+ Rewrite (N,
+ Unchecked_Convert_To (Typ,
+ Make_Op_And (Loc,
+ Left_Opnd =>
+ Unchecked_Convert_To
+ (Corresponding_Unsigned_Type (Typ), Left),
+ Right_Opnd =>
+ Make_Integer_Literal (Loc, 2 ** P2 - 1))));
+ Analyze_And_Resolve (N, Typ);
+ return;
+ end if;
+ end;
+
+ -- Here for the full rewrite
+
+ declare
+ Tnn : constant Entity_Id := Make_Temporary (Sloc (N), 'T', N);
+ Cmp : Node_Id;
+
+ begin
+ Cmp :=
+ Make_Op_Ge (Loc,
+ Left_Opnd => Duplicate_Subexpr_No_Checks (Left),
+ Right_Opnd => Make_Integer_Literal (Loc, 0));
+
+ if not LOK or else Rlo < 0 then
+ Cmp :=
+ Make_Op_Eq (Loc,
+ Left_Opnd => Cmp,
+ Right_Opnd =>
+ Make_Op_Ge (Loc,
+ Left_Opnd => Duplicate_Subexpr_No_Checks (Right),
+ Right_Opnd => Make_Integer_Literal (Loc, 0)));
+ end if;
+
+ Insert_Action (N,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Tnn,
+ Constant_Present => True,
+ Object_Definition => New_Occurrence_Of (Typ, Loc),
+ Expression =>
+ Make_Op_Rem (Loc,
+ Left_Opnd => Left,
+ Right_Opnd => Right)));
+
+ Rewrite (N,
+ Make_If_Expression (Loc,
+ Expressions => New_List (
+ Cmp,
+ New_Occurrence_Of (Tnn, Loc),
+ Make_If_Expression (Loc,
+ Is_Elsif => True,
+ Expressions => New_List (
+ Make_Op_Eq (Loc,
+ Left_Opnd => New_Occurrence_Of (Tnn, Loc),
+ Right_Opnd => Make_Integer_Literal (Loc, 0)),
+ Make_Integer_Literal (Loc, 0),
+ Make_Op_Add (Loc,
+ Left_Opnd => New_Occurrence_Of (Tnn, Loc),
+ Right_Opnd =>
+ Duplicate_Subexpr_No_Checks (Right)))))));
+
+ Analyze_And_Resolve (N, Typ);
+ return;
+ end;
+ end if;
+
+ -- Deal with annoying case of largest negative number mod minus one.
+ -- Gigi may not handle this case correctly, because on some targets,
+ -- the mod value is computed using a divide instruction which gives
+ -- an overflow trap for this case.
-- It would be a bit more efficient to figure out which targets
-- this is really needed for, but in practice it is reasonable
Analyze_And_Resolve (N, Standard_Boolean);
end Expand_N_Quantified_Expression;
- ------------------------
- -- Expand_N_Reference --
- ------------------------
-
- -- It is a little unclear why we generate references to expression values,
- -- but we definitely do! At the very least in Modify_Tree_For_C, we need to
- -- get rid of such constructs. We do this by expanding:
-
- -- expression'Reference
-
- -- into
-
- -- Tnn : constant typ := expression;
- -- ...
- -- Tnn'Reference
-
- procedure Expand_N_Reference (N : Node_Id) is
- begin
- -- No problem if Modify_Tree_For_C not set, the existing back ends will
- -- correctly handle P'Reference where P is a general expression.
-
- if not Modify_Tree_For_C then
- return;
-
- -- No problem if we have an entity name since we can take its address
-
- elsif Is_Entity_Name (Prefix (N)) then
- return;
-
- -- Can't go copying limited types
-
- elsif Is_Limited_Record (Etype (Prefix (N)))
- or else Is_Limited_Composite (Etype (Prefix (N)))
- then
- return;
-
- -- Here is the case where we do the transformation discussed above
-
- else
- declare
- Loc : constant Source_Ptr := Sloc (N);
- Expr : constant Node_Id := Prefix (N);
- Typ : constant Entity_Id := Etype (N);
- Tnn : constant Entity_Id := Make_Temporary (Loc, 'T', Expr);
- begin
- Insert_Action (N,
- Make_Object_Declaration (Loc,
- Defining_Identifier => Tnn,
- Constant_Present => True,
- Object_Definition => New_Occurrence_Of (Etype (Expr), Loc),
- Expression => Expr));
- Rewrite (N,
- Make_Reference (Loc,
- Prefix => New_Occurrence_Of (Tnn, Loc)));
- Analyze_And_Resolve (N, Typ);
- end;
- end if;
- end Expand_N_Reference;
-
---------------------------------
-- Expand_N_Selected_Component --
---------------------------------
procedure Expand_N_Or_Else (N : Node_Id);
procedure Expand_N_Qualified_Expression (N : Node_Id);
procedure Expand_N_Quantified_Expression (N : Node_Id);
- procedure Expand_N_Reference (N : Node_Id);
procedure Expand_N_Selected_Component (N : Node_Id);
procedure Expand_N_Slice (N : Node_Id);
procedure Expand_N_Type_Conversion (N : Node_Id);
end case;
end Process_Statements_For_Controlled_Objects;
+ ------------------
+ -- Power_Of_Two --
+ ------------------
+
+ function Power_Of_Two (N : Node_Id) return Nat is
+ Typ : constant Entity_Id := Etype (N);
+ pragma Assert (Is_Integer_Type (Typ));
+ Siz : constant Nat := UI_To_Int (Esize (Typ));
+ Val : Uint;
+
+ begin
+ if not Compile_Time_Known_Value (N) then
+ return 0;
+
+ else
+ Val := Expr_Value (N);
+ for J in 1 .. Siz - 1 loop
+ if Val = Uint_2 ** J then
+ return J;
+ end if;
+ end loop;
+
+ return 0;
+ end if;
+ end Power_Of_Two;
+
----------------------
-- Remove_Init_Call --
----------------------
-- causes trouble for the back end (see Component_May_Be_Bit_Aligned for
-- further details).
+ function Power_Of_Two (N : Node_Id) return Nat;
+ -- Determines if N is a known at compile time value which is of the form
+ -- 2**K, where K is in the range 1 .. M, where the Esize of N is 2**(M+1).
+ -- If so, returns the value K, otherwise returns zero. The caller checks
+ -- that N is of an integer type.
+
procedure Process_Statements_For_Controlled_Objects (N : Node_Id);
-- N is a node which contains a non-handled statement list. Inspect the
-- statements looking for declarations of controlled objects. If at least
when N_Record_Representation_Clause =>
Expand_N_Record_Representation_Clause (N);
- when N_Reference =>
- Expand_N_Reference (N);
-
when N_Requeue_Statement =>
Expand_N_Requeue_Statement (N);
@table @option
@item ^-I^/SEARCH=^@var{dir}
-@cindex @option{^-I^/SEARCH^} (@code{gnatpp})
+@cindex @option{^-I^/SEARCH^} (@command{gnatpp})
The same as the corresponding gcc switch
@item ^-I-^/NOCURRENT_DIRECTORY^
-@cindex @option{^-I-^/NOCURRENT_DIRECTORY^} (@code{gnatpp})
+@cindex @option{^-I-^/NOCURRENT_DIRECTORY^} (@command{gnatpp})
The same as the corresponding gcc switch
@item ^-gnatec^/CONFIGURATION_PRAGMAS_FILE^=@var{path}
-@cindex @option{^-gnatec^/CONFIGURATION_PRAGMAS_FILE^} (@code{gnatpp})
+@cindex @option{^-gnatec^/CONFIGURATION_PRAGMAS_FILE^} (@command{gnatpp})
The same as the corresponding gcc switch
@item ^--RTS^/RUNTIME_SYSTEM^=@var{path}
-@cindex @option{^--RTS^/RUNTIME_SYSTEM^} (@code{gnatpp})
+@cindex @option{^--RTS^/RUNTIME_SYSTEM^} (@command{gnatpp})
The same as the corresponding gcc switch
@end table
@table @option
@item ^-pipe^/STANDARD_OUTPUT^
-@cindex @option{^-pipe^/STANDARD_OUTPUT^} (@code{gnatpp})
+@cindex @option{^-pipe^/STANDARD_OUTPUT^} (@command{gnatpp})
Send the output to @code{Standard_Output}
@item ^-o @var{output_file}^/OUTPUT=@var{output_file}^
reading or processing the input file.
@item ^-of ^/FORCED_OUTPUT=^@var{output_file}
-@cindex @option{^-of^/FORCED_OUTPUT^} (@code{gnatpp})
+@cindex @option{^-of^/FORCED_OUTPUT^} (@command{gnatpp})
Write the output into @var{output_file}, overwriting the existing file
(if one is present).
@item ^-r^/REPLACE^
-@cindex @option{^-r^/REPLACE^} (@code{gnatpp})
+@cindex @option{^-r^/REPLACE^} (@command{gnatpp})
Replace the input source file with the reformatted output, and copy the
original input source into the file whose name is obtained by appending the
^@file{.npp}^@file{$NPP}^ suffix to the name of the input file.
already exists, it is overwritten.
@item ^-rnb^/REPLACE_NO_BACKUP^
-@cindex @option{^-rnb^/REPLACE_NO_BACKUP^} (@code{gnatpp})
+@cindex @option{^-rnb^/REPLACE_NO_BACKUP^} (@command{gnatpp})
Replace the input source file with the reformatted output without
creating any backup copy of the input source.
of the argument sources). On a multiprocessor machine this speeds up processing
of big sets of argument sources. If @var{n} is 0, then the maximum number of
parallel tree creations is the number of core processors on the platform.
+This option cannot be used together with @option{^-r^/REPLACE^},
+@option{^-rf^/OVERRIDING_REPLACE^} or
+@option{^-rnb^/REPLACE_NO_BACKUP^} option.
@cindex @option{^-t^/TIME^} (@command{gnatpp})
@item ^-t^/TIME^
---------
when Attribute_Old => Old : declare
+ procedure Check_References_In_Prefix (Subp_Id : Entity_Id);
+ -- Inspect the contents of the prefix and detect illegal uses of a
+ -- nested 'Old, attribute 'Result or a use of an entity declared in
+ -- the related postcondition expression. Subp_Id is the subprogram to
+ -- which the related postcondition applies.
+
+ procedure Check_Use_In_Contract_Cases (Prag : Node_Id);
+ -- Perform various semantic checks related to the placement of the
+ -- attribute in pragma Contract_Cases.
+
+ procedure Check_Use_In_Test_Case (Prag : Node_Id);
+ -- Perform various semantic checks related to the placement of the
+ -- attribute in pragma Contract_Cases.
+
+ --------------------------------
+ -- Check_References_In_Prefix --
+ --------------------------------
+
+ procedure Check_References_In_Prefix (Subp_Id : Entity_Id) is
+ function Check_Reference (Nod : Node_Id) return Traverse_Result;
+ -- Detect attribute 'Old, attribute 'Result of a use of an entity
+ -- and perform the appropriate semantic check.
+
+ ---------------------
+ -- Check_Reference --
+ ---------------------
+
+ function Check_Reference (Nod : Node_Id) return Traverse_Result is
+ begin
+ -- Attributes 'Old and 'Result cannot appear in the prefix of
+ -- another attribute 'Old.
+
+ if Nkind (Nod) = N_Attribute_Reference
+ and then Nam_In (Attribute_Name (Nod), Name_Old,
+ Name_Result)
+ then
+ Error_Msg_Name_1 := Attribute_Name (Nod);
+ Error_Msg_Name_2 := Name_Old;
+ Error_Msg_N
+ ("attribute % cannot appear in the prefix of attribute %",
+ Nod);
+ return Abandon;
+
+ -- Entities mentioned within the prefix of attribute 'Old must
+ -- be global to the related postcondition. If this is not the
+ -- case, then the scope of the local entity is be nested within
+ -- that of the subprogram.
+
+ elsif Nkind (Nod) = N_Identifier
+ and then Present (Entity (Nod))
+ and then Scope_Within (Scope (Entity (Nod)), Subp_Id)
+ then
+ Error_Attr
+ ("prefix of attribute % cannot reference local entities",
+ Nod);
+ return Abandon;
+ else
+ return OK;
+ end if;
+ end Check_Reference;
+
+ procedure Check_References is new Traverse_Proc (Check_Reference);
+
+ -- Start of processing for Check_References_In_Prefix
+
+ begin
+ Check_References (P);
+ end Check_References_In_Prefix;
+
+ ---------------------------------
+ -- Check_Use_In_Contract_Cases --
+ ---------------------------------
+
+ procedure Check_Use_In_Contract_Cases (Prag : Node_Id) is
+ Cases : constant Node_Id :=
+ Get_Pragma_Arg
+ (First (Pragma_Argument_Associations (Prag)));
+ Expr : Node_Id;
+
+ begin
+ -- Climb the parent chain to reach the top of the expression where
+ -- attribute 'Old resides.
+
+ Expr := N;
+ while Parent (Parent (Expr)) /= Cases loop
+ Expr := Parent (Expr);
+ end loop;
+
+ -- Ensure that the obtained expression is the consequence of a
+ -- contract case as this is the only postcondition-like part of
+ -- the pragma.
+
+ if Expr /= Expression (Parent (Expr)) then
+ Error_Attr
+ ("attribute % cannot appear in the condition of a contract "
+ & "case (SPARK RM 6.1.3(2))", P);
+ end if;
+ end Check_Use_In_Contract_Cases;
+
+ ----------------------------
+ -- Check_Use_In_Test_Case --
+ ----------------------------
+
+ procedure Check_Use_In_Test_Case (Prag : Node_Id) is
+ Ensures : constant Node_Id := Get_Ensures_From_CTC_Pragma (Prag);
+ Expr : Node_Id;
+
+ begin
+ -- Climb the parent chain to reach the top of the Ensures part of
+ -- pragma Test_Case.
+
+ Expr := N;
+ while Expr /= Prag loop
+ if Expr = Ensures then
+ return;
+ end if;
+
+ Expr := Parent (Expr);
+ end loop;
+
+ -- If we get there, then attribute 'Old appears in the requires
+ -- expression of pragma Test_Case which is not a postcondition-
+ -- like context.
+
+ Error_Attr
+ ("attribute % cannot appear in the requires expression of a "
+ & "test case", P);
+ end Check_Use_In_Test_Case;
+
+ -- Local variables
+
CS : Entity_Id;
-- The enclosing scope, excluding loops for quantified expressions.
-- During analysis, it is the postcondition subprogram. During
Prag : Node_Id;
-- During pre-analysis, Prag is the enclosing pragma node if any
+ -- Start of processing for Old
+
begin
Prag := Empty;
CS := Scope (CS);
end loop;
- -- If we are in Spec_Expression mode, this should be the prescan of
- -- the postcondition (or contract case, or test case) pragma.
+ -- A Contract_Cases, Postcondition or Test_Case pragma is in the
+ -- process of being preanalyzed. Perform the semantic checks now
+ -- before the pragma is relocated and/or expanded.
if In_Spec_Expression then
-
- -- Check in postcondition, Test_Case or Contract_Cases
-
Prag := N;
while Present (Prag)
- and then not Nkind_In (Prag, N_Pragma,
+ and then not Nkind_In (Prag, N_Aspect_Specification,
N_Function_Specification,
+ N_Pragma,
N_Procedure_Specification,
- N_Aspect_Specification,
N_Subprogram_Body)
loop
Prag := Parent (Prag);
if Nkind (Prag) = N_Aspect_Specification then
null;
- -- We must have a pragma
+ -- In all other cases the related context must be a pragma
elsif Nkind (Prag) /= N_Pragma then
Error_Attr ("% attribute can only appear in postcondition", P);
- -- Processing depends on which pragma we have
+ -- Verify the placement of the attribute with respect to the
+ -- related pragma.
else
case Get_Pragma_Id (Prag) is
- when Pragma_Test_Case =>
- declare
- Arg_Ens : constant Node_Id :=
- Get_Ensures_From_CTC_Pragma (Prag);
- Arg : Node_Id;
-
- begin
- Arg := N;
- while Arg /= Prag and then Arg /= Arg_Ens loop
- Arg := Parent (Arg);
- end loop;
-
- if Arg /= Arg_Ens then
- Error_Attr
- ("% attribute misplaced inside test case", P);
- end if;
- end;
-
when Pragma_Contract_Cases =>
- declare
- Aggr : constant Node_Id :=
- Expression
- (First (Pragma_Argument_Associations (Prag)));
- Arg : Node_Id;
-
- begin
- Arg := N;
- while Arg /= Prag
- and then Parent (Parent (Arg)) /= Aggr
- loop
- Arg := Parent (Arg);
- end loop;
-
- -- At this point, Parent (Arg) should be a component
- -- association. Attribute Result is only allowed in
- -- the expression part of this association.
-
- if Nkind (Parent (Arg)) /= N_Component_Association
- or else Arg /= Expression (Parent (Arg))
- then
- Error_Attr
- ("% attribute misplaced inside contract cases",
- P);
- end if;
- end;
+ Check_Use_In_Contract_Cases (Prag);
when Pragma_Postcondition | Pragma_Refined_Post =>
null;
+ when Pragma_Test_Case =>
+ Check_Use_In_Test_Case (Prag);
+
when others =>
Error_Attr
("% attribute can only appear in postcondition", P);
elsif not Expander_Active and then In_Refined_Post then
Preanalyze_And_Resolve (P);
+ Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
-- place during expansion (see below).
Preanalyze_And_Resolve (P);
+ Check_References_In_Prefix (CS);
P_Type := Etype (P);
Set_Etype (N, P_Type);
and then Is_Potentially_Unevaluated (N)
and then not Is_Entity_Name (P)
then
- Error_Attr_P ("prefix of attribute % that is potentially "
- & "unevaluated must denote an entity");
+ Error_Attr_P
+ ("prefix of attribute % that is potentially unevaluated must "
+ & "denote an entity");
end if;
-- The attribute appears within a pre/postcondition, but refers to
with Sinfo; use Sinfo;
with Snames; use Snames;
with Stand; use Stand;
+with Uintp; use Uintp;
package body Sem_Aux is
end if;
end Constant_Value;
+ ---------------------------------
+ -- Corresponding_Unsigned_Type --
+ ---------------------------------
+
+ function Corresponding_Unsigned_Type (Typ : Entity_Id) return Entity_Id is
+ pragma Assert (Is_Signed_Integer_Type (Typ));
+ Siz : constant Uint := Esize (Base_Type (Typ));
+ begin
+ if Siz = Esize (Standard_Short_Short_Integer) then
+ return Standard_Short_Short_Unsigned;
+ elsif Siz = Esize (Standard_Short_Integer) then
+ return Standard_Short_Unsigned;
+ elsif Siz = Esize (Standard_Unsigned) then
+ return Standard_Unsigned;
+ elsif Siz = Esize (Standard_Long_Integer) then
+ return Standard_Long_Unsigned;
+ elsif Siz = Esize (Standard_Long_Long_Integer) then
+ return Standard_Long_Long_Unsigned;
+ else
+ raise Program_Error;
+ end if;
+ end Corresponding_Unsigned_Type;
+
-----------------------------
-- Enclosing_Dynamic_Scope --
-----------------------------
-- constants from the point of view of constant folding. Empty is also
-- returned for variables with no initialization expression.
+ function Corresponding_Unsigned_Type (Typ : Entity_Id) return Entity_Id;
+ -- Typ is a signed integer subtype. This routine returns the standard
+ -- unsigned type with the same Esize as the implementation base type of
+ -- Typ, e.g. Long_Integer => Long_Unsigned.
+
function Enclosing_Dynamic_Scope (Ent : Entity_Id) return Entity_Id;
-- For any entity, Ent, returns the closest dynamic scope in which the
-- entity is declared or Standard_Standard for library-level entities.
if In_Spec_Expression then
return;
- -- The ghost subprogram appears inside an assertion expression
- -- which is one of the allowed cases.
+ -- The ghost subprogram appears inside an assertion expression which
+ -- is one of the allowed cases.
- elsif In_Assertion_Expression (N) then
+ elsif In_Assertion_Expression_Pragma (N) then
return;
-- Otherwise see if it inside another ghost subprogram
Check_Mixed_Parameter_And_Named_Associations;
end if;
- -- Mark a function that appears inside an assertion expression
-
- if Nkind (N) = N_Function_Call and then In_Assertion_Expr > 0 then
- Set_In_Assertion_Expression (N);
- end if;
-
-- Initialize the type of the result of the call to the error type,
-- which will be reset if the type is successfully resolved.
-- within an assertion expression, since we can get false warnings
-- in this case, due to the out of order handling in this case.
- and then (Nkind (Original_Node (N)) /= N_Function_Call
- or else not In_Assertion_Expression (Original_Node (N)))
+ and then
+ (Nkind (Original_Node (N)) /= N_Function_Call
+ or else not In_Assertion_Expression_Pragma (Original_Node (N)))
then
Error_Msg_Warn := SPARK_Mode /= On;
package Sem_Prag is
+ -- The following table lists all pragmas that act as an assertion
+ -- expression.
+
+ Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
+ (Pragma_Assert => True,
+ Pragma_Assert_And_Cut => True,
+ Pragma_Assume => True,
+ Pragma_Check => True,
+ Pragma_Contract_Cases => True,
+ Pragma_Initial_Condition => True,
+ Pragma_Invariant => True,
+ Pragma_Loop_Invariant => True,
+ Pragma_Loop_Variant => True,
+ Pragma_Post => True,
+ Pragma_Post_Class => True,
+ Pragma_Postcondition => True,
+ Pragma_Pre => True,
+ Pragma_Pre_Class => True,
+ Pragma_Precondition => True,
+ Pragma_Predicate => True,
+ Pragma_Refined_Post => True,
+ Pragma_Test_Case => True,
+ Pragma_Type_Invariant => True,
+ Pragma_Type_Invariant_Class => True,
+ others => False);
+
-- The following table lists all the implementation-defined pragmas that
-- may apply to a body stub (no language defined pragmas apply). The table
-- should be synchronized with Aspect_On_Body_Or_Stub_OK in unit Aspects if
with Sem_Ch8; use Sem_Ch8;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sinfo; use Sinfo;
return False;
end Implements_Interface;
+ ------------------------------------
+ -- In_Assertion_Expression_Pragma --
+ ------------------------------------
+
+ function In_Assertion_Expression_Pragma (N : Node_Id) return Boolean is
+ Par : Node_Id;
+ Prag : Node_Id := Empty;
+
+ begin
+ -- Climb the parent chain looking for an enclosing pragma
+
+ Par := N;
+ while Present (Par) loop
+ if Nkind (Par) = N_Pragma then
+ Prag := Par;
+ exit;
+
+ -- Precondition-like pragmas are expanded into if statements, check
+ -- the original node instead.
+
+ elsif Nkind (Original_Node (Par)) = N_Pragma then
+ Prag := Original_Node (Par);
+ exit;
+
+ -- Prevent the search from going too far
+
+ elsif Is_Body_Or_Package_Declaration (Par) then
+ return False;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ return
+ Present (Prag)
+ and then Assertion_Expression_Pragma (Get_Pragma_Id (Prag));
+ end In_Assertion_Expression_Pragma;
+
-----------------
-- In_Instance --
-----------------
Expr := N;
Par := Parent (N);
while not Nkind_In (Par, N_If_Expression,
- N_Case_Expression,
- N_And_Then,
- N_Or_Else,
- N_In,
- N_Not_In)
+ N_Case_Expression,
+ N_And_Then,
+ N_Or_Else,
+ N_In,
+ N_Not_In)
loop
Expr := Par;
Par := Parent (Par);
Exclude_Parents : Boolean := False) return Boolean;
-- Returns true if the Typ_Ent implements interface Iface_Ent
+ function In_Assertion_Expression_Pragma (N : Node_Id) return Boolean;
+ -- Determine whether an arbitrary node appears in a pragma that acts as an
+ -- assertion expression. See Sem_Prag for the list of qualifying pragmas.
+
function In_Instance return Boolean;
-- Returns True if the current scope is within a generic instance
return Flag16 (N);
end Import_Interface_Present;
- function In_Assertion_Expression
- (N : Node_Id) return Boolean is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Function_Call);
- return Flag4 (N);
- end In_Assertion_Expression;
-
function In_Present
(N : Node_Id) return Boolean is
begin
Set_Flag16 (N, Val);
end Set_Import_Interface_Present;
- procedure Set_In_Assertion_Expression
- (N : Node_Id; Val : Boolean := True) is
- begin
- pragma Assert (False
- or else NT (N).Nkind = N_Function_Call);
- Set_Flag4 (N, Val);
- end Set_In_Assertion_Expression;
-
procedure Set_In_Present
(N : Node_Id; Val : Boolean := True) is
begin
-- pragma of the other kind is also present. This is used to avoid
-- generating some unwanted error messages.
- -- In_Assertion_Expression (Flag4-Sem)
- -- This flag is present in N_Function_Call nodes. It is set if the
- -- function is called from within an assertion expression. This is
- -- used to avoid some bogus warnings about early elaboration.
-
-- Includes_Infinities (Flag11-Sem)
-- This flag is present in N_Range nodes. It is set for the range of
-- unconstrained float types defined in Standard, which include not only
-- actual parameter part)
-- First_Named_Actual (Node4-Sem)
-- Controlling_Argument (Node1-Sem) (set to Empty if not dispatching)
- -- In_Assertion_Expression (Flag4-Sem)
-- Is_Expanded_Build_In_Place_Call (Flag11-Sem)
-- Do_Tag_Check (Flag13-Sem)
-- No_Elaboration_Check (Flag14-Sem)
function Import_Interface_Present
(N : Node_Id) return Boolean; -- Flag16
- function In_Assertion_Expression
- (N : Node_Id) return Boolean; -- Flag4
-
function In_Present
(N : Node_Id) return Boolean; -- Flag15
procedure Set_Import_Interface_Present
(N : Node_Id; Val : Boolean := True); -- Flag16
- procedure Set_In_Assertion_Expression
- (N : Node_Id; Val : Boolean := True); -- Flag4
-
procedure Set_In_Present
(N : Node_Id; Val : Boolean := True); -- Flag15
pragma Inline (Interface_Present);
pragma Inline (Includes_Infinities);
pragma Inline (Import_Interface_Present);
- pragma Inline (In_Assertion_Expression);
pragma Inline (In_Present);
pragma Inline (Inherited_Discriminant);
pragma Inline (Instance_Spec);
pragma Inline (Set_Identifier);
pragma Inline (Set_Implicit_With);
pragma Inline (Set_Import_Interface_Present);
- pragma Inline (Set_In_Assertion_Expression);
pragma Inline (Set_In_Present);
pragma Inline (Set_Includes_Infinities);
pragma Inline (Set_Inherited_Discriminant);
Tree_Read_Int (Int (Standard_Integer_16));
Tree_Read_Int (Int (Standard_Integer_32));
Tree_Read_Int (Int (Standard_Integer_64));
+ Tree_Read_Int (Int (Standard_Unsigned_64));
+ Tree_Read_Int (Int (Standard_Short_Short_Unsigned));
+ Tree_Read_Int (Int (Standard_Short_Unsigned));
+ Tree_Read_Int (Int (Standard_Unsigned));
+ Tree_Read_Int (Int (Standard_Long_Unsigned));
+ Tree_Read_Int (Int (Standard_Long_Long_Unsigned));
Tree_Read_Int (Int (Abort_Signal));
Tree_Read_Int (Int (Standard_Op_Rotate_Left));
Tree_Read_Int (Int (Standard_Op_Rotate_Right));
Tree_Write_Int (Int (Standard_Integer_16));
Tree_Write_Int (Int (Standard_Integer_32));
Tree_Write_Int (Int (Standard_Integer_64));
+ Tree_Write_Int (Int (Standard_Unsigned_64));
+ Tree_Write_Int (Int (Standard_Short_Short_Unsigned));
+ Tree_Write_Int (Int (Standard_Short_Unsigned));
+ Tree_Write_Int (Int (Standard_Unsigned));
+ Tree_Write_Int (Int (Standard_Long_Unsigned));
+ Tree_Write_Int (Int (Standard_Long_Long_Unsigned));
Tree_Write_Int (Int (Abort_Signal));
Tree_Write_Int (Int (Standard_Op_Rotate_Left));
Tree_Write_Int (Int (Standard_Op_Rotate_Right));
-- These are signed integer types with the indicated sizes. Used for the
-- underlying implementation types for fixed-point and enumeration types.
- Standard_Unsigned : Entity_Id;
- -- An unsigned type of the same size as Standard_Integer
+ Standard_Short_Short_Unsigned : Entity_Id;
+ Standard_Short_Unsigned : Entity_Id;
+ Standard_Unsigned : Entity_Id;
+ Standard_Long_Unsigned : Entity_Id;
+ Standard_Long_Long_Unsigned : Entity_Id;
+ -- Unsigned types with same Esize as corresponding signed integer types
Standard_Unsigned_64 : Entity_Id;
-- An unsigned type, mod 2 ** 64, size of 64 bits.