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
=============
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
===========================
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
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
============
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
======================
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
=========================
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
===============
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
============
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
=========================
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
====================
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
==============
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
========================
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
=======================
.. _Running_the_binding_generator:
-Running the binding generator
+Running the Binding Generator
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
The binding generator is part of the *gcc* compiler and can be
.. _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
: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:
projects / gcc.git / commitdiff