NAME
local
-
for marking a global variable as being used by only one process.
SYNTAX
local
typename ivar DESCRIPTION
The keyword
local
can be used to prefix the declaration of any global variable.
It persuades the partial order reduction algorithm in the
model checker to treat the variable as if it were declared
local to a single process.
The addition of this prefix can affect only the verification
process.
EXAMPLES
local byte a;
local short p[3];
NOTES
If in effect the variable marked as
local
is accessed by more than one process, the
result of a verification may be rendered incomplete.
As yet there is no run-time check to detect such cases.
In a future revision the check is likely to be added though.
SEE ALSO
datatypes(2), hidden(2), show(2), _(5).
|