Error Messages For SPARK Violations
-----------------------------------

The following table shows all errors that correspond to SPARK language violations.

.. tabularcolumns:: |p{2in}|l|p{3in}|

.. csv-table::
   :header: "Violation Tag", "SRM Reference", "Explanation"
   :widths: 2, 1, 4

    "violation-access-constant", "SPARK RM 4.1.4(6)", "Access attribute of a named access-to-constant type whose prefix is not a constant part of an object"
    "violation-access-expression", "SPARK RM 4.1.4(1)", "Access attribute on a complex expression"
    "violation-access-function-with-side-effects", "SPARK RM 4.1.4(4)", "access to function with side effects"
    "violation-access-no-root", "SPARK RM 4.1.4(1)", "Access attribute of a path not rooted inside a parameter or standalone object"
    "violation-access-subprogram-within-protected", "SPARK RM 4.1.4(2)", "access to subprogram declared within a protected object"
    "violation-access-sub-formal-with-inv", "SPARK RM 4.1.4(2)", "formal with type invariants in access-to-subprogram"
    "violation-access-sub-return-type-with-inv", "SPARK RM 4.1.4(2)", "access-to-subprogram returning a type with invariants"
    "violation-access-sub-with-globals", "SPARK RM 4.1.4(7)", "access to subprogram with global effects"
    "violation-access-to-dispatch-op", "SPARK RM 4.1.4(2)", "access to dispatching operation"
    "violation-access-volatile-function", "SPARK RM 4.1.4(3)", "access to volatile function"
    "violation-address-of-non-object", "", "attribute Address of a non-object entity"
    "violation-address-outside-address-clause", "SPARK RM 13.7(2)", "attribute Address outside an attribute definition clause"
    "violation-aggregate-globals", "", "subprogram associated to aspect Aggregate with dependency on globals"
    "violation-aggregate-side-effects", "", "subprogram with side effects associated with aspect Aggregate"
    "violation-aggregate-volatile", "", "volatile function associated with aspect Aggregate"
    "violation-assert-and-cut-context", "SPARK RM 5.9", "pragma Assert_And_Cut outside a sequence of statements"
    "violation-backward-goto", "SPARK RM 5.8(1)", "backward goto statement"
    "violation-box-notation-without-init", "SPARK RM 4.3(1)", "box notation without default or relaxed initialization"
    "violation-code-statement", "", "code statement"
    "violation-controlled-types", "SPARK RM 7.6(1)", "controlled types"
    "violation-container-aggregate", "", "container aggregate whose type does not have the Container_Aggregates annotation"
    "violation-default-with-current-instance", "SPARK RM 3.8(1)", "default expression with current instance of enclosing type"
    "violation-derived-untagged-with-tagged-full-view", "SPARK RM 3.4(1)", "deriving from type declared as untagged private"
    "violation-discriminant-access", "SPARK RM 3.7(2)", "access discriminant"
    "violation-discriminant-derived", "SPARK RM 3.7(2)", "discriminant on derived type"
    "violation-dispatch-plain-pre", "SPARK RM 6.1.1(2)", "plain precondition on dispatching subprogram"
    "violation-dispatching-untagged-type", "SPARK RM 3.9.2(1)", "dispatching call on primitive of type with untagged partial view"
    "violation-exit-cases-exception", "SPARK RM 6.1.11(3)", "exit case mentioning exceptions when no exceptions can be propagated"
    "violation-exit-cases-normal-only", "SPARK RM 6.1.11(2)", "Exit_Case on subprogram which can only return normally"
    "violation-function-global-output", "SPARK RM 6.1(6)", "function with global outputs"
    "violation-function-out-param", "SPARK RM 6.1(6)", "function with out or in out parameters"
    "violation-ghost-concurrent-comp", "SPARK RM 6.9(22)", "concurrent component of ghost type"
    "violation-ghost-volatile", "SPARK RM 6.9(9)", "volatile ghost object"
    "violation-handler-choice-parameter", "SPARK RM 11.2(1)", "choice parameter in handler"
    "violation-invariant-class", "SPARK RM 7.3.2(2)", "classwide invariant"
    "violation-invariant-ext", "SPARK RM 7.3.2(2)", "type invariant on completion of private_type_extension"
    "violation-invariant-partial", "SPARK RM 7.3.2(2)", "type invariant on private_type_declaration or private_type_extension"
    "violation-invariant-volatile", "SPARK RM 7.3.2(4)", "type invariant on effectively volatile type"
    "violation-iterable-controlling-result", "SPARK RM 5.5.2(12)", "function associated to aspect Iterable with controlling result"
    "violation-iterable-full-view", "SPARK RM 5.5.2(13)", "Iterable aspect declared on the full view of a private type"
    "violation-iterable-globals", "SPARK RM 5.5.2(12)", "function associated to aspect Iterable with dependency on globals"
    "violation-iterable-side-effects", "SPARK RM 5.5.2(12)", "function with side effects associated with aspect Iterable"
    "violation-iterable-volatile", "SPARK RM 5.5.2(12)", "volatile function associated with aspect Iterable"
    "violation-iterator-specification", "SPARK RM 5.5.2", "iterator specification"
    "violation-loop-variant-structural", "SPARK RM 5.5.3 (8)", "structural loop variant which is not a variable of an anonymous access-to-object type"
    "violation-overlay-constant-not-imported", "SPARK RM 13.7(5)", "constant object with an address clause which is not imported"
    "violation-overlay-mutable-constant", "SPARK RM 13.7(4)", "mutable object and constant object overlaying each other"
    "violation-overlay-part-of-protected", "SPARK RM 13.7(3)", "overlaid object which is a part of a protected object"
    "violation-ownership-access-equality", "SPARK RM 3.10(19)", "equality on access types"
    "violation-ownership-allocator-invalid-context", "SPARK RM 4.8(2)", "allocator or call to allocating function not stored in object as part of assignment, declaration, or return statement"
    "violation-ownership-allocator-uninitialized", "SPARK RM 4.8(1)", "uninitialized allocator without default initialization"
    "violation-ownership-anonymous-access-to-named", "SPARK RM 3.10(18)", "conversion from an anonymous access type to a named access type"
    "violation-ownership-anonymous-part-of", "SPARK RM 3.10", "anonymous access variable marked Part_Of a protected object"
    "violation-ownership-anonymous-object-context", "SPARK RM 3.10(5)", "object of anonymous access not declared immediately within a subprogram, entry or block"
    "violation-ownership-anonymous-object-init", "SPARK RM 3.10(5)", "uninitialized object of anonymous access type"
    "violation-ownership-anonymous-result", "SPARK RM 3.10", "anonymous access type for result for non-traversal functions"
    "violation-ownership-assign-to-expr", "SPARK RM 3.10(3)", "assignment to a complex expression"
    "violation-ownership-assign-to-constant", "SPARK RM 3.10(3)", "assignment into a constant object"
    "violation-ownership-borrow-of-constant", "SPARK RM 3.10(11)", "borrow of a constant object"
    "violation-ownership-borrow-of-non-markable", "SPARK RM 3.10(4)", "borrow or observe of an expression which is not part of stand-alone object or parameter"
    "violation-ownership-anonymous-component", "SPARK RM 3.10", "component of anonymous access type"
    "violation-ownership-deallocate-general", "SPARK RM 3.10(20)", "instance of Unchecked_Deallocation with a general access type"
    "violation-ownership-different-branches", "SPARK RM 3.10", "observe of a conditional or case expression with branches rooted in different objects"
    "violation-ownership-duplicate-aggregate-value", "SPARK RM 3.10", "duplicate value of a type with ownership"
    "violation-ownership-loop-entry-old-copy", "SPARK RM 3.10(13)", "prefix of Loop_Entry or Old attribute introducing aliasing"
    "violation-ownership-loop-entry-old-traversal", "SPARK RM 3.10(13)", "traversal function call as a prefix of Loop_Entry or Old attribute"
    "violation-ownership-move-constant-part", "SPARK RM 3.10(1)", "access-to-constant part of an object as source of move"
    "violation-ownership-move-in-declare", "SPARK RM 3.10", "move in declare expression"
    "violation-ownership-move-not-name", "SPARK RM 3.10(1)", "expression as source of move"
    "violation-ownership-move-traversal-call", "SPARK RM 3.10(1)", "call to a traversal function as source of move"
    "violation-ownership-reborrow", "SPARK RM 3.10(8)", "observed or borrowed expression which does not have the left-hand side as a root"
    "violation-ownership-storage-pool", "SPARK RM 3.10", "access type with Storage_Pool"
    "violation-ownership-tagged-extension", "SPARK RM 3.10(14)", "owning component of tagged extension"
    "violation-ownership-traversal-extended-return", "SPARK RM 3.10(6)", "extended return applying to a traversal function"
    "violation-ownership-volatile", "SPARK RM 3.10(16)", "observe, move, or borrow of volatile object"
    "violation-potentially-invalid-dispatch", "SPARK RM 13.9.1(9)", "dispatching operation with Potentially_Invalid aspect"
    "violation-potentially-invalid-invariant", "SPARK RM 13.9.1(7)", "potentially invalid object with a part subject to a type invariant"
    "violation-potentially-invalid-overlay", "SPARK RM 13.9.1(8)", "potentially invalid overlaid object"
    "violation-potentially-invalid-part-access", "SPARK RM 13.9.1(5)", "potentially invalid object with a part of an access type"
    "violation-potentially-invalid-part-concurrent", "SPARK RM 13.9.1(5)", "potentially invalid object with a part of a concurrent type"
    "violation-potentially-invalid-part-tagged", "SPARK RM 13.9.1(5)", "potentially invalid object with a part of a tagged type"
    "violation-potentially-invalid-part-unchecked-union", "SPARK RM 13.9.1(5)", "potentially invalid object with a part of an Unchecked_Union type"
    "violation-potentially-invalid-scalar", "SPARK RM 13.9.1(4)", "function returning a scalar that is not imported with Potentially_Invalid aspect"
    "violation-predicate-volatile", "SPARK RM 3.2.4(3)", "subtype predicate on effectively volatile type for reading"
    "violation-program-exit-outputs", "SPARK RM 6.1.10(1)", "output mentioned in the expression of an aspect Program_Exit which is not a stand-alone object"
    "violation-real-root", "", "expression of type root_real"
    "violation-relaxed-init-dispatch", "SPARK RM 6.10(10)", "dispatching operation with Relaxed_Initialization aspect"
    "violation-relaxed-init-initialized-prefix", "SPARK RM 6.10(4)", "attribute Initialized on a prefix which does not have relaxed initialization"
    "violation-relaxed-init-part-generic", "", "part of tagged, Unchecked_Union, or effectively volatile object or type annotated with relaxed initialization"
    "violation-relaxed-init-part-of-tagged", "SPARK RM 6.10(6)", "part of tagged type with relaxed initialization"
    "violation-relaxed-init-part-of-unchecked-union", "SPARK RM 6.10(8)", "part of Unchecked_Union type with relaxed initialization"
    "violation-relaxed-init-part-of-volatile", "SPARK RM 6.10(7)", "part of effectively volatile object or type annotated with relaxed initialization"
    "violation-side-effects-call-context", "SPARK RM 6.1.13(4)", "call to a function with side effects outside of assignment or object declaration without a block"
    "violation-side-effects-eq", "SPARK RM 6.1.13(8)", "function with side effects as user-defined equality on record type"
    "violation-side-effects-traversal", "SPARK RM 6.1.13(7)", "traversal function with side effects"
    "violation-storage-size", "", "access type with Storage_Size"
    "violation-subp-variant-structural", "SPARK RM 6.1.8(5)", "structural subprogram variant which is not a parameter of the subprogram"
    "violation-tagged-extension-local", "SPARK RM 3.9.1(1)", "local derived type from non-local parent or interface"
    "violation-target-name-in-call-with-side-effets", "SPARK RM 6.4.2(7)", "use of @ inside a call to a function with side effects"
    "violation-tasking-configuration", "", "SPARK violation related to tasking configuration"
    "violation-tasking-synchronized-comp", "SPARK RM 9(5)", "synchronized component of non-synchronized type"
    "violation-tasking-unintialized-concurrent", "SPARK RM 9(4)", "not fully initialized part of concurrent type"
    "violation-tasking-unsupported-construct", "", "tasking"
    "violation-uc-from-access", "SPARK RM 13.9(1)", "unchecked conversion instance from a type with access subcomponents"
    "violation-uc-to-access", "SPARK RM 13.9(2)", "unchecked conversion instance to an access type which is not a general access-to-object type"
    "violation-uc-to-access-components", "SPARK RM 13.9(2)", "unchecked conversion instance to a composite type with access subcomponents"
    "violation-uc-to-access-from", "SPARK RM 13.9(2)", "unchecked conversion instance to an access-to-object type from a type which is neither System.Address nor an integer type"
    "violation-unsupported-attribute", "", "unsupported attribute"
    "violation-unsupported-pragma", "", "unknown pragma"
    "violation-use-of-rejected-entity", "", "use of entity rejected by SPARK"
    "violation-volatile-at-library-level", "SPARK RM 7.1.3(3)", "effectively volatile type or object not at library level"
    "violation-volatile-discriminant", "SPARK RM 7.1.3(4)", "volatile discriminant"
    "violation-volatile-discriminated-type", "SPARK RM 7.1.3(5)", "discriminated volatile type"
    "violation-volatile-eq", "SPARK RM 7.1.3(10)", "volatile function as user-defined equality on record type"
    "violation-volatile-global", "SPARK RM 7.1.3(7)", "nonvolatile function with volatile global inputs"
    "violation-volatile-in-interferring-context", "SPARK RM 7.1.3(9)", "volatile object or volatile function call in interfering context"
    "violation-volatile-incompatible-comp", "SPARK RM 7.1.3(6)", "component of composite type or designated type of an access with an incompatible volatility"
    "violation-volatile-incompatible-type", "SPARK RM 7.1.3(2)", "standalone object with an incompatible volatility with respect to its type"
    "violation-volatile-loop-param", "SPARK RM 7.1.3(4)", "effectively volatile loop parameter"
    "violation-volatile-parameter", "SPARK RM 7.1.3(8)", "nonvolatile function with effectively volatile parameter"
    "violation-volatile-result", "SPARK RM 7.1.3(8)", "nonvolatile function with effectively volatile result"