|
<Profile>.<MetaType>.<Tag>
|
<Description>
|
| AdaCodeGeneration.Attribute.generatePragmaAtomic |
Generates an “atomic” pragma for this attribute/variable. Only works for package variables or
static class attributes. |
| AdaCodeGeneration.Attribute.generatePragmaVolatile |
Generates a “volatile” pragma for this attribute/variable. Only works for package variables
or static class attributes. |
| AdaCodeGeneration.Attribute.representationClauses |
Contains the representation clauses to be generated for this attribute. Note that this is
only applicable for attributes defined on a package and for static attributes defined on
classes. |
| SPARK.Attribute.IsAbstract |
Controls the generation of the Ada declaration for the attribute. Used to model abstract own
variables |
| SPARK.Attribute.IsInitialized |
If this tag is set to true, the attribute name will be added to the initialization annotation
of the class or package it is defined in |
| SPARK.Attribute.OwnMode |
If this attribute is an own variable, controls the mode used in the own annotation of the
class or package it is defined in |
| SPARK.Attribute.OwnKind |
Controls the participation of the own attribute to the own annotation of the class or package
it is defined in |
| AdaCodeGeneration.Attribute.generatePragmaAtomic |
Generates an “atomic” pragma for this class record type. |
| AdaCodeGeneration.Class.generatePragmaElaborateBody |
Generates an “elaborate” pragma for this class |
| AdaCodeGeneration.Class.generatePragmaPreelaborate |
Generates a “preelaborate” pragma for this class |
| AdaCodeGeneration.Class.generatePragmaPure |
Generates a “pure” pragma for this class |
| AdaCodeGeneration.Attribute.generatePragmaVolatile |
Generates a “volatile” pragma for this class record type. |
| AdaCodeGeneration.Class.representationClauses |
Contains the representation clauses to be generated for this class |
| SPARK.Class.HideBody |
Controls the generation of the hide annotation for this class package body |
| SPARK.Class.HideElaborationCode |
Controls the generation of the hide annotation for this class package elaboration
code |
| SPARK.Class.HidePrivatePart |
Controls the generation of the hide annotation for this class package private part |
| SPARK.Class.Inherit |
Contains the comma separated list of packages this class is inheriting from |
| SPARK.Class.Initializes |
Contains the comma separated list of own variables this class is initializing |
| SPARK.Class.OwnSpec |
Contains the list of own variables (with optional modes and types) to be generated in the own
annotation of this class package spec |
| SPARK.Class.OwnBody |
Contains the list of own variables (with optional modes and types) to be generated in the own
annotation of this class package body |
| SPARK.Dependency.Inherit |
Indicates if this <<usage>> dependency shall also generate an inherit
annotation |
| SPARK.Dependency.GlobalMode |
Indicates the mode for the supplier variable of this <<SPARK_Global>>
dependency |
| SPARK.Operation.DerivesBody |
Enter the dependency clauses for the operation body derives annotation in this tag. |
| SPARK.Operation.DerivesSpec |
Enter the dependency clauses for the operation specification derives annotation in this
tag. |
| SPARK.Operation.GlobalBody |
Enter the global variables and their usage mode for this operation body in this tag |
| SPARK.Operation.GlobalSpes |
Enter the global variables and their usage mode for this operation specification in this
tag |
| SPARK.Operation.HideBody |
set this tag to true if you want the body for this operation to be hidden from the
examiner |
| SPARK.Operation.PostConditionBody |
Use this tag to capture the postcondition annotation for a procedure body or the return
annotation for a function body |
| SPARK.Operation.PostConditionSpec |
Use this tag to capture the postcondition annotation for a procedure specification or the
return annotation for a function specification |
| SPARK.Operation.PreConditionBody |
Use this tag to capture the precondition annotation for a procedure or function body |
| SPARK.Operation.PreConditionSpec |
Use this tag to capture the precondition annotation for a procedure or function
specification |
| AdaCodeGeneration.Package.generatePragmaElaborateBody |
Generates an “elaborate” pragma for this package |
| AdaCodeGeneration.Package.generatePragmaPreelaborate |
Generates a “preelaborate” pragma for this package |
| AdaCodeGeneration.Package.generatePragmaPure |
Generates a “pure” pragma for this package |
| SPARK.Class.HideBody |
Controls the generation of the hide annotation for this package body |
| SPARK.Class.HideElaborationCode |
Controls the generation of the hide annotation for this package elaboration code |
| SPARK.Class.HidePrivatePart |
Controls the generation of the hide annotation for this package private part |
| SPARK.Class.Inherit |
Contains the comma separated list of packages this package is inheriting from |
| SPARK.Class.Initializes |
Contains the comma separated list of own variables this package is initializing |
| SPARK.Class.OwnSpec |
Contains the list of own variables (with optional modes and types) to be generated in the own
annotation of this package spec |
| SPARK.Class.OwnBody |
Contains the list of own variables (with optional modes and types) to be generated in the own
annotation of this package body |
| AdaCodeGeneration.Attribute.generatePragmaAtomic |
Generates an “atomic” pragma for this type. |
| AdaCodeGeneration.Attribute.generatePragmaVolatile |
Generates a “volatile” pragma for this type. |
| AdaCodeGeneration.Type.representationClauses |
Contains the representation clauses to be generated for this type |