7.2.7.5. Error Messages For SPARK Violations

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

Violation Tag

SRM Reference

Explanation

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