+2012-10-02 Robert Dewar <dewar@adacore.com>
+
+ * usage.adb, gnat_rm.texi, vms_data.ads: Add entry for
+ /OVERFLOW_CHECKS=?? generating -gnato?? for control
+ of extended overflow checking.
+ * ug_words: Add entry for -gnato?? for /OVERFLOW_CHECKS=??
+ * gnat_ugn.texi: Add documentation for -gnato?? for control of overflow
+ checking mode.
+
+2012-10-02 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch4.adb (Analyze_Quantified_Expression): If the iterator in
+ a quantified expression is statically known to be null (e.g. a
+ array with an empty index type) emit a warning.
+
2012-10-02 Robert Dewar <dewar@adacore.com>
* sem_dim.adb: Minor code reorganization.
* Pragma Obsolescent::
* Pragma Optimize_Alignment::
* Pragma Ordered::
+* Pragma Overflow_Checks::
* Pragma Passive::
* Pragma Persistent_BSS::
* Pragma Polling::
* Pragma Obsolescent::
* Pragma Optimize_Alignment::
* Pragma Ordered::
+* Pragma Overflow_Checks::
* Pragma Passive::
* Pragma Persistent_BSS::
* Pragma Polling::
For additional information please refer to the description of the
@option{-gnatw.u} switch in the @value{EDITION} User's Guide.
+@node Pragma Overflow_Checks
+@unnumberedsec Pragma Overflow_Checks
+@findex Overflow checks
+@findex pragma @code{Overflow_Checks}
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Overflow_Checks
+ ( [General =>] MODE
+ [,[Assertions =>] MODE]);
+
+MODE ::= SUPPRESSED | CHECKED | MINIMIZED | ELIMINATED
+@end smallexample
+
+@noindent
+This pragma sets the current overflow mode to the given mode. For details
+of the meaning of these modes, see section on overflow checking in the
+GNAT users guide. If only the @code{General} parameter is present, the
+given mode applies to all expressions. If both parameters are present,
+the @code{General} mode applies to expressions outside assertions, and
+the @code{Eliminated} mode applies to expressions within assertions.
+
+The case of the @code{MODE} parameter is ignored,
+so @code{MINIMIZED}, @code{Minimized} and
+@code{minimized} all have the same effect.
+
+The @code{Overflow_Checks} pragma has the same scoping and placement
+rules as pragma @code{Suppress}, so it can occur either as a
+configuration pragma, specifying a default for the whole
+program, or in a declarative scope, where it applies to the
+remaining declarations and statements in that scope.
+
+The pragma @code{Suppress (Overflow_Check)} sets mode
+
+ General => Suppressed
+
+suppressing all overflow checking within and outside
+assertions.
+
+The pragam @code{Unsuppress (Overflow_Check)} sets mode
+
+ General => Checked
+
+which causes overflow checking of all intermediate overflows.
+This applies both inside and outside assertions.
+
@node Pragma Passive
@unnumberedsec Pragma Passive
@findex Passive
Historically front end inlining was more extensive than the gcc back end
inlining, but that is no longer the case.
+@item -gnato??
+@cindex @option{-gnato??} (@command{gcc})
+Set default overflow cheecking mode. If ?? is a single digit, in the
+range 0-3, it sets the overflow checking mode for all expressions,
+including those outside and within assertions. The meaning of nnn is:
+
+ 0 suppress overflow checks (SUPPRESSED)
+ 1 all intermediate overflows checked (CHECKED)
+ 2 minimize intermediate overflows (MINIMIZED)
+ 3 eliminate intermediate overflows (ELIMINATED)
+
+Otherwise ?? can be two digits, both 0-3, and in this case the first
+digit sets the mode (using the above code) for expressions outside an
+assertion, and the second digit sets the mode for expressions within
+an assertion.
+
@item -gnato
@cindex @option{-gnato} (@command{gcc})
Enable numeric overflow checking (which is not normally enabled by
default). Note that division by zero is a separate check that is not
controlled by this switch (division by zero checking is on by default).
+The checking mode is set to CHECKED (equivalent to @option{-gnato11}).
@item -gnatp
@cindex @option{-gnatp} (@command{gcc})
procedure Analyze_Quantified_Expression (N : Node_Id) is
QE_Scop : Entity_Id;
+ function Is_Empty_Range (Typ : Entity_Id) return Boolean;
+ -- If the iterator is part of a quantified expression, and the range is
+ -- known to be statically empty, emit a warning and replace expression
+ -- with its static value.
+
+ function Is_Empty_Range (Typ : Entity_Id) return Boolean is
+ Loc : constant Source_Ptr := Sloc (N);
+
+ begin
+ if Is_Array_Type (Typ)
+ and then Size_Known_At_Compile_Time (Typ)
+ and then RM_Size (Typ) = 0
+ then
+ if All_Present (N) then
+ Error_Msg_N ("?universal quantified expression "
+ & "over a null range has value True", N);
+ Rewrite (N, New_Occurrence_Of (Standard_True, Loc));
+
+ else
+ Error_Msg_N ("?existential quantified expression "
+ & "over a null range has value False", N);
+ Rewrite (N, New_Occurrence_Of (Standard_False, Loc));
+ end if;
+
+ Analyze (N);
+ return True;
+
+ else
+ return False;
+ end if;
+ end Is_Empty_Range;
+
begin
Check_SPARK_Restriction ("quantified expression is not allowed", N);
if Present (Iterator_Specification (N)) then
Preanalyze (Iterator_Specification (N));
+
+ if Is_Entity_Name (Name (Iterator_Specification (N)))
+ and then Is_Empty_Range (Etype (Name (Iterator_Specification (N))))
+ then
+ return;
+ end if;
+
else
Preanalyze (Loop_Parameter_Specification (N));
end if;
-gnatn2 ^ /INLINE=PRAGMA_LEVEL_2
-gnatN ^ /INLINE=FULL
-gnato ^ /CHECKS=OVERFLOW
+-gnato?? ^ /OVERFLOW_CHECKS=??
-gnatp ^ /CHECKS=SUPPRESS_ALL
-gnat-p ^ /CHECKS=UNSUPPRESS_ALL
-gnatP ^ /POLLING
-- Line for -gnato switch
Write_Switch_Char ("o");
- Write_Line ("Enable overflow checking (off by default)");
+ Write_Line ("Enable overflow checking mode to CHECKED (off by default)");
+
+ -- Line for -gnato? switch
+
+ Write_Switch_Char ("o?");
+ Write_Line ("Set SUPPRESSED/CHECKED/MINIMIZED/ELIMINATED (?=0/1/2/3) mode");
+
+ Write_Switch_Char ("o??");
+ Write_Line ("Set mode for general/assertion expressions separately");
-- Line for -gnatO switch
-- if the /CHECKS qualifier is not present on the
-- command line. Same as /NOCHECKS.
--
- -- OVERFLOW Enables overflow checking for integer operations and
- -- checks for access before elaboration on subprogram
- -- calls. This causes GNAT to generate slower and larger
- -- executable programs by adding code to check for both
- -- overflow and division by zero (resulting in raising
- -- "Constraint_Error" as required by Ada semantics).
+ -- OVERFLOW Enables overflow checking in CHECKED mode for integer
+ -- operations and checks for access before elaboration
+ -- on subprogram calls. This causes GNAT to generate
+ -- slower and larger executable programs by adding code
+ -- to check for both overflow and division by zero
+ -- (resulting in raising "Constraint_Error" as required
+ -- by Ada semantics).
-- Similarly, GNAT does not generate elaboration check
-- by default, and you must specify this keyword to
-- enable them.
-- file xyz.adb is compiled with -gnatl=.lst, then the output is written
-- to file xyz.adb_lst.
+ S_GCC_Overflo : aliased constant S := "/OVERFLOW_CHECKS=#" &
+ "-gnato#";
+ -- /OVERFLOW_CHECKS=nn
+ --
+ -- Set default overflow cheecking mode. If nn is a single digit, in the
+ -- range 0-3, it sets the overflow checking mode for all expressions,
+ -- including those outside and within assertions. The meaning of nnn is:
+ --
+ -- 0 suppress overflow checks (SUPPRESSED)
+ -- 1 all intermediate overflows checked (CHECKED)
+ -- 2 minimize intermediate overflows (MINIMIZED)
+ -- 3 eliminate intermediate overflows (ELIMINATED)
+ --
+ -- Otherwise nn can be two digits, both 0-3, and in this case the first
+ -- digit sets the mode (using the above code) for expressions outside an
+ -- assertion, and the second digit sets the mode for expressions within
+ -- an assertion.
+
S_GCC_Pointer : aliased constant S := "/POINTER_SIZE=" &
"64 " &
"-mmalloc64 " &
S_GCC_NoWarnP 'Access,
S_GCC_Opt 'Access,
S_GCC_OptX 'Access,
+ S_GCC_Overflo 'Access,
S_GCC_Pointer 'Access,
S_GCC_Polling 'Access,
S_GCC_Project 'Access,
projects / thirdparty / gcc.git / commitdiff
