From: Arnaud Charlet Date: Wed, 18 Nov 2015 10:50:40 +0000 (+0000) Subject: gnat_project_manager.rst, [...]: Update doc. X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2544cbe4f2f0a497fec59491333283750fe45fb2;p=gcc.git gnat_project_manager.rst, [...]: Update doc. * gnat_ugn/gnat_project_manager.rst, gnat_ugn/building_executable_programs_with_gnat.rst, gnat_ugn/gnat_and_program_execution.rst, gnat_ugn/the_gnat_compilation_model.rst, gnat_rm/implementation_defined_pragmas.rst, gnat_rm/standard_and_implementation_defined_restrictions.rst, gnat_ugn.texi, gnat_rm.texi: Update doc. From-SVN: r230538 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index de28d4677c4..8cafc9a19c2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,13 @@ +2015-11-18 Arnaud Charlet + + * gnat_ugn/gnat_project_manager.rst, + gnat_ugn/building_executable_programs_with_gnat.rst, + gnat_ugn/gnat_and_program_execution.rst, + gnat_ugn/the_gnat_compilation_model.rst, + gnat_rm/implementation_defined_pragmas.rst, + gnat_rm/standard_and_implementation_defined_restrictions.rst, + gnat_ugn.texi, gnat_rm.texi: Update doc. + 2015-11-18 Hristian Kirtchev * contracts.adb (Add_Contract_Item): Chain pragmas Attach_Handler diff --git a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst index aa569deda5c..2c762132788 100644 --- a/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst +++ b/gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst @@ -40,8 +40,50 @@ sequence). Pragma Abstract_State ===================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.4. +Syntax: + +.. code-block:: ada + + pragma Abstract_State (ABSTRACT_STATE_LIST); + + ABSTRACT_STATE_LIST ::= + null + | STATE_NAME_WITH_OPTIONS + | (STATE_NAME_WITH_OPTIONS {, STATE_NAME_WITH_OPTIONS} ) + + STATE_NAME_WITH_OPTIONS ::= + STATE_NAME + | (STATE_NAME with OPTION_LIST) + + OPTION_LIST ::= OPTION {, OPTION} + + OPTION ::= + SIMPLE_OPTION + | NAME_VALUE_OPTION + + SIMPLE_OPTION ::= Ghost | Synchronous + + NAME_VALUE_OPTION ::= + Part_Of => ABSTRACT_STATE + | External [=> EXTERNAL_PROPERTY_LIST] + + EXTERNAL_PROPERTY_LIST ::= + EXTERNAL_PROPERTY + | (EXTERNAL_PROPERTY {, EXTERNAL_PROPERTY} ) + + EXTERNAL_PROPERTY ::= + Async_Readers [=> boolean_EXPRESSION] + | Async_Writers [=> boolean_EXPRESSION] + | Effective_Reads [=> boolean_EXPRESSION] + | Effective_Writes [=> boolean_EXPRESSION] + others => boolean_EXPRESSION + + STATE_NAME ::= defining_identifier + + ABSTRACT_STATE ::= name + +For the semantics of this pragma, see the entry for aspect `Abstract_State` in +the SPARK 2014 Reference Manual, section 7.1.4. Pragma Ada_83 ============= @@ -510,14 +552,26 @@ case, and it is recommended that these two options not be used together. Pragma Async_Readers ==================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.2. +Syntax: + +.. code-block:: ada + + pragma Asynch_Readers [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Async_Readers` in +the SPARK 2014 Reference Manual, section 7.1.2. Pragma Async_Writers ==================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.2. +Syntax: + +.. code-block:: ada + + pragma Asynch_Writers [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Async_Writers` in +the SPARK 2014 Reference Manual, section 7.1.2. Pragma Attribute_Definition =========================== @@ -1049,23 +1103,30 @@ clause), the GNAT uses the default alignment as described previously. Pragma Constant_After_Elaboration ================================= -For the description of this pragma, see SPARK 2014 Reference Manual, -section 3.3.1. +Syntax: + +.. code-block:: ada + + pragma Constant_After_Elaboration [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect +`Constant_After_Elaboration` in the SPARK 2014 Reference Manual, section 3.3.1. Pragma Contract_Cases ===================== .. index:: Contract cases - Syntax: +.. code-block:: ada -:: + pragma Contract_Cases ((CONTRACT_CASE {, CONTRACT_CASE)); - pragma Contract_Cases ( - Condition => Consequence - {,Condition => Consequence}); + CONTRACT_CASE ::= CASE_GUARD => CONSEQUENCE + + CASE_GUARD ::= boolean_EXPRESSION | others + CONSEQUENCE ::= boolean_EXPRESSION The `Contract_Cases` pragma allows defining fine-grain specifications that can complement or replace the contract given by a precondition and a @@ -1308,8 +1369,14 @@ See Ada 2012 Reference Manual for details. Pragma Default_Initial_Condition ================================ -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.3.3. +Syntax: + +.. code-block:: ada + + pragma Default_Initial_Condition [ (null | boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect +`Default_Initial_Condition` in the SPARK 2014 Reference Manual, section 7.3.3. Pragma Debug ============ @@ -1449,8 +1516,33 @@ See Ada 2012 Reference Manual for details. Pragma Depends ============== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.1.5. +Syntax: + +.. code-block:: ada + + pragma Depends (DEPENDENCY_RELATION); + + DEPENDENCY_RELATION ::= + null + | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}) + + DEPENDENCY_CLAUSE ::= + OUTPUT_LIST =>[+] INPUT_LIST + | NULL_DEPENDENCY_CLAUSE + + NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST + + OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT}) + + INPUT_LIST ::= null | INPUT | (INPUT {, INPUT}) + + OUTPUT ::= NAME | FUNCTION_RESULT + INPUT ::= NAME + + where FUNCTION_RESULT is a function Result attribute_reference + +For the semantics of this pragma, see the entry for aspect `Depends` in the +SPARK 2014 Reference Manual, section 6.1.5. Pragma Detect_Blocking ====================== @@ -1512,14 +1604,26 @@ See Ada 2012 Reference Manual for details. Pragma Effective_Reads ====================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.2. +Syntax: + +.. code-block:: ada + + pragma Effective_Reads [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Effective_Reads` in +the SPARK 2014 Reference Manual, section 7.1.2. Pragma Effective_Writes ======================= -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.2. +Syntax: + +.. code-block:: ada + + pragma Effective_Writes [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Effective_Writes` +in the SPARK 2014 Reference Manual, section 7.1.2. Pragma Elaboration_Checks ========================= @@ -1966,8 +2070,14 @@ of GNAT specific extensions are recognized as follows: Pragma Extensions_Visible ========================= -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.1.7. +Syntax: + +.. code-block:: ada + + pragma Extensions_Visible [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Extensions_Visible` +in the SPARK 2014 Reference Manual, section 6.1.7. Pragma External =============== @@ -2168,14 +2278,37 @@ be `IEEE_Float` to specify the use of IEEE format, as follows: Pragma Ghost ============ -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.9. +Syntax: + +.. code-block:: ada + + pragma Ghost [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Ghost` in the SPARK +2014 Reference Manual, section 6.9. Pragma Global ============= -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.1.4. +Syntax: + +.. code-block:: ada + + pragma Global (GLOBAL_SPECIFICATION); + + GLOBAL_SPECIFICATION ::= + null + | (GLOBAL_LIST) + | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}) + + MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST + + MODE_SELECTOR ::= In_Out | Input | Output | Proof_In + GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM}) + GLOBAL_ITEM ::= NAME + +For the semantics of this pragma, see the entry for aspect `Global` in the +SPARK 2014 Reference Manual, section 6.1.4. Pragma Ident ============ @@ -2574,8 +2707,14 @@ tight packing). Pragma Initial_Condition ======================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.6. +Syntax: + +.. code-block:: ada + + pragma Initial_Condition (boolean_EXPRESSION); + +For the semantics of this pragma, see the entry for aspect `Initial_Condition` +in the SPARK 2014 Reference Manual, section 7.1.6. Pragma Initialize_Scalars ========================= @@ -2642,8 +2781,27 @@ User's Guide) when using this pragma. Pragma Initializes ================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.5. +Syntax: + +.. code-block:: ada + + pragma Initializes (INITIALIZATION_LIST); + + INITIALIZATION_LIST ::= + null + | (INITIALIZATION_ITEM {, INITIALIZATION_ITEM}) + + INITIALIZATION_ITEM ::= name [=> INPUT_LIST] + + INPUT_LIST ::= + null + | INPUT + | (INPUT {, INPUT}) + + INPUT ::= name + +For the semantics of this pragma, see the entry for aspect `Initializes` in the +SPARK 2014 Reference Manual, section 7.1.5. Pragma Inline_Always ==================== @@ -3988,8 +4146,16 @@ See Ada 2012 Reference Manual for details. Pragma Part_Of ============== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.2.6. +Syntax: + +.. code-block:: ada + + pragma Part_Of (ABSTRACT_STATE); + + ABSTRACT_STATE ::= NAME + +For the semantics of this pragma, see the entry for aspect `Part_Of` in the +SPARK 2014 Reference Manual, section 7.2.6. Pragma Passive ============== @@ -4943,26 +5109,92 @@ which is the preferred method of setting the `Ravenscar` profile. Pragma Refined_Depends ====================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.1.5. +Syntax: + +.. code-block:: ada + + pragma Refined_Depends (DEPENDENCY_RELATION); + + DEPENDENCY_RELATION ::= + null + | (DEPENDENCY_CLAUSE {, DEPENDENCY_CLAUSE}) + + DEPENDENCY_CLAUSE ::= + OUTPUT_LIST =>[+] INPUT_LIST + | NULL_DEPENDENCY_CLAUSE + + NULL_DEPENDENCY_CLAUSE ::= null => INPUT_LIST + + OUTPUT_LIST ::= OUTPUT | (OUTPUT {, OUTPUT}) + + INPUT_LIST ::= null | INPUT | (INPUT {, INPUT}) + + OUTPUT ::= NAME | FUNCTION_RESULT + INPUT ::= NAME + + where FUNCTION_RESULT is a function Result attribute_reference + +For the semantics of this pragma, see the entry for aspect `Refined_Depends` in +the SPARK 2014 Reference Manual, section 6.1.5. Pragma Refined_Global ===================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 6.1.4. +Syntax: + +.. code-block:: ada + + pragma Refined_Global (GLOBAL_SPECIFICATION); + + GLOBAL_SPECIFICATION ::= + null + | (GLOBAL_LIST) + | (MODED_GLOBAL_LIST {, MODED_GLOBAL_LIST}) + + MODED_GLOBAL_LIST ::= MODE_SELECTOR => GLOBAL_LIST + + MODE_SELECTOR ::= In_Out | Input | Output | Proof_In + GLOBAL_LIST ::= GLOBAL_ITEM | (GLOBAL_ITEM {, GLOBAL_ITEM}) + GLOBAL_ITEM ::= NAME + +For the semantics of this pragma, see the entry for aspect `Refined_Global` in +the SPARK 2014 Reference Manual, section 6.1.4. Pragma Refined_Post =================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.2.7. +Syntax: + +.. code-block:: ada + + pragma Refined_Post (boolean_EXPRESSION); + +For the semantics of this pragma, see the entry for aspect `Refined_Post` in +the SPARK 2014 Reference Manual, section 7.2.7. Pragma Refined_State ==================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.2.2. +Syntax: + +.. code-block:: ada + + pragma Refined_State (REFINEMENT_LIST); + + REFINEMENT_LIST ::= + (REFINEMENT_CLAUSE {, REFINEMENT_CLAUSE}) + + REFINEMENT_CLAUSE ::= state_NAME => CONSTITUENT_LIST + + CONSTITUENT_LIST ::= + null + | CONSTITUENT + | (CONSTITUENT {, CONSTITUENT}) + + CONSTITUENT ::= object_NAME | state_NAME + +For the semantics of this pragma, see the entry for aspect `Refined_State` in +the SPARK 2014 Reference Manual, section 7.2.2. Pragma Relative_Deadline ======================== @@ -6615,8 +6847,14 @@ It is not permissible to specify `Volatile_Full_Access` for a composite Pragma Volatile_Function ======================== -For the description of this pragma, see SPARK 2014 Reference Manual, -section 7.1.2. +Syntax: + +.. code-block:: ada + + pragma Volatile_Function [ (boolean_EXPRESSION) ]; + +For the semantics of this pragma, see the entry for aspect `Volatile_Function` +in the SPARK 2014 Reference Manual, section 7.1.2. Pragma Warning_As_Error ======================= diff --git a/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst b/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst index 04e3390af2a..f338f0f2f4d 100644 --- a/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst +++ b/gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst @@ -772,7 +772,7 @@ Pure_Barriers [GNAT] This restriction ensures at compile time that protected entry barriers are restricted to: -* simple boolean variables defined in the private part of the +* simple variables defined in the private part of the protected type/object, * constant declarations, * named numbers, diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst index 6bcc8191618..c6344132ab4 100644 --- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst +++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst @@ -1306,6 +1306,17 @@ Alphabetical List of All Switches :ref:`Optimization_and_Strict_Aliasing` for details. +.. index:: -fno-strict-overflow (gcc) + +:samp:`-fno-strict-overflow` + Causes the compiler to avoid assumptions regarding the rules of signed + integer overflow. These rules specify that signed integer overflow will + result in a Constraint_Error exception at run time and are enforced in + default mode by the compiler, so this switch should not be necessary in + normal operating mode. It might be useful in conjunction with *-gnato0* + for very peculiar cases of low-level programming. + + .. index:: -fstack-check (gcc) :samp:`-fstack-check` @@ -1548,6 +1559,17 @@ Alphabetical List of All Switches `Check_Float_Overflow` in GNAT RM. +.. index:: -gnateg (gcc) + +:samp:`-gnateg` +:samp:`-gnatceg` + + The `-gnatc` switch must always be specified before this switch, e.g. + `-gnatceg`. Generate a C header from the Ada input file. See + :ref:`Generating_C_Headers_for_Ada_Specifications` for more + information. + + .. index:: -gnateG (gcc) :samp:`-gnateG` diff --git a/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst b/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst index 6161073367b..c34e4d92683 100644 --- a/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst +++ b/gcc/ada/doc/gnat_ugn/gnat_and_program_execution.rst @@ -2999,9 +2999,9 @@ exception raised because of the intermediate overflow (and we really would prefer this precondition to be considered True at run time). -.. _Overflow_Checking_Modes_in_GNAT: +.. _Management_of_Overflows_in_GNAT: -Overflow Checking Modes in GNAT +Management of Overflows in GNAT ------------------------------- To deal with the portability issue, and with the problem of @@ -3202,7 +3202,7 @@ The default mode for overflow checks is General => Strict which causes all computations both inside and outside assertions to use -the base type. In addition overflow checks are suppressed. +the base type. This retains compatibility with previous versions of GNAT which suppressed overflow checks by default and always @@ -3220,8 +3220,6 @@ is equivalent to which causes overflow checking of all intermediate overflows both inside and outside assertions against the base type. -This provides compatibility -with this switch as implemented in previous versions of GNAT. The pragma `Suppress (Overflow_Check)` disables overflow checking, but it has no effect on the method used for computing diff --git a/gcc/ada/doc/gnat_ugn/gnat_project_manager.rst b/gcc/ada/doc/gnat_ugn/gnat_project_manager.rst index 21b4b6111e8..87269d8b315 100644 --- a/gcc/ada/doc/gnat_ugn/gnat_project_manager.rst +++ b/gcc/ada/doc/gnat_ugn/gnat_project_manager.rst @@ -2390,7 +2390,7 @@ building. The syntax looks like for External ("BUILD") use "PRODUCTION"; package Builder is - for Switches ("Ada") use ("-q"); + for Global_Compilation_Switches ("Ada") use ("-g"); end Builder; end Agg; diff --git a/gcc/ada/doc/gnat_ugn/the_gnat_compilation_model.rst b/gcc/ada/doc/gnat_ugn/the_gnat_compilation_model.rst index 673478a4aad..22e4950502b 100644 --- a/gcc/ada/doc/gnat_ugn/the_gnat_compilation_model.rst +++ b/gcc/ada/doc/gnat_ugn/the_gnat_compilation_model.rst @@ -4439,7 +4439,7 @@ easier to interface with other languages than previous versions of Ada. .. _Running_the_binding_generator: -Running the binding generator +Running the Binding Generator ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The binding generator is part of the *gcc* compiler and can be @@ -4534,7 +4534,7 @@ and then generate Ada bindings from this file: .. _Generating_bindings_for_C++_headers: -Generating bindings for C++ headers +Generating Bindings for C++ Headers ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Generating bindings for C++ headers is done using the same options, always @@ -4662,6 +4662,91 @@ Switches :samp:`-C` Extract comments from headers and generate Ada comments in the Ada spec files. +.. _Generating_C_Headers_for_Ada_Specifications: + +Generating C Headers for Ada Specifications +------------------------------------------- + +.. index:: Binding generation (for Ada specs) +.. index:: C headers (binding generation) + +GNAT includes a C header generator for Ada specifications which supports +Ada types that have a direct mapping to C types. This includes in particular +support for: + +* Scalar types +* Constrained arrays +* Records (untagged) +* Composition of the above types +* Constant declarations +* Object declarations +* Subprogram declarations + +Running the C Header Generator +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +The C header generator is part of the GNAT compiler and can be invoked via +the *-gnatceg* combination of switches, which will generate a :file:`.h` +file corresponding to the given input file (Ada spec or body). Note that +only spec files are processed in any case, so giving a spec or a body file +as input is equivalent. For example: + +.. code-block:: sh + + $ gcc -c -gnatceg pack1.ads + +will generate a self-contained file called :file:`pack1.h` including +common definitions from the Ada Standard package, followed by the +definitions included in :file:`pack1.ads`, as well as all the other units +withed by this file. + +For instance, given the following Ada files: + +.. code-block:: ada + + package Pack2 is + type Int is range 1 .. 10; + end Pack2; + +.. code-block:: ada + + with Pack2; + + package Pack1 is + type Rec is record + Field1, Field2 : Pack2.Int; + end record; + + Global : Rec := (1, 2); + + procedure Proc1 (R : Rec); + procedure Proc2 (R : in out Rec); + end Pack1; + +The above `gcc` command will generate the following :file:`pack1.h` file: + +.. code-block:: c + + /* Standard definitions skipped */ + #ifndef PACK2_ADS + #define PACK2_ADS + typedef short_short_integer pack2__TintB; + typedef pack2__TintB pack2__int; + #endif /* PACK2_ADS */ + + #ifndef PACK1_ADS + #define PACK1_ADS + typedef struct _pack1__rec { + pack2__int field1; + pack2__int field2; + } pack1__rec; + extern pack1__rec pack1__global; + extern void pack1__proc1(const pack1__rec r); + extern void pack1__proc2(pack1__rec *r); + #endif /* PACK1_ADS */ + +You can then `include` :file:`pack1.h` from a C source file and use the types, +call subprograms, reference objects, and constants. .. _GNAT_and_Other_Compilation_Models: