+2013-10-14 Robert Dewar <dewar@adacore.com>
+
+ * exp_prag.adb (Expand_Pragma_Check): Generate proper string
+ for invariant
+ * gnat_rm.texi: Add documentation for pragmas
+ Type_Invariant[_Class]
+ * par-prag.adb: Add entries for pragmas Type_Invariant[_Class]
+ * sem_ch13.adb: Minor reformatting
+ * sem_prag.adb: Implement pragmas Type_Invariant[_Class]
+ * snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class]
+
+2013-10-14 Johannes Kanig <kanig@adacore.com>
+
+ * debug.adb: Release now unused debug switches that were only
+ relevant for gnat2why backend, not the frontend
+ * frontend.adb (Frontend) Do not stop when -gnatd.H is present,
+ was unused
+
2013-10-14 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Analyze_Global_Item): Allow
-- d.E
-- d.F SPARK mode
-- d.G Frame condition mode for gnat2why
- -- d.H Standard package only mode for gnat2why
+ -- d.H
-- d.I Do not ignore enum representation clauses in CodePeer mode
-- d.J Disable parallel SCIL generation mode
- -- d.K SPARK check mode for gnat2why
+ -- d.K
-- d.L Depend on back end for limited types in if and case expressions
-- d.M Relaxed RM semantics
-- d.N Add node to all entities
-- d.O Dump internal SCO tables
-- d.P Previous (non-optimized) handling of length comparisons
- -- d.Q Flow Analysis mode for gnat2why
+ -- d.Q
-- d.R Restrictions in ali files in positional form
-- d.S Force Optimize_Alignment (Space)
-- d.T Force Optimize_Alignment (Time)
-- d.W Print out debugging information for Walk_Library_Items
-- d.X
-- d.Y
- -- d.Z Dump flow analysis graphs, for debugging purposes (gnat2why)
+ -- d.Z
-- d1 Error msgs have node numbers where possible
-- d2 Eliminate error flags in verbose form error messages
-- d.D SPARK strict mode. Interpret compiler permissions as strictly as
-- possible in SPARK mode.
-
+ --
-- d.F SPARK mode. Generate AST in a form suitable for formal
-- verification, as well as additional cross reference information in
-- ALI files to compute effects of subprograms. Note that ALI files
-- generate Why code. Instead, it generates ALI files with an extra
-- section which contains the effects of subprograms.
- -- d.H Standard package only mode for gnat2why. In this mode, gnat2why
- -- will only generate Why code for package Standard. Any given input
- -- file will be ignored.
-
-- d.I Do not ignore enum representation clauses in CodePeer mode.
-- The default of ignoring representation clauses for enumeration
-- types in CodePeer is good for the majority of Ada code, but in some
-- done in parallel to speed processing. This switch disables this
-- behavior.
- -- d.K SPARK check mode for gnat2why. In this mode, gnat2why does not
- -- generate Why code.
-
-- d.L Normally the front end generates special expansion for conditional
-- expressions of a limited type. This debug flag removes this special
-- case expansion, leaving it up to the back end to handle conditional
-- This is there in case we find a situation where the optimization
-- malfunctions, to provide a work around.
- -- d.Q Flow Analysis mode for gnat2why. When this flag is given,
- -- gnat2why will do flow analysis, and no translation to Why is done.
-
-- d.R As documented in lib-writ.ads, restrictions in the ali file can
-- have two forms, positional and named. The named notation is the
-- current preferred form, but the use of this debug switch will force
-- the order in which units are walked. This is primarily for use in
-- debugging CodePeer mode.
- -- d.Z In gnat2why, in Flow analysis mode (-gnatd.Q), dump the different
- -- graphs (control flow, control dependence) for debugging purposes.
- -- This debug flag will be removed when flow analysis is sufficiently
- -- stable.
-
-- d.Y Prevents the use of the N_Expression_With_Actions node even in the
-- case of the gcc back end. Provided as a back up in case the new
-- scheme has problems.
-- at" is omitted for name = Assertion, since it is redundant, given
-- that the name of the exception is Assert_Failure.)
+ -- Also, instead of "XXX failed at", we generate slightly
+ -- different messages for some of the contract assertions (see
+ -- code below for details).
+
-- An alternative expansion is used when the No_Exception_Propagation
-- restriction is active and there is a local Assert_Failure handler.
-- This is not a common combination of circumstances, but it occurs in
Insert_Str_In_Name_Buffer ("failed ", 1);
Add_Str_To_Name_Buffer (" from ");
+ -- For special case of Invariant, the string is "failed
+ -- invariant from yy", to be consistent with the string that is
+ -- generated for the aspect case (the code later on checks for
+ -- this specific string to modify it in some cases, so this is
+ -- functionally important).
+
+ elsif Nam = Name_Invariant then
+ Add_Str_To_Name_Buffer ("failed invariant from ");
+
-- For all other checks, the string is "xxx failed at yyy"
-- where xxx is the check name with current source file casing.
CStand.Create_Standard;
- -- If the -gnatd.H flag is present, we are only interested in the Standard
- -- package, so the frontend has done its job here.
-
- if Debug_Flag_Dot_HH then
- return;
- end if;
-
-- Check possible symbol definitions specified by -gnateD switches
Prepcomp.Process_Command_Line_Symbol_Definitions;
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
* Pragma Unchecked_Union::
* Pragma Unimplemented_Unit::
* Pragma Universal_Aliasing ::
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
* Pragma Unchecked_Union::
* Pragma Unimplemented_Unit::
* Pragma Universal_Aliasing ::
Dynamic_Predicate => F(Q) or G(Q);
@end smallexample
+Note that there is are no pragmas @code{Dynamic_Predicate}
+or @code{Static_Predicate}. That is
+because these pragmas would affect legality and semantics of
+the program and thus do not have a neutral effect if ignored.
+The motivation behind providing pragmas equivalent to
+corresponding aspects is to allow a program to be written
+using the pragmas, and then compiled with a compiler that
+will ignore the pragmas. That doesn't work in the case of
+static and dynamic predicates, since if the corresponding
+pragmas are ignored, then the behavior of the program is
+fundamentally changed (for example a membership test
+@code{A in B} would not take into account a predicate
+defined for subtype B). When following this approach, the
+use of predicates should be avoided.
+
@node Pragma Preelaborable_Initialization
@unnumberedsec Pragma Preelaborable_Initialization
@findex Preelaborable_Initialization
notation is used, and named and positional notation can be mixed
following the normal rules for procedure calls in Ada.
+@node Pragma Type_Invariant
+@unnumberedsec Pragma Type_Invariant
+@findex Invariant
+@findex Type_Invariant pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant
+ ([Entity =>] type_LOCAL_NAME,
+ [Check =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant}
+aspect, and shares its restrictions and semantics. It differs
+from the language defined @code{Invariant} pragma in that it
+does not permit a string parameter, and it is
+controlled by the assertion identifier @code{Type_Invariant}
+rather than @code{Invariant}.
+
+@node Pragma Type_Invariant_Class
+@unnumberedsec Pragma Type_Invariant_Class
+@findex Invariant
+@findex Type_Invariant_Class pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant_Class
+ ([Entity =>] type_LOCAL_NAME,
+ [Check =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant_Class} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant'Class}
+aspect, and shares its restrictions and semantics.
+
+Note: This pragma is called @code{Type_Invariant_Class} rather than
+@code{Type_Invariant'Class} because the latter would not be strictly
+conforming to the allowed syntax for pragmas. The motivation
+for providing pragmas equivalent to the aspects is to allow a program
+to be written using the pragmas, and then compiled if necessary
+using an Ada compiler that does not recognize the pragmas or
+aspects, but is prepared to ignore the pragmas. The assertion
+policy that controls this pragma is @code{Type_Invariant'Class},
+not @code{Type_Invariant_Class}.
+
@node Pragma Unchecked_Union
@unnumberedsec Pragma Unchecked_Union
@cindex Unions in C
Pragma_Thread_Local_Storage |
Pragma_Time_Slice |
Pragma_Title |
+ Pragma_Type_Invariant |
+ Pragma_Type_Invariant_Class |
Pragma_Unchecked_Union |
Pragma_Unimplemented_Unit |
Pragma_Universal_Aliasing |
if Present (SId) then
PDecl := Unit_Declaration_Node (SId);
-
else
PDecl := Build_Invariant_Procedure_Declaration (Typ);
end if;
if Is_Input then
if (Ekind (Item_Id) = E_Out_Parameter
- and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
+ and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
or else
(Global_Seen and then not Appears_In (Subp_Inputs, Item_Id))
then
Name_Link_Name));
Check_At_Least_N_Arguments (2);
-
Check_At_Most_N_Arguments (4);
Process_Convention (C, Def_Id);
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
- Check_At_Most_N_Arguments (3);
+ Check_At_Most_N_Arguments (3);
Check_Optional_Identifier (Arg1, Name_Entity);
Check_Optional_Identifier (Arg2, Name_Check);
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
+ Check_At_Most_N_Arguments (2);
-- Process first argument
begin
GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (1);
+ Check_Arg_Count (1);
Check_No_Identifiers;
Check_Pre_Post;
+ -- Rewrite Post[_Class] pragma as Precondition pragma setting the
+ -- flag Class_Present to True for the Post_Class case.
+
Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
PC_Pragma := New_Copy (N);
Set_Pragma_Identifier
begin
GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (1);
+ Check_Arg_Count (1);
Check_No_Identifiers;
Check_Pre_Post;
+ -- Rewrite Pre[_Class] pragma as Precondition pragma setting the
+ -- flag Class_Present to True for the Pre_Class case.
+
Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
PC_Pragma := New_Copy (N);
Set_Pragma_Identifier
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
+ Check_At_Most_N_Arguments (2);
Check_Optional_Identifier (Arg1, Name_Check);
Check_Precondition_Postcondition (In_Body);
end loop;
end Title;
+ ----------------------------
+ -- Type_Invariant[_Class] --
+ ----------------------------
+
+ -- pragma Type_Invariant[_Class]
+ -- ([Entity =>] type_LOCAL_NAME,
+ -- [Check =>] EXPRESSION);
+
+ when Pragma_Type_Invariant |
+ Pragma_Type_Invariant_Class =>
+ Type_Invariant : declare
+ I_Pragma : Node_Id;
+
+ begin
+ Check_Arg_Count (2);
+
+ -- Rewrite Type_Invariant[_Class] pragma as an Invariant pragma,
+ -- setting Class_Present for the Type_Invariant_Class case.
+
+ Set_Class_Present (N, Prag_Id = Pragma_Type_Invariant_Class);
+ I_Pragma := New_Copy (N);
+ Set_Pragma_Identifier
+ (I_Pragma, Make_Identifier (Loc, Name_Invariant));
+ Rewrite (N, I_Pragma);
+ Set_Analyzed (N, False);
+ Analyze (N);
+ end Type_Invariant;
+
---------------------
-- Unchecked_Union --
---------------------
Pragma_Thread_Local_Storage => 0,
Pragma_Time_Slice => -1,
Pragma_Title => -1,
+ Pragma_Type_Invariant => -1,
+ Pragma_Type_Invariant_Class => -1,
Pragma_Unchecked_Union => 0,
Pragma_Unimplemented_Unit => -1,
Pragma_Universal_Aliasing => -1,
Name_Dynamic_Predicate : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
Name_Synchronization : constant Name_Id := N + $;
- Name_Type_Invariant : constant Name_Id := N + $;
- Name_Type_Invariant_Class : constant Name_Id := N + $;
-- Some special names used by the expander. Note that the lower case u's
-- at the start of these names get translated to extra underscores. These
Name_Wide_Character_Encoding : constant Name_Id := N + $; -- GNAT
Last_Configuration_Pragma_Name : constant Name_Id := N + $;
- -- Remaining pragma names
+ -- Remaining pragma names (non-configuration pragmas)
Name_Abort_Defer : constant Name_Id := N + $; -- GNAT
Name_Abstract_State : constant Name_Id := N + $; -- GNAT
Name_Thread_Local_Storage : constant Name_Id := N + $; -- GNAT
Name_Time_Slice : constant Name_Id := N + $; -- GNAT
Name_Title : constant Name_Id := N + $; -- GNAT
+ Name_Type_Invariant : constant Name_Id := N + $; -- GNAT
+ Name_Type_Invariant_Class : constant Name_Id := N + $; -- GNAT
Name_Unchecked_Union : constant Name_Id := N + $; -- Ada 05
Name_Unimplemented_Unit : constant Name_Id := N + $; -- GNAT
Name_Universal_Aliasing : constant Name_Id := N + $; -- GNAT
Pragma_Thread_Local_Storage,
Pragma_Time_Slice,
Pragma_Title,
+ Pragma_Type_Invariant,
+ Pragma_Type_Invariant_Class,
Pragma_Unchecked_Union,
Pragma_Unimplemented_Unit,
Pragma_Universal_Aliasing,
projects / thirdparty / gcc.git / commitdiff
