+2014-01-21 Thomas Quinot <quinot@adacore.com>
+
+ * atree.adb, atree.ads (Num_Extension_Nodes): Switch to Node_Id, since
+ this is value is used in Node_Id arithmetic operations.
+ (Copy_Node, Exchange_Entities): Use loops indexed by Num_Extension_Nodes
+ instead of hard-coded unrolled code.
+
+2014-01-21 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb: Minor code cleanup, removing useless code.
+
+2014-01-21 Arnaud Charlet <charlet@adacore.com>
+
+ * opt.ads (SPARK_Switches_File_Name): New.
+ * switch-c.adb (Scan_Front_End_Switches): Add handling of -gnates=xxx *
+ * usage.adb (Usage): Document -gnates, in gnatprove mode only.
+ * gnat_ugn.texi: Document -gnates.
+
+2014-01-21 Yannick Moy <moy@adacore.com>
+
+ * errout.adb (Special_Msg_Delete): Update comment. Remove
+ special case for GNATprove which should not ignore mismatch
+ in sizes for representation clauses.
+ * sem_prag.adb (Analyze_Pragma): Remove special case for GNATprove
+ which should not ignore pragma Pack.
+
+2014-01-21 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch4.adb: Code clean up.
+
+2014-01-21 Steve Baird <baird@adacore.com>
+
+ * gnat_rm.texi: Improve GNAT RM description of SPARK_Mode pragma.
+
2014-01-21 Robert Dewar <dewar@adacore.com>
* gcc-interface/gigi.h: Get Flags array address.
if With_Extension then
if Present (Src) and then Has_Extension (Src) then
for J in 1 .. Num_Extension_Nodes loop
- Nodes.Append (Nodes.Table (Src + Node_Id (J)));
- Flags.Append (Flags.Table (Src + Node_Id (J)));
+ Nodes.Append (Nodes.Table (Src + J));
+ Flags.Append (Flags.Table (Src + J));
end loop;
else
for J in 1 .. Num_Extension_Nodes loop
if Has_Extension (Source) then
pragma Assert (Has_Extension (Destination));
- Nodes.Table (Destination + 1) := Nodes.Table (Source + 1);
- Nodes.Table (Destination + 2) := Nodes.Table (Source + 2);
- Nodes.Table (Destination + 3) := Nodes.Table (Source + 3);
- Nodes.Table (Destination + 4) := Nodes.Table (Source + 4);
- Nodes.Table (Destination + 5) := Nodes.Table (Source + 5);
+ for J in 1 .. Num_Extension_Nodes loop
+ Nodes.Table (Destination + J) := Nodes.Table (Source + J);
+ end loop;
else
pragma Assert (not Has_Extension (Source));
Temp_Flg : Flags_Byte;
begin
- pragma Assert (Has_Extension (E1)
+ pragma Assert (True
+ and then Has_Extension (E1)
and then Has_Extension (E2)
and then not Nodes.Table (E1).In_List
and then not Nodes.Table (E2).In_List);
-- Exchange the contents of the two entities
- Temp_Ent := Nodes.Table (E1);
- Nodes.Table (E1) := Nodes.Table (E2);
- Nodes.Table (E2) := Temp_Ent;
-
- Temp_Ent := Nodes.Table (E1 + 1);
- Nodes.Table (E1 + 1) := Nodes.Table (E2 + 1);
- Nodes.Table (E2 + 1) := Temp_Ent;
-
- Temp_Ent := Nodes.Table (E1 + 2);
- Nodes.Table (E1 + 2) := Nodes.Table (E2 + 2);
- Nodes.Table (E2 + 2) := Temp_Ent;
-
- Temp_Ent := Nodes.Table (E1 + 3);
- Nodes.Table (E1 + 3) := Nodes.Table (E2 + 3);
- Nodes.Table (E2 + 3) := Temp_Ent;
-
- Temp_Ent := Nodes.Table (E1 + 4);
- Nodes.Table (E1 + 4) := Nodes.Table (E2 + 4);
- Nodes.Table (E2 + 4) := Temp_Ent;
-
- Temp_Ent := Nodes.Table (E1 + 5);
- Nodes.Table (E1 + 5) := Nodes.Table (E2 + 5);
- Nodes.Table (E2 + 5) := Temp_Ent;
+ for J in 0 .. Num_Extension_Nodes loop
+ Temp_Ent := Nodes.Table (E1 + J);
+ Nodes.Table (E1 + J) := Nodes.Table (E2 + J);
+ Nodes.Table (E2 + J) := Temp_Ent;
+ end loop;
-- Exchange flag bytes for first component. No need to do the exchange
-- for the other components, since the flag bytes are always zero.
-- nodes, considered as a single record. The following definition gives
-- the number of extension nodes.
- Num_Extension_Nodes : Int := 5;
+ Num_Extension_Nodes : Node_Id := 5;
-- This value is increased by one if debug flag -gnatd.N is set. This is
-- for testing performance impact of adding a new extension node.
elsif Msg = "size for& too small, minimum allowed is ^" then
- -- Suppress "size too small" errors in CodePeer mode and SPARK mode,
- -- since pragma Pack is also ignored in these configurations.
+ -- Suppress "size too small" errors in CodePeer mode, since code may
+ -- be analyzed in a different configuration than the one used for
+ -- compilation. Even when the configurations match, this message
+ -- may be issued on correct code, because pragma Pack is ignored
+ -- in CodePeer mode.
- -- 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
+ if CodePeer_Mode then
return True;
-- When a size is wrong for a frozen type there is no explicit size
Operating_Mode := Check_Semantics;
- -- Skip call to gigi
-
- -- This debug flag is not documented, AARGH! ???
-
- Debug_Flag_HH := True;
-
-- Enable assertions, since they give valuable extra information for
-- formal verification.
Syntax:
@smallexample @c ada
-pragma CPU (EXPRESSSION);
+pragma CPU (EXPRESSION);
@end smallexample
@noindent
Syntax:
@smallexample @c ada
-pragma Relative_Deadline (time_span_EXPRESSSION);
+pragma Relative_Deadline (time_span_EXPRESSION);
@end smallexample
@noindent
@end smallexample
@noindent
-This pragma is used to designate whether a contract and its implementation must
-follow the SPARK 2014 programming language syntactic and semantic rules. The
-pragma is intended for use with formal verification tools and has no effect on
-the generated code.
+This pragma is used to specify whether a construct must
+satisfy the syntactic and semantic rules of the SPARK 2014 programming
+language. The pragma is intended for use with formal verification tools
+and has no effect on the generated code.
-When used as a configuration pragma over a whole compilation or in a particular
-compilation unit, it sets the mode of the units involved, in particular:
+The SPARK_Mode pragma is used to specify the value of the SPARK_Mode aspect
+(a three-valued aspect having values of On, Off, or Auto) of an entity.
+More precisely, it is used to specify the aspect value of a ``section''
+of an entity (the term ``section'' is defined below).
+If a Spark_Mode pragma's (optional) argument is omitted,
+an implicit argument of On is assumed.
+
+A SPARK_Mode pragma may be used as a configuration pragma and then has the
+semantics described below. A SPARK_Mode pragma which is not used as a
+configuration pragma shall not have an argument of Auto.
+
+A SPARK_Mode pragma can be used as a local pragma only
+in the following contexts:
@itemize @bullet
@item
-@code{On}: All entities in the units must follow the SPARK 2014 language, and
-an error will be generated if not, unless locally overridden by a local
-SPARK_Mode pragma or aspect. @code{On} is the default mode when pragma
-SPARK_Mode is used without an argument.
+When the pragma is at the start of the visible declarations (preceded only
+by other pragmas) of a package declaration, it marks the visible part
+of the package as being in or out of SPARK 2014.
+
+@item
+When the pragma appears at the start of the private declarations of a
+package (preceded only by other pragmas), it marks the private part
+of the package as being in or out of SPARK 2014.
@item
-@code{Off}: The units are considered to be in Ada by default and therefore not
-part of SPARK 2014 unless overridden locally. These units may be called by
-SPARK 2014 units.
+When the pragma appears at the start of the declarations of a
+package body (preceded only by other pragmas),
+it marks the declaration list of the package body body as being
+in or out of SPARK 2014.
@item
-@code{Auto}: The formal verification tools will automatically detect whether
-each entity is in SPARK 2014 or in Ada.
+When the pragma appears at the start of the elaboration statements of
+a package body (preceded only by other pragmas),
+it marks the handled_sequence_of_statements of the package body
+as being in or out of SPARK 2014.
+
+@item
+When the pragma appears after a subprogram declaration (with only other
+pragmas intervening), it marks the subprogram's specification as
+being in or out of SPARK 2014.
+
+@item
+When the pragma appears at the start of the declarations of a subprogram
+body (preceded only by other pragmas), it marks the subprogram body
+as being in or out of SPARK 2014. For a subprogram body which is
+not a completion of another declaration, it also applies to the
+specification of the subprogram.
@end itemize
-Pragma SPARK_Mode can be used as a local pragma with the following semantics:
+A package is defined to have 4 ``sections'': its visible part, its private
+part, its body's declaration list, and its body's
+handled_sequence_of_statements. Any other construct which requires a
+completion is defined to have 2 ``sections'': its declaration and its
+completion. Any other construct is defined to have 1 section.
-@itemize @bullet
+The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity
+or construct is then defined to be the following value (except if this yields
+a result of Auto for a non-package; see below):
-@item
-Auto cannot be used as a mode argument.
+@itemize
@item
-When the pragma is at the start of the visible declarations (preceded only
-by other pragmas) of a package declaration, it marks the whole package
-(declaration and body) in or out of SPARK 2014.
+If SPARK_Mode has been specified for the given section of the given entity or
+construct, then the specified value;
@item
-When the pragma appears at the start of the private declarations of a
-package (only other pragmas can appear between the @code{private} keyword
-and the @code{SPARK_Mode} pragma), it marks the private part in or
-out of SPARK 2014 (overriding the default mode of the visible part).
+else if SPARK_Mode has been specified for at least one preceding section of
+the same entity, then the SPARK_Mode of the immediately preceding section;
@item
-When the pragma appears immediately at the start of the declarations of a
-package body (preceded only by other pragmas),
-it marks the whole body in or out of SPARK 2014 (overriding the default
-mode set by the declaration).
+else for any of the visible part or body declarations of a library unit package
+or either section of a library unit subprogram, if there is an applicable
+SPARK_Mode configuration pragma then the value specified by the
+pragma; if no such configuration pragma applies, then an implicit
+specification of Auto is assumed;
@item
-When the pragma appears at the start of the elaboration statements of
-a package body (only other pragmas can appear between the @code{begin}
-keyword and the @code{SPARK_Mode} pragma),
-it marks the elaboration statements in or out of SPARK 2014 (overriding
-the default mode of the package body).
+else for any subsequent (i.e., not the first) section of a library unit
+package, the SPARK_Mode of the preceding section;
@item
-When the pragma appears after a subprogram declaration (with only other
-pragmas intervening), it marks the whole
-subprogram (spec and body) in or out of SPARK 2014.
+else the SPARK_Mode of the enclosing section of the nearest enclosing package
+or subprogram;
+
+@end itemize
+
+If the above computation yields a result of Auto for any construct other than
+one of the four sections of a package, then a result of On or Off is
+determined instead based on the legality (with respect to the rules of
+SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only
+if the construct is in SPARK 2014. [A SPARK_Mode of
+Auto is therefore only possible for sections of a package.]
+
+If an earlier section of an entity has a Spark_Mode of Off, then the
+Spark_Mode aspect of any later section of that entity shall not be
+specified to be On. For example,
+if the specification of a subprogram has a Spark_Mode of Off, then the
+body of the subprogram shall not have a Spark_Mode of On.
+
+The following rules apply to SPARK code (i.e., constructs which
+have a SPARK_Mode aspect value of On):
+
+@itemize
@item
-When the pragma appears at the start of the declarations of a subprogram
-body (preceded only by other pragmas), it marks the whole body in or out
-of SPARK 2014 (overriding the default mode set by the declaration).
+SPARK code shall only reference SPARK declarations, but a SPARK declaration
+which requires a completion may have a non-SPARK completion.
@item
-Any other use of the pragma is illegal.
+SPARK code shall only enclose SPARK code, except that SPARK code may enclose
+a non-SPARK completion of an enclosed SPARK declaration.
@end itemize
@unnumberedsec Aspect SPARK_Mode
@findex SPARK_Mode
@noindent
-This aspect is equivalent to pragma @code{SPARK_Mode}.
+This aspect is equivalent to pragma @code{SPARK_Mode} and
+may be specified for either or both of the specification and body
+of a subprogram or package.
@node Aspect Suppress_Debug_Info
@unnumberedsec Aspect Suppress_Debug_Info
manner). This can be useful in some specialized circumstances such as the
temporary use of special test software.
+@item -gnates=@var{path}
+@cindex @option{-gnates=file} (@command{gcc})
+Only relevant to the SPARK toolset (gnat2why), where gnatprove passes
+extra switches via a response file to gnat2why via this switch.
+This switch is otherwise ignored by gcc.
+
@item -gnateS
@cindex @option{-gnateS} (@command{gcc})
Synonym of @option{-fdump-scos}, kept for backwards compatibility.
-- GNAT
-- Current SPARK mode setting
+ SPARK_Switches_File_Name : String_Ptr := null;
+ -- GNAT
+ -- Set to non-null file name by use of the -gnates switch to specify
+ -- SPARK (gnat2why) specific switches in the given file name.
+
Special_Exception_Package_Used : Boolean := False;
-- GNAT
-- Set to True if either of the unit GNAT.Most_Recent_Exception or
-- The parser cannot distinguish between a loop specification
-- and an iterator specification. If after pre-analysis the
-- proper form has been recognized, rewrite the expression to
- -- reflect the right kind. The analysis of the loop has been
- -- performed on a copy that has the proper iterator form. This
- -- is needed in particular for ASIS navigation.
+ -- reflect the right kind. This is needed for proper ASIS
+ -- navigation. If expansion is enabled, the transformation is
+ -- performed when the expression is rewritten as a loop.
- Set_Loop_Parameter_Specification (N, Empty);
Set_Iterator_Specification (N,
New_Copy_Tree (Iterator_Specification (Parent (Loop_Par))));
+
+ Set_Defining_Identifier (Iterator_Specification (N),
+ Relocate_Node (Defining_Identifier (Loop_Par)));
+ Set_Name (Iterator_Specification (N),
+ Relocate_Node (Discrete_Subtype_Definition (Loop_Par)));
+ Set_Comes_From_Source (Iterator_Specification (N),
+ Comes_From_Source (Loop_Parameter_Specification (N)));
+ Set_Loop_Parameter_Specification (N, Empty);
end if;
end;
end if;
if not Rep_Item_Too_Late (Typ, N) then
- -- In the context of static code analysis, we do not need
- -- complex front-end expansions related to pragma Pack,
- -- so disable handling of pragma Pack in these cases.
+ -- In CodePeer mode, we do not need complex front-end
+ -- expansions related to pragma Pack, so disable handling
+ -- of pragma Pack.
- if CodePeer_Mode or GNATprove_Mode then
+ if CodePeer_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly
-- files for the benefit of source coverage analysis tools
-- (xcov).
+ when 's' =>
+ if not First_Switch then
+ Osint.Fail
+ ("-gnates must not be combined with other switches");
+ end if;
+
+ -- Check for '='
+
+ Ptr := Ptr + 1;
+
+ if Ptr >= Max or else Switch_Chars (Ptr) /= '=' then
+ Bad_Switch ("-gnates");
+ else
+ SPARK_Switches_File_Name :=
+ new String'(Switch_Chars (Ptr + 1 .. Max));
+ end if;
+
+ return;
+
when 'S' =>
Generate_SCO := True;
Generate_SCO_Instance_Table := True;
Write_Switch_Char ("eP");
Write_Line ("Pure/Prelaborate errors generate warnings rather than errors");
+ if GNATprove_Mode then
+ -- Line for -gnates switch
+
+ Write_Switch_Char ("es=?");
+ Write_Line ("Specify extra switches for gnat2why");
+ end if;
+
-- Line for -gnateS switch
Write_Switch_Char ("eS");
projects / platform / upstream / gcc.git / commitdiff