+2011-08-01 Yannick Moy <moy@adacore.com>
+
+ * par-ch4.adb (P_Name): issue a syntax error in SPARK mode on character
+ literal or operator symbol which is prefixed
+ * sem_attr.adb (Analyze_Access_Attribute): issue an error in formal
+ mode on access attributes.
+ * sem_ch4.adb (Analyze_Concatenation_Operand): new procedure to check
+ that concatenation operands are properly restricted in formal mode
+ (Analyze_Concatenation, Analyze_Concatenation_Rest): call new procedure
+ Analyze_Concatenation_Operand. Issue an error in formal mode if the
+ result of the concatenation has a type different from String.
+ (Analyze_Conditional_Expression, Analyze_Explicit_Dereference,
+ Analyze_Quantified_Expression, Analyze_Slice,
+ Analyze_Null): issue an error in formal mode on unsupported constructs
+ * sem_ch5.adb
+ (Analyze_Block_Statement): only issue error on source block statement
+ * sem_util.ads, sem_util.adb (Last_Source_Node_In_Sequence): new
+ function which returns the last node in a list of nodes for which
+ Comes_From_Source returns True, if any
+ * sem_ch6.adb (Check_Missing_Return): minor refactoring to use
+ Last_Source_Node_In_Sequence
+ * sem_ch8.adb (Analyze_Exception_Renaming, Analyze_Generic_Renaming,
+ Analyze_Object_Renaming, Analyze_Use_Package): issue an error in formal
+ mode on unsupported constructs
+ * sem_ch9.adb Do not return after issuing error in formal mode, as the
+ rest of the actions may be needed later on since the error is marked as
+ not serious.
+ * sinfo.ads: Typos in comments.
+
+2011-08-01 Pascal Obry <obry@adacore.com>
+
+ * projects.texi: Minor editing.
+
2011-08-01 Yannick Moy <moy@adacore.com>
* err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for
-- designator.
if Token not in Token_Class_Desig then
+
+ -- Selector name cannot be a character literal in SPARK
+
+ if SPARK_Mode and then Token = Tok_Char_Literal then
+ Error_Msg_SC ("|~~character literal cannot be prefixed");
+ end if;
+
goto Scan_Name_Extension_Dot;
else
+ -- Selector name cannot be an operator symbol in SPARK
+
+ if SPARK_Mode and then Token = Tok_Operator_Symbol then
+ Error_Msg_SC ("|~~operator symbol cannot be prefixed");
+ end if;
+
Prefix_Node := Name_Node;
Name_Node := New_Node (N_Selected_Component, Prev_Token_Ptr);
Set_Prefix (Name_Node, Prefix_Node);
The default output of GPRbuild's execution is kept reasonably simple and easy
to understand. In particular, some of the less frequently used commands are not
shown, and some parameters are abbreviated. So it is not possible to rerun the
-effect of the gprbuild command by cut-and-pasting its output. GPRbuild's option
-@code{-v} provides a much more verbose output which includes, among other
-information, more complete compilation, post-compilation and link commands.
+effect of the @command{gprbuild} command by cut-and-pasting its output.
+GPRbuild's option @code{-v} provides a much more verbose output which includes,
+among other information, more complete compilation, post-compilation and link
+commands.
@c ---------------------------------------------
@node Executable File Names
@itemize @bullet
@item First, the file is searched relative to the directory that contains the
current project file.
+
@item
@cindex @code{ADA_PROJECT_PATH}
@cindex @code{GPR_PROJECT_PATH}
^environment variables^logical names^ @b{GPR_PROJECT_PATH} and
@b{ADA_PROJECT_PATH} (in that order) if they exist. The former is
recommended, the latter is kept for backward compatibility.
+
@item Finally, it is searched relative to the default project directories.
- Such directories depends on the tool used. For @command{gnatmake}, there is
- one default project directory: @file{<prefix>/lib/gnat/}. In our example,
- @file{gtkada.gpr} is found in the predefined directory if it was installed at
- the same root as GNAT.
+ Such directories depends on the tool used. The different locations searched
+ in the specified order are:
+
+ @itemize @bullet
+ @item @file{<prefix>/<target>/lib/gnat}
+ (for @command{gprbuild} only and if option @option{--target} is specified)
+ @item @file{<prefix>/share/gpr/}
+ (for @command{gnatmake} and @command{gprbuild})
+ @item @file{<prefix>/lib/gnat/}
+ (for @command{gnatmake} and @command{gprbuild})
+ @end itemize
+ In our example, @file{gtkada.gpr} is found in the predefined directory if
+ it was installed at the same root as GNAT.
@end itemize
@noindent
-- Start of processing for Analyze_Access_Attribute
begin
+ -- Access attribute is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode and then Comes_From_Source (N) then
+ Error_Attr_P ("|~~% attribute is not allowed");
+ end if;
+
+ -- Proceed with analysis
+
Check_E0;
if Nkind (P) = N_Character_Literal then
-- Local Subprograms --
-----------------------
+ procedure Analyze_Concatenation_Operand (N : Node_Id);
+ -- Checks that concatenation operands are properly restricted in SPARK or
+ -- ALFA: each operand must be either a string literal, a static character
+ -- expression, or another concatenation.
+
procedure Analyze_Concatenation_Rest (N : Node_Id);
-- Does the "rest" of the work of Analyze_Concatenation, after the left
-- operand has been analyzed. See Analyze_Concatenation for details.
C : Node_Id;
begin
+ -- Allocator is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~allocator is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
-- Deal with allocator restrictions
-- In accordance with H.4(7), the No_Allocators restriction only applies
-- First analyze L ...
Analyze_Expression (L);
+ Analyze_Concatenation_Operand (L);
-- ... then walk NN back up until we reach N (where we started), calling
-- Analyze_Concatenation_Rest along the way.
exit when NN = N;
NN := Parent (NN);
end loop;
+
+ if Formal_Verification_Mode
+ and then Etype (N) /= Standard_String
+ then
+ Error_Msg_F ("|~~result of concatenation should have type String", N);
+ end if;
end Analyze_Concatenation;
+ -----------------------------------
+ -- Analyze_Concatenation_Operand --
+ -----------------------------------
+
+ -- Concatenation is restricted in SPARK or ALFA: each operand must be
+ -- either a string literal, a static character expression, or another
+ -- concatenation. N cannot be a concatenation here as Analyze_Concatenation
+ -- and Analyze_Concatenation_Rest call Analyze_Concatenation_Operand
+ -- separately on each final operand, past concatenation operations.
+
+ procedure Analyze_Concatenation_Operand (N : Node_Id) is
+ begin
+ if Formal_Verification_Mode then
+ if Is_Character_Type (Etype (N)) then
+ if not Is_Static_Expression (N) then
+ Error_Msg_F ("|~~character operand for concatenation should be "
+ & "static", N);
+ end if;
+ elsif Is_String_Type (Etype (N)) then
+ if Nkind (N) /= N_String_Literal then
+ Error_Msg_F ("|~~string operand for concatenation should be "
+ & "a literal", N);
+ end if;
+
+ -- Do not issue error on an operand that is neither a character nor
+ -- a string, as the error is issued in Analyze_Concatenation_Rest.
+
+ end if;
+ end if;
+ end Analyze_Concatenation_Operand;
+
--------------------------------
-- Analyze_Concatenation_Rest --
--------------------------------
begin
Analyze_Expression (R);
+ Analyze_Concatenation_Operand (R);
-- If the entity is present, the node appears in an instance, and
-- denotes a predefined concatenation operation. The resulting type is
return;
end if;
+ -- Conditional expression is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~conditional expression is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Else_Expr := Next (Then_Expr);
if Comes_From_Source (N) then
-- Start of processing for Analyze_Explicit_Dereference
begin
+ -- Explicit dereference is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~explicit dereference is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Analyze (P);
Set_Etype (N, Any_Type);
procedure Analyze_Null (N : Node_Id) is
begin
+ -- Null is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~null is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Set_Etype (N, Any_Access);
end Analyze_Null;
Iterator : Node_Id;
begin
+ -- Quantified expression is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~quantified expression is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Set_Etype (Ent, Standard_Void_Type);
Set_Parent (Ent, N);
-- Start of processing for Analyze_Slice
begin
+ -- Slice is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~slice is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Analyze (P);
Analyze (D);
begin
-- Block statement is not allowed in SPARK or ALFA
- if Formal_Verification_Mode then
+ if Formal_Verification_Mode
+ and then Comes_From_Source (N)
+ then
Error_Msg_F ("|~~block statement is not allowed", N);
end if;
if Formal_Verification_Mode then
declare
- Stat : Node_Id := Last (Statements (HSS));
+ Stat : constant Node_Id :=
+ Last_Source_Node_In_Sequence (Statements (HSS));
begin
- while Present (Stat) loop
- if Comes_From_Source (Stat) then
- if not Nkind_In (Nkind (Stat),
- N_Simple_Return_Statement,
- N_Extended_Return_Statement)
- then
- Error_Msg_F ("|~~last statement in function "
- & "should be RETURN", N);
- end if;
- exit;
- end if;
-
- -- Reach before the generated statements at the end of
- -- the function.
-
- Stat := Prev (Stat);
- end loop;
+ if Present (Stat)
+ and then not Nkind_In (Nkind (Stat),
+ N_Simple_Return_Statement,
+ N_Extended_Return_Statement)
+ then
+ Error_Msg_F ("|~~last statement in function should "
+ & "be RETURN", Stat);
+ end if;
end;
elsif Return_Present (Id) then
-- private with on E.
procedure Find_Expanded_Name (N : Node_Id);
- -- The input is a selected component is known to be expanded name. Verify
+ -- The input is a selected component known to be an expanded name. Verify
-- legality of selector given the scope denoted by prefix, and change node
-- N into a expanded name with a properly set Entity field.
Nam : constant Node_Id := Name (N);
begin
+ -- Exception renaming is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~exception renaming is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
Enter_Name (Id);
Analyze (Nam);
Inst : Boolean := False; -- prevent junk warning
begin
+ -- Generic renaming is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~generic renaming is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
if Name (N) = Error then
return;
end if;
-- Start of processing for Analyze_Object_Renaming
begin
+ -- Object renaming is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~object renaming is not allowed", N);
+ end if;
+
+ -- Proceed with analysis
+
if Nam = Error then
return;
end if;
-- Start of processing for Analyze_Use_Package
begin
+ -- Use package is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode then
+ Error_Msg_F ("|~~use clause is not allowed", N);
+ return;
+ end if;
+
+ -- Proceed with analysis
+
Set_Hidden_By_Use_Clause (N, No_Elist);
-- Use clause is not allowed in a spec of a predefined package
elsif Is_Entity_Name (P) then
P_Name := Entity (P);
+ -- Selector name is restricted in SPARK
+
+ if SPARK_Mode then
+ if Is_Subprogram (P_Name) then
+ Error_Msg_F
+ ("|~~prefix of expanded name cannot be a subprogram", P);
+ elsif Ekind (P_Name) = E_Loop then
+ Error_Msg_F
+ ("|~~prefix of expanded name cannot be a loop statement", P);
+ end if;
+ end if;
+
-- The prefix may denote an enclosing type which is the completion
-- of an incomplete type declaration.
if Formal_Verification_Mode then
Error_Msg_F ("|~~abort statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~accept statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~select statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~select statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~delay statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~delay statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~entry call is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~requeue statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~select statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
if Formal_Verification_Mode then
Error_Msg_F ("|~~select statement is not allowed", N);
- return;
end if;
-- Proceed with analysis
end case;
end Known_To_Be_Assigned;
+ ----------------------------------
+ -- Last_Source_Node_In_Sequence --
+ ----------------------------------
+
+ function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id is
+ N : Node_Id := Last (List);
+ begin
+ while Present (N) loop
+ exit when Comes_From_Source (N);
+
+ -- Reach before the generated statements at the end of the function
+
+ N := Prev (N);
+ end loop;
+
+ return N;
+ end Last_Source_Node_In_Sequence;
+
-------------------
-- May_Be_Lvalue --
-------------------
-- direction. Cases which may possibly be assignments but are not known to
-- be may return True from May_Be_Lvalue, but False from this function.
+ function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id;
+ -- Returns the last node in List for which Comes_From_Source returns True,
+ -- if any, or Empty otherwise.
+
function Make_Simple_Return_Statement
(Sloc : Source_Ptr;
Expression : Node_Id := Empty) return Node_Id
-- This node is created by the analyzer/expander to handle some
-- expansion cases, notably short circuit forms where there are
- -- actions associated with the right hand operand.
+ -- actions associated with the right-hand side operand.
-- The N_Expression_With_Actions node represents an expression with
-- an associated set of actions (which are executable statements and
-- executing all the actions.
-- Note: if the actions contain declarations, then these declarations
- -- maybe referenced with in the expression. It is thus appropriate for
- -- the back end to create a scope that encompasses the construct (any
+ -- may be referenced within the expression. It is thus appropriate for
+ -- the back-end to create a scope that encompasses the construct (any
-- declarations within the actions will definitely not be referenced
-- once elaboration of the construct is completed).
projects / gcc.git / commitdiff