Void-safe Option

Project configuration allows assigning the void safety status for the selected set of classes. In order to facilitate the migration of the existing code to meet the standard requirements, different levels of void safety can be used. They are described in the sections below. The validity rules that are affected by the void safety settings include 3 different sets:

1. VUTA - target of a feature call should be attached
2. VEVI - entity of an attached type should be properly set before use
3. VJAR and family - attachment status is taken into account when checking type conformance

Depending on the requested void safety level different validity rules are involved in checks.

Compatibility - none (no void safety)

No void safety checks are performed.

Standard - all (complete void safety)

All void safety checks are performed.

On-demand - initialization (selective void safety)

Some void safety checks are performed. Let's consider the validity rules listed above to see what are the dependencies among them. First, VUTA relies on the property of entities of an attached type to be really attached before they are used. In other words, VUTA checks are sound only when VEVI checks are performed. For example,

local
	a: attached ACCOUNT
do
	a.deposit (amount) -- Does not make sense to check VUTA here because VEVI is not satisfied
	...
end

On the other hand, VEVI validity rules cannot be ensured if attachment status is not taken into account when performing conformance checks. For example,

check_account (account: detachable ACCOUNT)
	local
		a: attached ACCOUNT
	do
		a := account -- Does not make sense to check VEVI here because VJAR is not satisfied
		...
	end

So, the on-demand void safety ensures that attached entities are properly set and takes attachment status into account when checking type conformance.