From: Yannick Moy Date: Thu, 11 Jan 2018 08:52:12 +0000 (+0000) Subject: [Ada] Update description of restriction SPARK_05 with SPARK 2014 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5b2e4408ca5b9471e7d901b1baacf0fa9003496;p=gcc.git [Ada] Update description of restriction SPARK_05 with SPARK 2014 2018-01-11 Yannick Moy 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 34f13b975ae..fc7573112c7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2018-01-11 Yannick Moy + + * 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 * doc/gnat_ugn/gnat_utility_programs.rst: Fix layout. 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 1f56403f81a..0b9f6dc30a6 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 @@ -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 - .. 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. diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 12b2f42c8a0..50eac85c045 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -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 @@ -13163,10 +13179,9 @@ violation of restriction "SPARK_05" at @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.