[Ada] Update description of restriction SPARK_05 with SPARK 2014
2018-01-11 Yannick Moy <moy@adacore.com> gcc/ada/ * doc/gnat_rm/standard_and_implementation_defined_restrictions.rst: Update description of restriction SPARK_05 with SPARK 2014. * gnat_rm.texi: Regenerate. From-SVN: r256498
This commit is contained in:
Yannick Moy
Pierre-Marie de Rodat
parent
151af7d208
commit
a5b2e4408c
|
|
@ -1,3 +1,9 @@
|
|||
2018-01-11 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* doc/gnat_rm/standard_and_implementation_defined_restrictions.rst:
|
||||
Update description of restriction SPARK_05 with SPARK 2014.
|
||||
* gnat_rm.texi: Regenerate.
|
||||
|
||||
2018-01-11 Vasiliy Fofanov <fofanov@adacore.com>
|
||||
|
||||
* doc/gnat_ugn/gnat_utility_programs.rst: Fix layout.
|
||||
|
|
|
|||
|
|
@ -999,23 +999,32 @@ SPARK_05
|
|||
--------
|
||||
.. index:: SPARK_05
|
||||
|
||||
[GNAT] This restriction checks at compile time that some constructs
|
||||
forbidden in SPARK 2005 are not present. Error messages related to
|
||||
SPARK restriction have the form:
|
||||
[GNAT] This restriction checks at compile time that some constructs forbidden
|
||||
in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by
|
||||
SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that
|
||||
a codebase respects SPARK 2014 restrictions, mark the code with pragma or
|
||||
aspect ``SPARK_Mode``, and run the tool GNATprove at Stone assurance level, as
|
||||
follows::
|
||||
|
||||
gnatprove -P project.gpr --mode=stone
|
||||
|
||||
or equivalently::
|
||||
|
||||
gnatprove -P project.gpr --mode=check_all
|
||||
|
||||
With restriction ``SPARK_05``, error messages related to SPARK 2005 restriction
|
||||
have the form:
|
||||
|
||||
::
|
||||
|
||||
violation of restriction "SPARK_05" at <source-location>
|
||||
<error message>
|
||||
|
||||
|
||||
.. index:: SPARK
|
||||
|
||||
The restriction ``SPARK`` is recognized as a
|
||||
synonym for ``SPARK_05``. This is retained for historical
|
||||
compatibility purposes (and an unconditional warning will be generated
|
||||
for its use, advising replacement by ``SPARK``).
|
||||
The restriction ``SPARK`` is recognized as a synonym for ``SPARK_05``. This is
|
||||
retained for historical compatibility purposes (and an unconditional warning
|
||||
will be generated for its use, advising replacement by ``SPARK_05``).
|
||||
|
||||
This is not a replacement for the semantic checks performed by the
|
||||
SPARK Examiner tool, as the compiler currently only deals with code,
|
||||
|
|
@ -1023,13 +1032,13 @@ not SPARK 2005 annotations, and does not guarantee catching all
|
|||
cases of constructs forbidden by SPARK 2005.
|
||||
|
||||
Thus it may well be the case that code which passes the compiler with
|
||||
the SPARK restriction is rejected by the SPARK Examiner, e.g. due to
|
||||
the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to
|
||||
the different visibility rules of the Examiner based on SPARK 2005
|
||||
``inherit`` annotations.
|
||||
|
||||
This restriction can be useful in providing an initial filter for code
|
||||
developed using SPARK 2005, or in examining legacy code to see how far
|
||||
it is from meeting SPARK restrictions.
|
||||
it is from meeting SPARK 2005 restrictions.
|
||||
|
||||
The list below summarizes the checks that are performed when this
|
||||
restriction is in force:
|
||||
|
|
@ -1084,7 +1093,7 @@ restriction is in force:
|
|||
* Subprogram declaration only allowed in package spec (unless followed by import)
|
||||
* Access types not allowed
|
||||
* Incomplete type declaration not allowed
|
||||
* Object and subtype declarations must respect SPARK restrictions
|
||||
* Object and subtype declarations must respect SPARK 2005 restrictions
|
||||
* Digits or delta constraint not allowed
|
||||
* Decimal fixed point type not allowed
|
||||
* Aliasing of objects not allowed
|
||||
|
|
@ -1093,7 +1102,7 @@ restriction is in force:
|
|||
* Unary operators not allowed on modular types (except not)
|
||||
* Untagged record cannot be null
|
||||
* No class-wide operations
|
||||
* Initialization expressions must respect SPARK restrictions
|
||||
* Initialization expressions must respect SPARK 2005 restrictions
|
||||
* Nonstatic ranges not allowed except in iteration schemes
|
||||
* String subtypes must have lower bound of 1
|
||||
* Subtype of Boolean cannot have constraint
|
||||
|
|
@ -1117,7 +1126,7 @@ strict that the latest SPARK 2005 language definition:
|
|||
This list summarises the main SPARK 2005 language rules that are not
|
||||
currently checked by the SPARK_05 restriction:
|
||||
|
||||
* SPARK annotations are treated as comments so are not checked at all
|
||||
* SPARK 2005 annotations are treated as comments so are not checked at all
|
||||
* Based real literals not allowed
|
||||
* Objects cannot be initialized at declaration by calls to user-defined functions
|
||||
* Objects cannot be initialized at declaration by assignments from variables
|
||||
|
|
@ -1142,6 +1151,6 @@ currently checked by the SPARK_05 restriction:
|
|||
* Pragma import must be immediately after entity it names
|
||||
* No mutual recursion between multiple units (this can be checked with gnatcheck)
|
||||
|
||||
Note that if a unit is compiled in Ada 95 mode with the SPARK restriction,
|
||||
Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction,
|
||||
violations will be reported for constructs forbidden in SPARK 95,
|
||||
instead of SPARK 2005.
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@
|
|||
|
||||
@copying
|
||||
@quotation
|
||||
GNAT Reference Manual , Dec 15, 2017
|
||||
GNAT Reference Manual , Jan 10, 2018
|
||||
|
||||
AdaCore
|
||||
|
||||
|
|
@ -13152,9 +13152,25 @@ associated with dispatch tables can be placed in read-only memory.
|
|||
|
||||
@geindex SPARK_05
|
||||
|
||||
[GNAT] This restriction checks at compile time that some constructs
|
||||
forbidden in SPARK 2005 are not present. Error messages related to
|
||||
SPARK restriction have the form:
|
||||
[GNAT] This restriction checks at compile time that some constructs forbidden
|
||||
in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by
|
||||
SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that
|
||||
a codebase respects SPARK 2014 restrictions, mark the code with pragma or
|
||||
aspect @code{SPARK_Mode}, and run the tool GNATprove at Stone assurance level, as
|
||||
follows:
|
||||
|
||||
@example
|
||||
gnatprove -P project.gpr --mode=stone
|
||||
@end example
|
||||
|
||||
or equivalently:
|
||||
|
||||
@example
|
||||
gnatprove -P project.gpr --mode=check_all
|
||||
@end example
|
||||
|
||||
With restriction @code{SPARK_05}, error messages related to SPARK 2005 restriction
|
||||
have the form:
|
||||
|
||||
@example
|
||||
violation of restriction "SPARK_05" at <source-location>
|
||||
|
|
@ -13163,10 +13179,9 @@ violation of restriction "SPARK_05" at <source-location>
|
|||
|
||||
@geindex SPARK
|
||||
|
||||
The restriction @code{SPARK} is recognized as a
|
||||
synonym for @code{SPARK_05}. This is retained for historical
|
||||
compatibility purposes (and an unconditional warning will be generated
|
||||
for its use, advising replacement by @code{SPARK}).
|
||||
The restriction @code{SPARK} is recognized as a synonym for @code{SPARK_05}. This is
|
||||
retained for historical compatibility purposes (and an unconditional warning
|
||||
will be generated for its use, advising replacement by @code{SPARK_05}).
|
||||
|
||||
This is not a replacement for the semantic checks performed by the
|
||||
SPARK Examiner tool, as the compiler currently only deals with code,
|
||||
|
|
@ -13174,13 +13189,13 @@ not SPARK 2005 annotations, and does not guarantee catching all
|
|||
cases of constructs forbidden by SPARK 2005.
|
||||
|
||||
Thus it may well be the case that code which passes the compiler with
|
||||
the SPARK restriction is rejected by the SPARK Examiner, e.g. due to
|
||||
the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to
|
||||
the different visibility rules of the Examiner based on SPARK 2005
|
||||
@code{inherit} annotations.
|
||||
|
||||
This restriction can be useful in providing an initial filter for code
|
||||
developed using SPARK 2005, or in examining legacy code to see how far
|
||||
it is from meeting SPARK restrictions.
|
||||
it is from meeting SPARK 2005 restrictions.
|
||||
|
||||
The list below summarizes the checks that are performed when this
|
||||
restriction is in force:
|
||||
|
|
@ -13339,7 +13354,7 @@ Access types not allowed
|
|||
Incomplete type declaration not allowed
|
||||
|
||||
@item
|
||||
Object and subtype declarations must respect SPARK restrictions
|
||||
Object and subtype declarations must respect SPARK 2005 restrictions
|
||||
|
||||
@item
|
||||
Digits or delta constraint not allowed
|
||||
|
|
@ -13366,7 +13381,7 @@ Untagged record cannot be null
|
|||
No class-wide operations
|
||||
|
||||
@item
|
||||
Initialization expressions must respect SPARK restrictions
|
||||
Initialization expressions must respect SPARK 2005 restrictions
|
||||
|
||||
@item
|
||||
Nonstatic ranges not allowed except in iteration schemes
|
||||
|
|
@ -13428,7 +13443,7 @@ currently checked by the SPARK_05 restriction:
|
|||
@itemize *
|
||||
|
||||
@item
|
||||
SPARK annotations are treated as comments so are not checked at all
|
||||
SPARK 2005 annotations are treated as comments so are not checked at all
|
||||
|
||||
@item
|
||||
Based real literals not allowed
|
||||
|
|
@ -13500,7 +13515,7 @@ Pragma import must be immediately after entity it names
|
|||
No mutual recursion between multiple units (this can be checked with gnatcheck)
|
||||
@end itemize
|
||||
|
||||
Note that if a unit is compiled in Ada 95 mode with the SPARK restriction,
|
||||
Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction,
|
||||
violations will be reported for constructs forbidden in SPARK 95,
|
||||
instead of SPARK 2005.
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue