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

gcc/ada/ChangeLog

+2015-11-18  Arnaud Charlet  <charlet@adacore.com>
+
+	* 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  <kirtchev@adacore.com>
 
 	* contracts.adb (Add_Contract_Item): Chain pragmas Attach_Handler

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
 =======================

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,

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`

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

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;
 

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: