Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/doc/gnat_rm/standard_and_implementation_defined_restrictions.rst @ 131:84e7813d76e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc-8.2
author mir3636
date Thu, 25 Oct 2018 07:37:49 +0900
parents 04ced10e8804
children 1830386684a0
comparison
equal deleted inserted replaced
111:04ced10e8804 131:84e7813d76e9
986 wide types 986 wide types
987 appear, and that no wide or wide wide string or character literals 987 appear, and that no wide or wide wide string or character literals
988 appear in the program (that is literals representing characters not in 988 appear in the program (that is literals representing characters not in
989 type ``Character``). 989 type ``Character``).
990 990
991 Static_Dispatch_Tables
992 ----------------------
993 .. index:: Static_Dispatch_Tables
994
995 [GNAT] This restriction checks at compile time that all the artifacts
996 associated with dispatch tables can be placed in read-only memory.
997
991 SPARK_05 998 SPARK_05
992 -------- 999 --------
993 .. index:: SPARK_05 1000 .. index:: SPARK_05
994 1001
995 [GNAT] This restriction checks at compile time that some constructs 1002 [GNAT] This restriction checks at compile time that some constructs forbidden
996 forbidden in SPARK 2005 are not present. Error messages related to 1003 in SPARK 2005 are not present. Note that SPARK 2005 has been superseded by
997 SPARK restriction have the form: 1004 SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that
998 1005 a codebase respects SPARK 2014 restrictions, mark the code with pragma or
1006 aspect ``SPARK_Mode``, and run the tool GNATprove at Stone assurance level, as
1007 follows::
1008
1009 gnatprove -P project.gpr --mode=stone
1010
1011 or equivalently::
1012
1013 gnatprove -P project.gpr --mode=check_all
1014
1015 With restriction ``SPARK_05``, error messages related to SPARK 2005 restriction
1016 have the form:
999 1017
1000 :: 1018 ::
1001 1019
1002 violation of restriction "SPARK_05" at <source-location> 1020 violation of restriction "SPARK_05" at <source-location>
1003 <error message> 1021 <error message>
1004 1022
1005
1006 .. index:: SPARK 1023 .. index:: SPARK
1007 1024
1008 The restriction ``SPARK`` is recognized as a 1025 The restriction ``SPARK`` is recognized as a synonym for ``SPARK_05``. This is
1009 synonym for ``SPARK_05``. This is retained for historical 1026 retained for historical compatibility purposes (and an unconditional warning
1010 compatibility purposes (and an unconditional warning will be generated 1027 will be generated for its use, advising replacement by ``SPARK_05``).
1011 for its use, advising replacement by ``SPARK``).
1012 1028
1013 This is not a replacement for the semantic checks performed by the 1029 This is not a replacement for the semantic checks performed by the
1014 SPARK Examiner tool, as the compiler currently only deals with code, 1030 SPARK Examiner tool, as the compiler currently only deals with code,
1015 not SPARK 2005 annotations, and does not guarantee catching all 1031 not SPARK 2005 annotations, and does not guarantee catching all
1016 cases of constructs forbidden by SPARK 2005. 1032 cases of constructs forbidden by SPARK 2005.
1017 1033
1018 Thus it may well be the case that code which passes the compiler with 1034 Thus it may well be the case that code which passes the compiler with
1019 the SPARK restriction is rejected by the SPARK Examiner, e.g. due to 1035 the SPARK 2005 restriction is rejected by the SPARK Examiner, e.g. due to
1020 the different visibility rules of the Examiner based on SPARK 2005 1036 the different visibility rules of the Examiner based on SPARK 2005
1021 ``inherit`` annotations. 1037 ``inherit`` annotations.
1022 1038
1023 This restriction can be useful in providing an initial filter for code 1039 This restriction can be useful in providing an initial filter for code
1024 developed using SPARK 2005, or in examining legacy code to see how far 1040 developed using SPARK 2005, or in examining legacy code to see how far
1025 it is from meeting SPARK restrictions. 1041 it is from meeting SPARK 2005 restrictions.
1026 1042
1027 The list below summarizes the checks that are performed when this 1043 The list below summarizes the checks that are performed when this
1028 restriction is in force: 1044 restriction is in force:
1029 1045
1030 * No block statements 1046 * No block statements
1075 * Equality not allowed for arrays with non-matching static bounds (except strings) 1091 * Equality not allowed for arrays with non-matching static bounds (except strings)
1076 * Conversion / qualification not allowed for arrays with non-matching static bounds 1092 * Conversion / qualification not allowed for arrays with non-matching static bounds
1077 * Subprogram declaration only allowed in package spec (unless followed by import) 1093 * Subprogram declaration only allowed in package spec (unless followed by import)
1078 * Access types not allowed 1094 * Access types not allowed
1079 * Incomplete type declaration not allowed 1095 * Incomplete type declaration not allowed
1080 * Object and subtype declarations must respect SPARK restrictions 1096 * Object and subtype declarations must respect SPARK 2005 restrictions
1081 * Digits or delta constraint not allowed 1097 * Digits or delta constraint not allowed
1082 * Decimal fixed point type not allowed 1098 * Decimal fixed point type not allowed
1083 * Aliasing of objects not allowed 1099 * Aliasing of objects not allowed
1084 * Modular type modulus must be power of 2 1100 * Modular type modulus must be power of 2
1085 * Base not allowed on subtype mark 1101 * Base not allowed on subtype mark
1086 * Unary operators not allowed on modular types (except not) 1102 * Unary operators not allowed on modular types (except not)
1087 * Untagged record cannot be null 1103 * Untagged record cannot be null
1088 * No class-wide operations 1104 * No class-wide operations
1089 * Initialization expressions must respect SPARK restrictions 1105 * Initialization expressions must respect SPARK 2005 restrictions
1090 * Nonstatic ranges not allowed except in iteration schemes 1106 * Nonstatic ranges not allowed except in iteration schemes
1091 * String subtypes must have lower bound of 1 1107 * String subtypes must have lower bound of 1
1092 * Subtype of Boolean cannot have constraint 1108 * Subtype of Boolean cannot have constraint
1093 * At most one tagged type or extension per package 1109 * At most one tagged type or extension per package
1094 * Interface is not allowed 1110 * Interface is not allowed
1108 * Subtype of unconstrained array must have constraint 1124 * Subtype of unconstrained array must have constraint
1109 1125
1110 This list summarises the main SPARK 2005 language rules that are not 1126 This list summarises the main SPARK 2005 language rules that are not
1111 currently checked by the SPARK_05 restriction: 1127 currently checked by the SPARK_05 restriction:
1112 1128
1113 * SPARK annotations are treated as comments so are not checked at all 1129 * SPARK 2005 annotations are treated as comments so are not checked at all
1114 * Based real literals not allowed 1130 * Based real literals not allowed
1115 * Objects cannot be initialized at declaration by calls to user-defined functions 1131 * Objects cannot be initialized at declaration by calls to user-defined functions
1116 * Objects cannot be initialized at declaration by assignments from variables 1132 * Objects cannot be initialized at declaration by assignments from variables
1117 * Objects cannot be initialized at declaration by assignments from indexed/selected components 1133 * Objects cannot be initialized at declaration by assignments from indexed/selected components
1118 * Ranges shall not be null 1134 * Ranges shall not be null
1133 * After renaming, cannot use the original name 1149 * After renaming, cannot use the original name
1134 * Subprograms can only be renamed to remove package prefix 1150 * Subprograms can only be renamed to remove package prefix
1135 * Pragma import must be immediately after entity it names 1151 * Pragma import must be immediately after entity it names
1136 * No mutual recursion between multiple units (this can be checked with gnatcheck) 1152 * No mutual recursion between multiple units (this can be checked with gnatcheck)
1137 1153
1138 Note that if a unit is compiled in Ada 95 mode with the SPARK restriction, 1154 Note that if a unit is compiled in Ada 95 mode with the SPARK 2005 restriction,
1139 violations will be reported for constructs forbidden in SPARK 95, 1155 violations will be reported for constructs forbidden in SPARK 95,
1140 instead of SPARK 2005. 1156 instead of SPARK 2005.