+2014-01-20 Robert Dewar <dewar@adacore.com>
+
+ * checks.adb: Make warnings on exceptions into errors in GNATprove mode.
+ * errout.adb: Implement [ and ] insertion characters.
+ * errout.ads: Document new [ and ] insertion characters.
+ * sem_ch12.adb, restrict.adb, frontend.adb, exp_ch7.adb: Minor
+ addition of ??? comment.
+ * lib-xref.adb, exp_util.adb, gnat1drv.adb: Minor reformatting
+ * exp_ch4.adb, sem_ch3.adb, sem_ch4.adb, sem_ch6.adb, sem_elab.adb,
+ sem_eval.adb, sem_res.adb, sem_util.adb, sem_attr.adb, sem_aggr.adb:
+ Make warnings on exceptions into errors in GNATprove mode.
+ * sem_dim.adb: Minor reformatting throughout Quote [ and ]
+ in error messages.
+
+2014-01-20 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch13.adb: Code clean up.
+
2014-01-20 Robert Dewar <dewar@adacore.com>
* errout.ads, errout.adb: Implement >? >x? >X? sequences in error
Loc : constant Source_Ptr := Sloc (Ck_Node);
Checks_On : constant Boolean :=
(not Index_Checks_Suppressed (Target_Typ))
- or else (not Length_Checks_Suppressed (Target_Typ));
+ or else (not Length_Checks_Suppressed (Target_Typ));
begin
+ -- Note: this means that we lose some useful warnings if the expander
+ -- is not active, and we also lose these warnings in SPARK mode ???
+
if not Expander_Active then
return;
end if;
-- Here we have the optimizable case, warn if not short-circuited
if K = N_Op_And or else K = N_Op_Or then
+ Error_Msg_Warn := not GNATprove_Mode;
+
case Check is
when Access_Check =>
- Error_Msg_N
- ("Constraint_Error may be raised (access check)??",
- Parent (Nod));
+ if GNATprove_Mode then
+ Error_Msg_N
+ ("Constraint_Error might have been raised (access check)",
+ Parent (Nod));
+ else
+ Error_Msg_N
+ ("Constraint_Error may be raised (access check)??",
+ Parent (Nod));
+ end if;
+
when Division_Check =>
- Error_Msg_N
- ("Constraint_Error may be raised (zero divide)??",
- Parent (Nod));
+ if GNATprove_Mode then
+ Error_Msg_N
+ ("Constraint_Error might have been raised (zero divide)",
+ Parent (Nod));
+ else
+ Error_Msg_N
+ ("Constraint_Error may be raised (zero divide)??",
+ Parent (Nod));
+ end if;
when others =>
raise Program_Error;
N_Discriminant_Specification =>
Apply_Compile_Time_Constraint_Error
(N => Expr,
- Msg => "(Ada 2005) null not allowed " &
- "in null-excluding components??",
+ Msg => "(Ada 2005) null not allowed "
+ & "in null-excluding components??",
Reason => CE_Null_Not_Allowed);
when N_Object_Declaration =>
Apply_Compile_Time_Constraint_Error
(N => Expr,
- Msg => "(Ada 2005) null not allowed " &
- "in null-excluding objects?",
+ Msg => "(Ada 2005) null not allowed "
+ & "in null-excluding objects?",
Reason => CE_Null_Not_Allowed);
when N_Parameter_Specification =>
Apply_Compile_Time_Constraint_Error
(N => Expr,
- Msg => "(Ada 2005) null not allowed " &
- "in null-excluding formals??",
+ Msg => "(Ada 2005) null not allowed "
+ & "in null-excluding formals??",
Reason => CE_Null_Not_Allowed);
when others =>
if not Inside_Init_Proc then
Apply_Compile_Time_Constraint_Error
- (N,
- "null value not allowed here??",
- CE_Access_Check_Failed);
+ (N, "null value not allowed here??", CE_Access_Check_Failed);
else
Insert_Action (N,
Make_Raise_Constraint_Error (Loc,
C : Character; -- Current character
P : Natural; -- Current index;
- procedure Set_Msg_Insertion_Warning;
- -- Deal with ? ?? ?x? ?X? insertion sequences (also < <? <x? <X?). The
- -- caller has already bumped the pointer past the initial ? or <.
+ procedure Set_Msg_Insertion_Warning (C : Character);
+ -- Deal with ? ?? ?x? ?X? insertion sequences (also < << <x< <X<). The
+ -- caller has already bumped the pointer past the initial ? or < and C
+ -- is set to this initial character (? or <).
-------------------------------
-- Set_Msg_Insertion_Warning --
-------------------------------
- procedure Set_Msg_Insertion_Warning is
+ procedure Set_Msg_Insertion_Warning (C : Character) is
begin
Warning_Msg_Char := ' ';
- if P <= Text'Last and then Text (P) = '?' then
+ if P <= Text'Last and then Text (P) = C then
if Warning_Doc_Switch then
Warning_Msg_Char := '?';
end if;
and then (Text (P) in 'a' .. 'z'
or else
Text (P) in 'A' .. 'Z')
- and then Text (P + 1) = '?'
+ and then Text (P + 1) = C
then
if Warning_Doc_Switch then
Warning_Msg_Char := Text (P);
null; -- already dealt with
when '?' =>
- Set_Msg_Insertion_Warning;
+ Set_Msg_Insertion_Warning ('?');
when '<' =>
-- is False, the call to Set_Msg_Insertion_Warning here does
-- no harm, since Warning_Msg_Char is ignored in that case.
- Set_Msg_Insertion_Warning;
+ Set_Msg_Insertion_Warning ('<');
when '|' =>
null; -- already dealt with
Set_Msg_Char (C);
end if;
+ -- '[' (will be/would have been raised at run time)
+
+ when '[' =>
+ if Is_Warning_Msg then
+ Set_Msg_Str ("will be raised at run time");
+ else
+ Set_Msg_Str ("would have been raised at run time");
+ end if;
+
+ -- ']' (may be/might have been raised at run time)
+
+ when ']' =>
+ if Is_Warning_Msg then
+ Set_Msg_Str ("may be raised at run time");
+ else
+ Set_Msg_Str ("might have been raised at run time");
+ end if;
+
-- Normal character with no special treatment
when others =>
-- Suppress "size too small" errors in CodePeer mode and SPARK mode,
-- since pragma Pack is also ignored in these configurations.
+ -- At least the comment is bogus, since you can have this message
+ -- with no pragma Pack in sight! ???
+
if CodePeer_Mode or GNATprove_Mode then
return True;
-- Insertion character < (Less Than: conditional warning message)
-- The character < appearing anywhere in a message is used for a
-- conditional error message. If Error_Msg_Warn is True, then the
- -- effect is the same as ? described above, and in particular <? and
- -- <X? have the effect of ?? and ?X? respectively. If Error_Msg_Warn
- -- is False, then the < <? or <X? sequence is ignored and the message
+ -- effect is the same as ? described above, and in particular << and
+ -- <X< have the effect of ?? and ?X? respectively. If Error_Msg_Warn
+ -- is False, then the < << or <X< sequence is ignored and the message
-- is treated as a error rather than a warning.
-- Insertion character A-Z (Upper case letter: Ada reserved word)
-- inserted to replace the ~ character. The string is inserted in the
-- literal form it appears, without any action on special characters.
+ -- Insertion character [ (Left bracket: will/would be raised at run time)
+ -- This is used in messages about exceptions being raised at run-time.
+ -- If the current message is a warning message, then if the code is
+ -- executed, the exception will be raised, and [ inserts:
+ --
+ -- will be raised at run time
+ --
+ -- If the current message is an error message, then it is an error
+ -- because the exception would have been raised and [ inserts:
+ --
+ -- would have been raised at run time
+ --
+ -- Typically the message contains a < insertion which means that the
+ -- message is a warning or error depending on Error_Msg_Warn. This is
+ -- most typically used in the context of messages which are normally
+ -- warnings, but are errors in GNATprove mode, corresponding to the
+ -- permission in the definition of SPARK that allows an implementation
+ -- to reject a program as illegal if a situation arises in which the
+ -- compiler can determine that it is certain that a run-time check
+ -- would have fail if the statement was executed.
+
+ -- Insertion character ] (Right bracket: may/might be raised at run time)
+ -- This is like [ except that the insertion messages say may/might,
+ -- instead of will/would.
+
----------------------------------------
-- Specialization of Messages for VMS --
----------------------------------------
procedure Raise_Accessibility_Error is
begin
+ Error_Msg_Warn := not GNATprove_Mode;
Rewrite (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Accessibility_Check_Failed));
Set_Etype (N, Target_Type);
- Error_Msg_N
- ("??accessibility check failure", N);
- Error_Msg_NE
- ("\??& will be raised at run time", N, Standard_Program_Error);
+ Error_Msg_N ("<<accessibility check failure", N);
+ Error_Msg_NE ("\<<& [", N, Standard_Program_Error);
end Raise_Accessibility_Error;
----------------------
-- Do not create finalization masters in SPARK mode because they result
-- in unwanted expansion.
+ -- More detail would be useful here ???
+
elsif GNATprove_Mode then
return;
end if;
-- may be constants that depend on the bounds of a string literal, both
-- standard string types and more generally arrays of characters.
- -- In GNATprove mode, we also need the more precise subtype to be set.
+ -- In GNATprove mode, we also need the more precise subtype to be set
if not (Expander_Active or GNATprove_Mode)
and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
-- Cleanup processing after completing main analysis
+ -- Comment needed for ASIS mode test and GNATprove mode test???
+
if Operating_Mode = Generate_Code
or else (Operating_Mode = Check_Semantics
and then (ASIS_Mode or GNATprove_Mode))
-- trees between specs compiled as part of a main unit or as part of
-- a with-clause.
+ -- Comment is incomplete, SPARK semantics rely on static mode no???
+
Dynamic_Elaboration_Checks := False;
-- Set STRICT mode for overflow checks if not set explicitly. This
-- Skip call to gigi
+ -- This debug flag is not documented, AARGH! ???
+
Debug_Flag_HH := True;
-- Enable assertions, since they give valuable extra information for
-- since representations are largely symbolic there.
if Back_End_Mode = Declarations_Only
- and then
- (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
- or else Main_Kind = N_Subunit
- or else Targparm.Frontend_Layout_On_Target
- or else Targparm.VM_Target /= No_VM)
+ and then
+ (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
+ or else Main_Kind = N_Subunit
+ or else Targparm.Frontend_Layout_On_Target
+ or else Targparm.VM_Target /= No_VM)
then
Sem_Ch13.Validate_Unchecked_Conversions;
Sem_Ch13.Validate_Address_Clauses;
or else
(GNATprove_Mode
- and then In_Extended_Main_Code_Unit (N)
- and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
+ and then In_Extended_Main_Code_Unit (N)
+ and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
then
null;
else
Actual_Typ := 'P';
end if;
+ -- Comment needed here for special SPARK code ???
+
if GNATprove_Mode then
Ref := Sloc (Nod);
Def := Sloc (Ent);
-- set in gnat1drv.adb so that we have consistency between each
-- compilation.
+ -- Just checking, SPARK does not allow restrictions to be set ???
+
if CodePeer_Mode or GNATprove_Mode then
return;
end if;
elsif Expr_Value (This_Low) /= Expr_Value (Aggr_Low (Dim)) then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("sub-aggregate low bound mismatch??", N);
- Error_Msg_N
- ("\Constraint_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("sub-aggregate low bound mismatch<<", N);
+ Error_Msg_N ("\Constraint_Error [<<", N);
end if;
end if;
Expr_Value (This_High) /= Expr_Value (Aggr_High (Dim))
then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("sub-aggregate high bound mismatch??", N);
- Error_Msg_N
- ("\Constraint_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("sub-aggregate high bound mismatch<<", N);
+ Error_Msg_N ("\Constraint_Error [<<", N);
end if;
end if;
end if;
if OK_BH and then OK_AH and then Val_BH < Val_AH then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("upper bound out of range??", AH);
- Error_Msg_N ("\Constraint_Error will be raised at run time??", AH);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("upper bound out of range<<", AH);
+ Error_Msg_N ("\Constraint_Error [<<", AH);
-- You need to set AH to BH or else in the case of enumerations
-- indexes we will not be able to resolve the aggregate bounds.
if OK_L and then Val_L > Val_AL then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("lower bound of aggregate out of range??", N);
- Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("lower bound of aggregate out of range<<", N);
+ Error_Msg_N ("\Constraint_Error [<<", N);
end if;
if OK_H and then Val_H < Val_AH then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("upper bound of aggregate out of range??", N);
- Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("upper bound of aggregate out of range<<", N);
+ Error_Msg_N ("\Constraint_Error [<<", N);
end if;
end Check_Bounds;
if Range_Len < Len then
Set_Raises_Constraint_Error (N);
- Error_Msg_N ("too many elements??", N);
- Error_Msg_N ("\Constraint_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("too many elements<<", N);
+ Error_Msg_N ("\Constraint_Error [<<", N);
end if;
end Check_Length;
Name_Simple_Storage_Pool_Type))
then
Error_Msg_Name_1 := Aname;
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_N ("cannot use % attribute for type with simple "
- & "storage pool??", N);
- Error_Msg_N
- ("\Program_Error will be raised at run time??", N);
+ & "storage pool<<", N);
+ Error_Msg_N ("\Program_Error [<<", N);
Rewrite
(N, Make_Raise_Program_Error
-- know will fail, so generate an appropriate warning.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_F
- ("??non-local pointer cannot point to local object", P);
- Error_Msg_F
- ("\??Program_Error will be raised at run time", P);
+ ("non-local pointer cannot point to local object<<", P);
+ Error_Msg_F ("\Program_Error [<<", P);
Rewrite (N,
Make_Raise_Program_Error (Loc,
Reason => PE_Accessibility_Check_Failed));
-- know will fail, so generate an appropriate warning.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_F
- ("??non-local pointer cannot point to local object", P);
- Error_Msg_F
- ("\??Program_Error will be raised at run time", P);
+ ("non-local pointer cannot point to local object<<", P);
+ Error_Msg_F ("\Program_Error [<<", P);
+
Rewrite (N,
Make_Raise_Program_Error (Loc,
Reason => PE_Accessibility_Check_Failed));
and then not Is_Actual_Pack
and then not Inline_Now
and then (Operating_Mode = Generate_Code
+
+ -- Need comment for this check ???
+
or else (Operating_Mode = Check_Semantics
and then (ASIS_Mode or GNATprove_Mode)));
Set_Parent (Exp, N);
Preanalyze_Assert_Expression (Exp, Standard_Boolean);
+ -- In ASIS mode, even if assertions are not enabled, we must
+ -- analyze the original expression in the aspect specification
+ -- because it is part of the original tree.
+
+ if ASIS_Mode then
+ declare
+ Inv : constant Node_Id :=
+ Expression (Corresponding_Aspect (Ritem));
+ begin
+ Replace_Type_References (Inv, Chars (T));
+ Preanalyze_Assert_Expression (Inv, Standard_Boolean);
+ end;
+ end if;
+
-- Build first two arguments for Check pragma
Assoc := New_List (
and then Present (Get_Attribute_Definition_Clause
(E, Attribute_Address))
then
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_N
- ("??more than one task with same entry address", N);
- Error_Msg_N
- ("\??Program_Error will be raised at run time", N);
+ ("more than one task with same entry address<<", N);
+ Error_Msg_N ("\Program_Error [<<", N);
Insert_Action (N,
Make_Raise_Program_Error (Loc,
Reason => PE_Duplicated_Entry_Address));
Set_Etype (Sel, Etype (Comp));
Set_Etype (N, Etype (Comp));
- -- Emit appropriate message. Gigi will replace the
- -- node subsequently with the appropriate Raise.
+ -- Emit appropriate message. Gigi will replace the node
+ -- subsequently with the appropriate Raise.
-- In SPARK mode, this is made into an error to simplify
-- the processing of the formal verification backend.
- if GNATprove_Mode then
- Apply_Compile_Time_Constraint_Error
- (N, "component not present in }",
- CE_Discriminant_Check_Failed,
- Ent => Prefix_Type, Rep => False);
- else
- Apply_Compile_Time_Constraint_Error
- (N, "component not present in }??",
- CE_Discriminant_Check_Failed,
- Ent => Prefix_Type, Rep => False);
- end if;
+ Error_Msg_Warn := not GNATprove_Mode;
+ Apply_Compile_Time_Constraint_Error
+ (N, "component not present in }<<",
+ CE_Discriminant_Check_Failed,
+ Ent => Prefix_Type, Rep => False);
Set_Raises_Constraint_Error (N);
return;
Reason => PE_Accessibility_Check_Failed));
Analyze (N);
- Error_Msg_N
- ("cannot return a local value by reference??", N);
- Error_Msg_NE
- ("\& will be raised at run time??",
- N, Standard_Program_Error);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("cannot return a local value by reference<<", N);
+ Error_Msg_NE ("\& [<<", N, Standard_Program_Error);
end if;
end if;
-- In GNATprove mode, it is an error to have a missing return
- if GNATprove_Mode then
- Error_Msg_N
- ("RETURN statement missing following this statement!",
- Last_Stm);
-
- -- Otherwise normal case of warning (RM insists this is legal)
-
- else
- Error_Msg_N
- ("RETURN statement missing following this statement??!",
- Last_Stm);
- Error_Msg_N
- ("\Program_Error may be raised at run time??!",
- Last_Stm);
- end if;
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N
+ ("RETURN statement missing following this statement<<!",
+ Last_Stm);
+ Error_Msg_N
+ ("\Program_Error ]<<!", Last_Stm);
end if;
-- Note: we set Err even though we have not issued a warning
else
if not Raise_Exception_Call then
- Error_Msg_N
- ("implied return after this statement " &
- "will raise Program_Error??",
- Last_Stm);
+ if GNATprove_Mode then
+ Error_Msg_N
+ ("implied return after this statement "
+ & "would have raised Program_Error", Last_Stm);
+ else
+ Error_Msg_N
+ ("implied return after this statement "
+ & "will raise Program_Error??", Last_Stm);
+ end if;
+
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_NE
- ("\procedure & is marked as No_Return??!",
- Last_Stm, Proc);
+ ("\procedure & is marked as No_Return<<!", Last_Stm, Proc);
end if;
declare
type Name_Array is
array (Dimension_Position range
Low_Position_Bound .. High_Position_Bound) of Name_Id;
- -- A data structure used to store the names of all units within a system
+ -- Store the names of all units within a system
No_Names : constant Name_Array := (others => No_Name);
type Symbol_Array is
array (Dimension_Position range
Low_Position_Bound .. High_Position_Bound) of String_Id;
- -- A data structure used to store the symbols of all units within a system
+ -- Store the symbols of all units within a system
No_Symbols : constant Symbol_Array := (others => No_String);
(N : Node_Id;
Description_Needed : Boolean := False) return String;
-- Given a node N, return the dimension symbols of N, preceded by "has
- -- dimension" if Description_Needed. if N is dimensionless, return "[]", or
- -- "is dimensionless" if Description_Needed.
+ -- dimension" if Description_Needed. if N is dimensionless, return "'[']",
+ -- or "is dimensionless" if Description_Needed.
procedure Dim_Warning_For_Numeric_Literal (N : Node_Id; Typ : Entity_Id);
- -- Issue a warning on the given numeric literal N to indicate the
- -- compilateur made the assumption that the literal is not dimensionless
+ -- Issue a warning on the given numeric literal N to indicate that the
+ -- compiler made the assumption that the literal is not dimensionless
-- but has the dimension of Typ.
procedure Eval_Op_Expon_With_Rational_Exponent
-- Given a dimension vector and a dimension system, return the proper
-- string of dimension symbols. If In_Error_Msg is True (i.e. the String_Id
-- will be used to issue an error message) then this routine has a special
- -- handling for the insertion character asterisk * which must be precede by
+ -- handling for the insertion characters * or [ which must be preceded by
-- a quote ' to to be placed literally into the message.
function From_Dim_To_Str_Of_Unit_Symbols
function "+" (Right : Whole) return Rational is
begin
- return Rational'(Numerator => Right,
- Denominator => 1);
+ return Rational'(Numerator => Right, Denominator => 1);
end "+";
function "+" (Left, Right : Rational) return Rational is
R : constant Rational :=
- Rational'(Numerator => Left.Numerator * Right.Denominator +
- Left.Denominator * Right.Numerator,
- Denominator => Left.Denominator * Right.Denominator);
+ Rational'(Numerator => Left.Numerator * Right.Denominator +
+ Left.Denominator * Right.Numerator,
+ Denominator => Left.Denominator * Right.Denominator);
begin
return Reduce (R);
end "+";
function "-" (Right : Rational) return Rational is
begin
- return Rational'(Numerator => -Right.Numerator,
+ return Rational'(Numerator => -Right.Numerator,
Denominator => Right.Denominator);
end "-";
function "-" (Left, Right : Rational) return Rational is
R : constant Rational :=
- Rational'(Numerator => Left.Numerator * Right.Denominator -
- Left.Denominator * Right.Numerator,
+ Rational'(Numerator => Left.Numerator * Right.Denominator -
+ Left.Denominator * Right.Numerator,
Denominator => Left.Denominator * Right.Denominator);
begin
function "*" (Left, Right : Rational) return Rational is
R : constant Rational :=
- Rational'(Numerator => Left.Numerator * Right.Numerator,
+ Rational'(Numerator => Left.Numerator * Right.Numerator,
Denominator => Left.Denominator * Right.Denominator);
begin
return Reduce (R);
L.Numerator := Whole (-Integer (L.Numerator));
end if;
- return Reduce (Rational'(Numerator => L.Numerator * R.Denominator,
+ return Reduce (Rational'(Numerator => L.Numerator * R.Denominator,
Denominator => L.Denominator * R.Numerator));
end "/";
function "abs" (Right : Rational) return Rational is
begin
- return Rational'(Numerator => abs Right.Numerator,
+ return Rational'(Numerator => abs Right.Numerator,
Denominator => Right.Denominator);
end "abs";
-- Integer case
if Is_Integer_Type (Def_Id) then
+
-- Dimension value must be an integer literal
if Nkind (Expr) = N_Integer_Literal then
N_String_Literal)
then
Num_Choices := Num_Choices + 1;
- Error_Msg_N ("optional component Symbol expected, found&",
- Choice);
+ Error_Msg_N
+ ("optional component Symbol expected, found&", Choice);
end if;
end if;
end if;
if Present (First (Expressions (Aggr)))
and then (First (Expressions (Aggr)) /= Symbol_Expr
- or else Present (Next (Symbol_Expr)))
+ or else Present (Next (Symbol_Expr)))
and then (Num_Choices > 1
or else (Num_Choices = 1 and then not Others_Seen))
then
Position := Position + 1;
if Position > High_Position_Bound then
- Error_Msg_N
- ("too many dimensions in system", Aggr);
+ Error_Msg_N ("too many dimensions in system", Aggr);
exit;
end if;
and then List_Length (Expressions (Dim_Aggr)) /= 3
then
Error_Msg_N
- ("three components expected in aggregate", Dim_Aggr);
+ ("three components expected in aggregate", Dim_Aggr);
else
-- Named dimension aggregate
or else Nkind (Choice) /= N_Identifier
then
Error_Msg_NE ("wrong syntax for aspect&", Choice, Id);
-
elsif Chars (Choice) /= Name_Dim_Symbol then
Error_Msg_N ("expected Dim_Symbol, found&", Choice);
end if;
-- Verify that the string is not empty
if String_Length (Dim_Symbols (Position)) = 0 then
- Error_Msg_N
- ("empty string not allowed here", Dim_Symbol);
+ Error_Msg_N ("empty string not allowed here", Dim_Symbol);
end if;
end if;
end if;
end if;
Error_Msg_N
- ("\expected dimension "
- & Dimensions_Msg_Of (Comp_Typ)
- & ", found "
- & Dimensions_Msg_Of (Expr),
- Expr);
+ ("\expected dimension " & Dimensions_Msg_Of (Comp_Typ)
+ & ", found " & Dimensions_Msg_Of (Expr), Expr);
end if;
-- Look at the named components right after the positional components
procedure Error_Dim_Msg_For_Binary_Op (N, L, R : Node_Id) is
begin
- Error_Msg_NE ("both operands for operation& must have same " &
- "dimensions",
- N,
- Entity (N));
+ Error_Msg_NE
+ ("both operands for operation& must have same dimensions",
+ N, Entity (N));
Error_Msg_N ("\left operand " & Dimensions_Msg_Of (L, True), N);
Error_Msg_N ("\right operand " & Dimensions_Msg_Of (R, True), N);
end Error_Dim_Msg_For_Binary_Op;
or else N_Kind in N_Op_Compare
then
declare
- L : constant Node_Id := Left_Opnd (N);
+ L : constant Node_Id := Left_Opnd (N);
Dims_Of_L : constant Dimension_Type := Dimensions_Of (L);
- L_Has_Dimensions : constant Boolean := Exists (Dims_Of_L);
- R : constant Node_Id := Right_Opnd (N);
+ L_Has_Dimensions : constant Boolean := Exists (Dims_Of_L);
+ R : constant Node_Id := Right_Opnd (N);
Dims_Of_R : constant Dimension_Type := Dimensions_Of (R);
- R_Has_Dimensions : constant Boolean := Exists (Dims_Of_R);
- Dims_Of_N : Dimension_Type := Null_Dimension;
+ R_Has_Dimensions : constant Boolean := Exists (Dims_Of_R);
+ Dims_Of_N : Dimension_Type := Null_Dimension;
begin
-- N_Op_Add, N_Op_Mod, N_Op_Rem or N_Op_Subtract case
if L_Has_Dimensions then
if not Compile_Time_Known_Value (R) then
- Error_Msg_N ("exponent of dimensioned operand must be " &
- "known at compile time", N);
+ Error_Msg_N
+ ("exponent of dimensioned operand must be "
+ & "known at compile time", N);
end if;
declare
-- Check if error has already been encountered
if not Error_Detected then
- Error_Msg_NE ("dimensions mismatch in call of&",
- N, Name (N));
+ Error_Msg_NE
+ ("dimensions mismatch in call of&",
+ N, Name (N));
Error_Detected := True;
end if;
- Error_Msg_N ("\expected dimension [], found " &
- Dimensions_Msg_Of (Actual),
- Actual);
+ Error_Msg_N
+ ("\expected dimension '['], found "
+ & Dimensions_Msg_Of (Actual), Actual);
end if;
Next_Actual (Actual);
Actual := First_Actual (N);
Formal := First_Formal (Nam);
-
while Present (Formal) loop
-- A missing corresponding actual indicates that the analysis of
Expr : Node_Id) is
begin
Error_Msg_N ("dimensions mismatch in component declaration", N);
- Error_Msg_N ("\expected dimension "
- & Dimensions_Msg_Of (Etyp)
- & ", found "
- & Dimensions_Msg_Of (Expr),
- Expr);
+ Error_Msg_N
+ ("\expected dimension " & Dimensions_Msg_Of (Etyp) & ", found "
+ & Dimensions_Msg_Of (Expr), Expr);
end Error_Dim_Msg_For_Component_Declaration;
-- Start of processing for Analyze_Dimension_Component_Declaration
-- Check dimensions match
if Dims_Of_Etyp /= Dims_Of_Expr then
+
-- Numeric literal case. Issue a warning if the object type is not
-- dimensionless to indicate the literal is treated as if its
-- dimension matches the type dimension.
procedure Analyze_Dimension_Extended_Return_Statement (N : Node_Id) is
Return_Ent : constant Entity_Id := Return_Statement_Entity (N);
Return_Etyp : constant Entity_Id :=
- Etype (Return_Applies_To (Return_Ent));
+ Etype (Return_Applies_To (Return_Ent));
Return_Obj_Decls : constant List_Id := Return_Object_Declarations (N);
Return_Obj_Decl : Node_Id;
Return_Obj_Id : Entity_Id;
(N : Node_Id;
Return_Etyp : Entity_Id;
Return_Obj_Typ : Entity_Id);
- -- Error using Error_Msg_N at node N. Output the dimensions of the
- -- returned type Return_Etyp and the returned object type Return_Obj_Typ
- -- of N.
+ -- Error using Error_Msg_N at node N. Output dimensions of the returned
+ -- type Return_Etyp and the returned object type Return_Obj_Typ of N.
-------------------------------------------------
-- Error_Dim_Msg_For_Extended_Return_Statement --
is
begin
Error_Msg_N ("dimensions mismatch in extended return statement", N);
- Error_Msg_N ("\expected dimension "
- & Dimensions_Msg_Of (Return_Etyp)
- & ", found "
- & Dimensions_Msg_Of (Return_Obj_Typ),
- N);
+ Error_Msg_N
+ ("\expected dimension " & Dimensions_Msg_Of (Return_Etyp)
+ & ", found " & Dimensions_Msg_Of (Return_Obj_Typ), N);
end Error_Dim_Msg_For_Extended_Return_Statement;
-- Start of processing for Analyze_Dimension_Extended_Return_Statement
end if;
Error_Msg_N
- ("\expected dimension "
- & Dimensions_Msg_Of (Comp_Typ)
- & ", found "
- & Dimensions_Msg_Of (Expr),
- Comp);
+ ("\expected dimension " & Dimensions_Msg_Of (Comp_Typ)
+ & ", found " & Dimensions_Msg_Of (Expr), Comp);
end if;
end if;
declare
Expr : Node_Id;
Exprs : constant List_Id := Expressions (N);
-
begin
if Present (Exprs) then
Expr := First (Exprs);
begin
Error_Msg_N ("dimensions mismatch in object declaration", N);
Error_Msg_N
- ("\expected dimension "
- & Dimensions_Msg_Of (Etyp)
- & ", found "
- & Dimensions_Msg_Of (Expr),
- Expr);
+ ("\expected dimension " & Dimensions_Msg_Of (Etyp) & ", found "
+ & Dimensions_Msg_Of (Expr), Expr);
end Error_Dim_Msg_For_Object_Declaration;
-- Start of processing for Analyze_Dimension_Object_Declaration
begin
Error_Msg_N ("dimensions mismatch in object renaming declaration", N);
Error_Msg_N
- ("\expected dimension "
- & Dimensions_Msg_Of (Sub_Mark)
- & ", found "
- & Dimensions_Msg_Of (Renamed_Name),
- Renamed_Name);
+ ("\expected dimension " & Dimensions_Msg_Of (Sub_Mark) & ", found "
+ & Dimensions_Msg_Of (Renamed_Name), Renamed_Name);
end Error_Dim_Msg_For_Object_Renaming_Declaration;
-- Start of processing for Analyze_Dimension_Object_Renaming_Declaration
begin
Error_Msg_N ("dimensions mismatch in return statement", N);
Error_Msg_N
- ("\expected dimension "
- & Dimensions_Msg_Of (Return_Etyp)
- & ", found "
- & Dimensions_Msg_Of (Expr),
- Expr);
+ ("\expected dimension " & Dimensions_Msg_Of (Return_Etyp)
+ & ", found " & Dimensions_Msg_Of (Expr), Expr);
end Error_Dim_Msg_For_Simple_Return_Statement;
-- Start of processing for Analyze_Dimension_Simple_Return_Statement
if Exists (Dims_Of_Id) then
Error_Msg_N
("subtype& already" & Dimensions_Msg_Of (Id, True), N);
-
else
Set_Dimensions (Id, Dims_Of_Etyp);
Set_Symbol (Id, Symbol_Of (Etyp));
begin
case Nkind (N) is
when N_Op_Plus | N_Op_Minus | N_Op_Abs =>
+
+ -- Propagate the dimension if the operand is not dimensionless
+
declare
R : constant Node_Id := Right_Opnd (N);
-
begin
- -- Propagate the dimension if the operand is not dimensionless
-
Move_Dimensions (R, N);
end;
Right_Rat : Rational;
begin
- -- Both left and right operands are an integer literal
+ -- Both left and right operands are integer literals
if Nkind (Left) = N_Integer_Literal
- and then Nkind (Right) = N_Integer_Literal
+ and then
+ Nkind (Right) = N_Integer_Literal
then
Left_Rat := Process_Literal (Left);
Right_Rat := Process_Literal (Right);
elsif Description_Needed then
Add_Str_To_Name_Buffer ("is dimensionless");
- -- Otherwise, return "[]"
+ -- Otherwise, return "'[']"
else
- Add_Str_To_Name_Buffer ("[]");
+ Add_Str_To_Name_Buffer ("'[']");
end if;
Dimensions_Msg := Name_Find;
Add_String_To_Name_Buffer (String_From_Numeric_Literal (N));
-- Insert a blank between the literal and the symbol
- Add_Str_To_Name_Buffer (" ");
+ Add_Str_To_Name_Buffer (" ");
Add_String_To_Name_Buffer (Symbol_Of (Typ));
Error_Msg_Name_1 := Name_Find;
- Error_Msg_N ("??assumed to be%%", N);
+ Error_Msg_N ("assumed to be%%??", N);
end Dim_Warning_For_Numeric_Literal;
----------------------------------------
(N : Node_Id;
Exponent_Value : Rational)
is
+ Loc : constant Source_Ptr := Sloc (N);
Dims_Of_N : constant Dimension_Type := Dimensions_Of (N);
- L : constant Node_Id := Left_Opnd (N);
- Etyp_Of_L : constant Entity_Id := Etype (L);
- Btyp_Of_L : constant Entity_Id := Base_Type (Etyp_Of_L);
- Loc : constant Source_Ptr := Sloc (N);
+ L : constant Node_Id := Left_Opnd (N);
+ Etyp_Of_L : constant Entity_Id := Etype (L);
+ Btyp_Of_L : constant Entity_Id := Base_Type (Etyp_Of_L);
Actual_1 : Node_Id;
Actual_2 : Node_Id;
Dim_Power : Rational;
-- Step 1: Generate the new aggregate for the aspect Dimension
New_Aspects := Empty_List;
- List_Of_Dims := New_List;
+ List_Of_Dims := New_List;
for Position in Dims_Of_N'First .. System.Count loop
Dim_Power := Dims_Of_N (Position);
Append_To (List_Of_Dims,
Make_Op_Divide (Loc,
Left_Opnd =>
- Make_Integer_Literal (Loc,
- Int (Dim_Power.Numerator)),
+ Make_Integer_Literal (Loc, Int (Dim_Power.Numerator)),
Right_Opnd =>
- Make_Integer_Literal (Loc,
- Int (Dim_Power.Denominator))));
+ Make_Integer_Literal (Loc, Int (Dim_Power.Denominator))));
end loop;
-- Step 2: Create the new Aspect Specification for Aspect Dimension
New_N :=
Make_Type_Conversion (Loc,
Subtype_Mark => New_Reference_To (New_Id, Loc),
- Expression =>
+ Expression =>
Make_Function_Call (Loc,
Name => New_Reference_To (RTE (RE_Expon_LLF), Loc),
Parameter_Associations => New_List (
Actual_Str : Node_Id;
begin
- Actual := First (Actuals);
-
-- Look for a symbols parameter association in the list of actuals
+ Actual := First (Actuals);
while Present (Actual) loop
-- Positional parameter association case when the actual is a
-- Store the dimension symbols inside boxes
- Store_String_Char ('[');
+ if In_Error_Msg then
+ Store_String_Chars ("'[");
+ else
+ Store_String_Char ('[');
+ end if;
for Position in Dimension_Type'Range loop
Dim_Power := Dims (Position);
-- Positive dimension case
if Dim_Power.Numerator > 0 then
+
-- Integer case
if Dim_Power.Denominator = 1 then
end if;
end loop;
- Store_String_Char (']');
+ if In_Error_Msg then
+ Store_String_Chars ("']");
+ else
+ Store_String_Char (']');
+ end if;
+
return End_String;
end From_Dim_To_Str_Of_Dim_Symbols;
Dim_Power := Dims (Position);
if Dim_Power /= Zero then
-
if First_Dim then
First_Dim := False;
else
declare
G : constant Int := GCD (X.Numerator, X.Denominator);
begin
- return Rational'(Numerator => Whole (Int (X.Numerator) / G),
+ return Rational'(Numerator => Whole (Int (X.Numerator) / G),
Denominator => Whole (Int (X.Denominator) / G));
end;
end Reduce;
Sbuffer : constant Source_Buffer_Ptr :=
Source_Text (Get_Source_File_Index (Loc));
Src_Ptr : Source_Ptr := Loc;
- C : Character := Sbuffer (Src_Ptr);
- -- Current source program character
+
+ C : Character := Sbuffer (Src_Ptr);
+ -- Current source program character
function Belong_To_Numeric_Literal (C : Character) return Boolean;
-- Return True if C belongs to a numeric literal
-- Here we definitely have a bad instantiation
- Error_Msg_NE ("??cannot instantiate& before body seen", N, Ent);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_NE ("cannot instantiate& before body seen<<", N, Ent);
if Present (Instance_Spec (N)) then
Supply_Bodies (Instance_Spec (N));
end if;
- Error_Msg_N ("\??Program_Error will be raised at run time", N);
+ Error_Msg_N ("\Program_Error [<<", N);
Insert_Elab_Check (N);
Set_ABE_Is_Certain (N);
end Check_Bad_Instantiation;
-- level, and the ABE is bound to occur.
if Elab_Call.Last = 0 then
+ Error_Msg_Warn := not GNATprove_Mode;
+
if Inst_Case then
Error_Msg_NE
- ("??cannot instantiate& before body seen", N, Orig_Ent);
+ ("cannot instantiate& before body seen<<", N, Orig_Ent);
else
- Error_Msg_NE ("??cannot call& before body seen", N, Orig_Ent);
+ Error_Msg_NE
+ ("cannot call& before body seen<<", N, Orig_Ent);
end if;
- Error_Msg_N ("\??Program_Error will be raised at run time", N);
+ Error_Msg_N ("\Program_Error [<<", N);
Insert_Elab_Check (N);
-- Call is not at outer level
and then (Nkind (Original_Node (N)) /= N_Function_Call
or else not In_Assertion_Expression (Original_Node (N)))
then
+ Error_Msg_Warn := not GNATprove_Mode;
+
if Inst_Case then
Error_Msg_NE
- ("instantiation of& may occur before body is seen??",
+ ("instantiation of& may occur before body is seen<<",
N, Orig_Ent);
else
Error_Msg_NE
- ("call to& may occur before body is seen??", N, Orig_Ent);
+ ("call to& may occur before body is seen<<", N, Orig_Ent);
end if;
Error_Msg_N
- ("\Program_Error may be raised at run time??", N);
+ ("\Program_Error ]<<", N);
Output_Calls (N);
end if;
or else
Scope (Proc) = Scope (Defining_Identifier (Decl)))
then
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_N
- ("task will be activated before elaboration of its body??",
+ ("task will be activated before elaboration of its body<<",
Decl);
- Error_Msg_N
- ("\Program_Error will be raised at run time??", Decl);
+ Error_Msg_N ("\Program_Error [<<", Decl);
elsif
Present (Corresponding_Body (Unit_Declaration_Node (Proc)))
Intval (N) > Expr_Value (Type_High_Bound (Universal_Integer)))
then
Apply_Compile_Time_Constraint_Error
- (N, "non-static universal integer value out of range??",
+ (N, "non-static universal integer value out of range<<",
CE_Range_Check_Failed);
-- Check out of range of base type
elsif Is_Out_Of_Range (N, T, Assume_Valid => True) then
Apply_Compile_Time_Constraint_Error
- (N, "value not in range of}??", CE_Range_Check_Failed);
+ (N, "value not in range of}<<", CE_Range_Check_Failed);
elsif Checks_On then
Enable_Range_Check (N);
Stat := False;
Fold := False;
+ -- Inhibit folding if -gnatd.f flag set
+
if Debug_Flag_Dot_F and then In_Extended_Main_Source_Unit (N) then
return;
end if;
and then Nkind (Parent (P)) = N_Subprogram_Body
and then Is_Empty_List (Declarations (Parent (P)))
then
- Error_Msg_N ("!??infinite recursion", N);
- Error_Msg_N ("\!??Storage_Error will be raised at run time", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("!infinite recursion<<", N);
+ Error_Msg_N ("\!Storage_Error [<<", N);
Insert_Action (N,
Make_Raise_Storage_Error (Sloc (N),
Reason => SE_Infinite_Recursion));
end if;
end loop;
- Error_Msg_N ("!??possible infinite recursion", N);
- Error_Msg_N ("\!??Storage_Error may be raised at run time", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("!possible infinite recursion<<", N);
+ Error_Msg_N ("\!??Storage_Error ]<<", N);
return True;
end Check_Infinite_Recursion;
Deepest_Type_Access_Level (Typ)
then
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_N
- ("??type in allocator has deeper level than "
- & "designated class-wide type", E);
- Error_Msg_N
- ("\??Program_Error will be raised at run time", E);
+ ("type in allocator has deeper level than "
+ & "designated class-wide type<<", E);
+ Error_Msg_N ("\Program_Error [<<", E);
Rewrite (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Accessibility_Check_Failed));
and then Ekind (Current_Scope) = E_Package
and then not In_Package_Body (Current_Scope)
then
- Error_Msg_N ("??cannot activate task before body seen", N);
- Error_Msg_N ("\??Program_Error will be raised at run time", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("cannot activate task before body seen<<", N);
+ Error_Msg_N ("\Program_Error [<<", N);
end if;
-- Ada 2012 (AI05-0111-3): Detect an attempt to allocate a task or a
and then Present (Subpool_Handle_Name (N))
and then Has_Task (Desig_T)
then
- Error_Msg_N ("??cannot allocate task on subpool", N);
- Error_Msg_N ("\??Program_Error will be raised at run time", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("cannot allocate task on subpool<<", N);
+ Error_Msg_N ("\Program_Error [<<", N);
Rewrite (N,
Make_Raise_Program_Error (Sloc (N),
and then Is_Entry_Barrier_Function (P))
then
Rtype := Etype (N);
+ Error_Msg_Warn := not GNATprove_Mode;
Error_Msg_NE
- ("??& should not be used in entry body (RM C.7(17))",
+ ("& should not be used in entry body (RM C.7(17))<<",
N, Nam);
- Error_Msg_NE
- ("\Program_Error will be raised at run time??", N, Nam);
+ Error_Msg_NE ("\Program_Error [<<", N, Nam);
Rewrite (N,
Make_Raise_Program_Error (Loc,
Reason => PE_Current_Task_In_Entry_Body));
-- Here warning is to be issued
Set_Has_Recursive_Call (Nam);
- Error_Msg_N
- ("??possible infinite recursion!", N);
- Error_Msg_N
- ("\??Storage_Error may be raised at run time!", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("possible infinite recursion<<!", N);
+ Error_Msg_N ("\Storage_Error ]<<!", N);
end if;
exit Scope_Loop;
end loop;
if not Call_OK then
- Error_Msg_N ("!?? cannot determine tag of result", N);
- Error_Msg_N ("!?? Program_Error will be raised", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_N ("!cannot determine tag of result<<", N);
+ Error_Msg_N ("\Program_Error [<<!", N);
Insert_Action (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Explicit_Raise));
Deepest_Type_Access_Level (Opnd_Type)
then
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Conversion_Error_N
- ("??source array type has deeper accessibility "
- & "level than target", Operand);
- Conversion_Error_N
- ("\??Program_Error will be raised at run time",
- Operand);
+ ("source array type has deeper accessibility "
+ & "level than target<<", Operand);
+ Conversion_Error_N ("\Program_Error [<<", Operand);
Rewrite (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Accessibility_Check_Failed));
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Conversion_Error_N
- ("??cannot convert local pointer to non-local access type",
+ ("cannot convert local pointer to non-local access type<<",
Operand);
- Conversion_Error_N
- ("\??Program_Error will be raised at run time", Operand);
+ Conversion_Error_N ("\Program_Error [<<", Operand);
else
Conversion_Error_N
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Conversion_Error_N
- ("??cannot convert access discriminant to non-local "
- & "access type", Operand);
- Conversion_Error_N
- ("\??Program_Error will be raised at run time",
- Operand);
+ ("cannot convert access discriminant to non-local "
+ & "access type<<", Operand);
+ Conversion_Error_N ("\Program_Error [<<", Operand);
+
+ -- Real error if not in instance body
+
else
Conversion_Error_N
("cannot convert access discriminant to non-local "
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Conversion_Error_N
- ("??cannot convert local pointer to non-local access type",
+ ("cannot convert local pointer to non-local access type<<",
Operand);
- Conversion_Error_N
- ("\??Program_Error will be raised at run time", Operand);
+ Conversion_Error_N ("\Program_Error [<<", Operand);
+
+ -- If not in an instance body, this is a real error
else
-- Avoid generation of spurious error message
-- will be generated by Expand_N_Type_Conversion.
if In_Instance_Body then
+ Error_Msg_Warn := not GNATprove_Mode;
Conversion_Error_N
- ("??cannot convert access discriminant to non-local "
- & "access type", Operand);
- Conversion_Error_N
- ("\??Program_Error will be raised at run time",
- Operand);
+ ("cannot convert access discriminant to non-local "
+ & "access type<<", Operand);
+ Conversion_Error_N ("\Program_Error [<<", Operand);
+
+ -- If not in an instance body, this is a real error
else
Conversion_Error_N
begin
if Has_Predicates (Typ) then
if Is_Generic_Actual_Type (Typ) then
- Error_Msg_FE (Msg & "??", N, Typ);
- Error_Msg_F ("\Program_Error will be raised at run time??", N);
+ Error_Msg_Warn := not GNATprove_Mode;
+ Error_Msg_FE (Msg & "<<", N, Typ);
+ Error_Msg_F ("\Program_Error [<<", N);
Insert_Action (N,
Make_Raise_Program_Error (Sloc (N),
Reason => PE_Bad_Predicated_Generic_Type));
Warn : Boolean := False) return Node_Id
is
Msgc : String (1 .. Msg'Length + 3);
- -- Copy of message, with room for possible ?? and ! at end
+ -- Copy of message, with room for possible ?? or << and ! at end
Msgl : Natural;
Wmsg : Boolean;
Eloc : Source_Ptr;
begin
+ -- If this is a warning, convert it into an error if we are operating
+ -- in GNATprove mode, because in SPARK, we are allowed to consider
+ -- such warnings as illegalities, and we choose to do so!
+
+ Error_Msg_Warn := not GNATprove_Mode;
+
-- A static constraint error in an instance body is not a fatal error.
-- we choose to inhibit the message altogether, because there is no
-- obvious node (for now) on which to post it. On the other hand the
Eloc := Sloc (N);
end if;
- Msgc (1 .. Msg'Length) := Msg;
+ -- Copy message to Msgc, converting any ? in the message into
+ -- < instead, so that we have an error in GNATprove mode.
+
Msgl := Msg'Length;
+ for J in 1 .. Msgl loop
+ if Msg (J) = '?' and then (J = 1 or else Msg (J) /= ''') then
+ Msgc (J) := '<';
+ else
+ Msgc (J) := Msg (J);
+ end if;
+ end loop;
+
-- Message is a warning, even in Ada 95 case
- if Msg (Msg'Last) = '?' then
+ if Msg (Msg'Last) = '?' or else Msg (Msg'Last) = '<' then
Wmsg := True;
-- In Ada 83, all messages are warnings. In the private part and
or else (Ada_Version = Ada_83 and then Comes_From_Source (N))
then
Msgl := Msgl + 1;
- Msgc (Msgl) := '?';
+ Msgc (Msgl) := '<';
Msgl := Msgl + 1;
- Msgc (Msgl) := '?';
+ Msgc (Msgl) := '<';
Wmsg := True;
elsif In_Instance_Not_Visible then
Msgl := Msgl + 1;
- Msgc (Msgl) := '?';
+ Msgc (Msgl) := '<';
Msgl := Msgl + 1;
- Msgc (Msgl) := '?';
+ Msgc (Msgl) := '<';
Wmsg := True;
-- Otherwise we have a real error message (Ada 95 static case)
end loop;
if Msgs then
+ Error_Msg_Warn := not GNATprove_Mode;
+
if Present (Ent) then
Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
else
and then not Comes_From_Source (Conc_Typ)
then
Error_Msg_NEL
- ("\??& will be raised at run time",
- N, Standard_Constraint_Error, Eloc);
+ ("\& [<<", N, Standard_Constraint_Error, Eloc);
else
- Error_Msg_NEL
- ("\??& will be raised for objects of this type",
- N, Standard_Constraint_Error, Eloc);
+ if GNATprove_Mode then
+ Error_Msg_NEL
+ ("\& would have been raised for objects of this "
+ & "type", N, Standard_Constraint_Error, Eloc);
+ else
+ Error_Msg_NEL
+ ("\& will be raised for objects of this type??",
+ N, Standard_Constraint_Error, Eloc);
+ end if;
end if;
end;
else
- Error_Msg_NEL
- ("\??& will be raised at run time",
- N, Standard_Constraint_Error, Eloc);
+ Error_Msg_NEL ("\& [<<", N, Standard_Constraint_Error, Eloc);
end if;
else
- Error_Msg
- ("\static expression fails Constraint_Check", Eloc);
+ Error_Msg ("\static expression fails Constraint_Check", Eloc);
Set_Error_Posted (N);
end if;
end if;