+2012-08-06 Robert Dewar <dewar@adacore.com>
+
+ * aspects.ads: Define Aspect_Id_Exclude_No_Aspect.
+ * par-ch13.adb, restrict.adb: Use Aspect_Id_Exclude_No_Aspect to
+ simplify code.
+
+2012-08-06 Yannick Moy <moy@adacore.com>
+
+ * gnat-style.texi: Update style guide for declarations.
+
+2012-08-06 Yannick Moy <moy@adacore.com>
+
+ * sem_attr.adb (Analyze_Attribute): In the case for 'Old,
+ skip a special expansion which is not needed in Alfa mode.
+
+2012-08-06 Yannick Moy <moy@adacore.com>
+
+ * sem_ch5.adb (Analyze_Iterator_Specification): Do not perform
+ an expansion of the iterator in Alfa mode.
+
2012-08-06 Robert Dewar <dewar@adacore.com>
* s-oscons-tmplt.c, sem_ch9.adb, osint.adb: Minor reformatting.
Aspect_Lock_Free);
+ subtype Aspect_Id_Exclude_No_Aspect is
+ Aspect_Id range Aspect_Id'Succ (No_Aspect) .. Aspect_Id'Last;
+ -- Aspect_Id's excluding No_Aspect
+
-- The following array indicates aspects that accept 'Class
Class_Aspect_OK : constant array (Aspect_Id) of Boolean :=
@c o
@c G N A T C O D I N G S T Y L E o
@c o
-@c GNAT is maintained by Ada Core Technologies Inc (http://www.gnat.com). o
+@c Copyright (C) 1992-2012, AdaCore o
@c o
@c oooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooo
@setfilename gnat-style.info
@copying
-Copyright @copyright{} 1992-2008, Free Software Foundation, Inc.
+Copyright @copyright{} 1992-2012, AdaCore
Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License, Version 1.3 or
Local names can be shorter, because they are used only within
one context, where comments explain their purpose.
+@item
+When starting a default expression on the line that follows the declaration
+line, use 2 characters for indentation.
+
+@smallexample @c adanocomment
+ Entity1 : Integer :=
+ Function_Name (Parameters, For_Call);
+@end smallexample
+
+@item
+If a default expression needs to be continued on subsequent lines, the
+continuations should be indented from the start of the expression.
+
+@smallexample @c adanocomment
+ Entity1 : Integer := Long_Function_Name
+ (parameters for call);
+@end smallexample
+
@end itemize
-- Check bad spelling
- for J in Aspect_Id loop
- if J /= No_Aspect and then
- Is_Bad_Spelling_Of (Token_Name, Aspect_Names (J))
- then
+ for J in Aspect_Id_Exclude_No_Aspect loop
+ if Is_Bad_Spelling_Of (Token_Name, Aspect_Names (J)) then
Error_Msg_Name_1 := Aspect_Names (J);
Error_Msg_SC -- CODEFIX
("\possible misspelling of%");
(N : Node_Id;
Warning : Boolean)
is
- A_Id : constant Aspect_Id := Get_Aspect_Id (Chars (N));
- pragma Assert (A_Id /= No_Aspect);
+ A_Id : constant Aspect_Id_Exclude_No_Aspect := Get_Aspect_Id (Chars (N));
begin
No_Specification_Of_Aspects (A_Id) := Sloc (N);
-- enclosing subprogram. This is properly an expansion activity
-- but it has to be performed now to prevent out-of-order issues.
- if not Is_Entity_Name (P) then
+ -- This expansion is both harmful and not needed in Alfa mode, since
+ -- the formal verification backend relies on the types of nodes
+ -- (hence is not robust w.r.t. a change to base type here), and does
+ -- not suffer from the out-of-order issue described above. Thus, this
+ -- expansion is skipped in Alfa mode.
+
+ if not Is_Entity_Name (P) and then not Alfa_Mode then
P_Type := Base_Type (P_Type);
Set_Etype (N, P_Type);
Set_Etype (P, P_Type);
-- If the domain of iteration is an expression, create a declaration for
-- it, so that finalization actions are introduced outside of the loop.
-- The declaration must be a renaming because the body of the loop may
- -- assign to elements. When the context is a quantified expression, the
- -- renaming declaration is delayed until the expansion phase.
+ -- assign to elements.
if not Is_Entity_Name (Iter_Name)
+
+ -- When the context is a quantified expression, the renaming
+ -- declaration is delayed until the expansion phase if we are
+ -- doing expansion.
+
and then (Nkind (Parent (N)) /= N_Quantified_Expression
+ or else Operating_Mode = Check_Semantics)
- -- The following two tests need comments ???
+ -- Do not perform this expansion in Alfa mode, since the formal
+ -- verification directly deals with the source form of the iterator.
- or else Operating_Mode = Check_Semantics
- or else Alfa_Mode)
+ and then not Alfa_Mode
then
declare
Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
-- Container is an entity or an array with uncontrolled components, or
-- else it is a container iterator given by a function call, typically
-- called Iterate in the case of predefined containers, even though
- -- Iterate is not a reserved name. What matter is that the return type
+ -- Iterate is not a reserved name. What matters is that the return type
-- of the function is an iterator type.
elsif Is_Entity_Name (Iter_Name) then
projects / gcc.git / commitdiff