Promela |
Extension |
c_code |
NAME
c_code -
embedded C code fragments.
SYNTAX
c_code { /* c code */ }
c_code '[' /* c expr */ ']' { /* c code */ ; }
EXECUTABILITY
true
EFFECT
As defined by the semantics of the C
code fragment placed between
the curly braces.
DESCRIPTION
The
c_code primitive supports the use of embedded C
code fragments inside Promela models.
The code must be syntactically valid C, and must be terminated by a
semicolon (a required statement terminator in C).
There are two forms of the c_code primitive: with or without an embedded expression in square brackets. A missing expression clause is equivalent to [ true ] . If an expression is specified, its value will be evaluated as a general C expression before the C code fragment inside the curly braces is executed. If the result of the evaluation is non-zero, the c_code fragment is executed. If the result of the evaluation is zero, the code between the curly braces is ignored, and the statement is treated as an assertion violation. The typical use of the expression clause is to add checks for nil-pointers or for bounds in array indices. For example:
c_code [Pex->ptr != 0 && now.i < 10 && now.i >= 0] {
Pex->ptr.x[now.i] = 12;
}
A
c_code fragment can appear anywhere in a Promela model, but it
must be meaningful within its context, as determined by the C
compiler that is used to compile the complete model checking
program that is generated by Spin from the model.
Function and data declarations, for instance, can be placed in global c_code fragments preceding all proctype definitions. Code fragments that are placed inside a proctype definition cannot contain function or data declarations. Violations of such rules are caught by the C compiler. The Spin parser merely passes all C code fragments through into the generated verifier uninterpreted, and therefore cannot detect such errors.
There can be any number of C statements inside a c_code fragment.
EXAMPLES
int q;
c_code { int *p; };
init {
c_code { *p = 0; *p++; };
c_code [p != 0] { *p = &(now.q); };
c_code { Printf("%d\n", Pinit->_pid); }
}
In this example we first declare a normal Promela integer variable
q that automatically becomes part of the verifier's internal
state vector (called
now ) during verification.
We also declare a global integer pointer
p in a global
c_code fragment.
Since the contents of a C
code fragment are not interpreted by Spin when
it generates the verifier, Spin cannot know about the presence of the
declaration for pointer variable
p , and therefore this variable remains invisible to the verifier:
its declaration appears outside the state vector.
It can be manipulated as shown as a regular global pointer variable,
but the values assigned to this variable are not considered
to be part of the global system state that the verifier tracks.
To arrange for data objects to appear inside the state vector, and to be treated as system state variables, one or more of the primitives c_decl , c_state , and c_track should be used (for details, see the corresponding manual pages).
The local c_code fragment inside the init process manipulates the variable p in a direct way. Since the variable is not moved into the state vector, no prefix is needed to reference it.
In the second c_code fragment in the body of init , an expression clause is used that verifies that the pointer p has a non-zero value, which secures that the dereference operation that follows cannot result in a memory fault. (Of course, it would be wiser to add this expression clause also to the preceding c_code statement.) When the c_code statement is executed, the value of p is set to the address of the Promela integer variable q . Since the Promela variable is accessed inside a c_code fragment, we need a special prefix to identify it in the global state vector. For a global variable, the required prefix is the three-letter word now followed by a period. The ampersand in &(now.q) takes the address of the global variable within the state vector.
The last c_code statement in init prints the value of the process identifier for the running process. This is a predefined local variable.
To access the local variable in the init process, the required prefix is Pinit-> . This format consists of the uppercase letter P , followed by the name of the process type, followed by an arrow -> .
See also the description on data access in c_expr .
NOTES
The embedded C
code fragments must be syntactically correct and complete.
That is, they must contain proper punctuation with semicolons, using
the standard semantics from C, not from Promela.
Note, for instance, that semicolons are statement terminators in C,
but statement separators in Promela.
Because embedded C code is not interpreted by the Spin parser, inline parameter substitutions are not applied to those code fragments. In cases where this is needed, the inline definitions can be replaced with macro preprocessor definitions.
A common use of the c_code primitive is to include a larger piece of code into a model that is stored in a separate file, for instance, as follows:
c_code {
#include "someheaders.h"
#include "someCcode.c"
};
If the included code fragment is too large (in the current implementation
of Spin this means larger than about 64Kbyte of text), Spin will complain
about that and fail.
A simple way to bypass this restriction,
for instance, when generating the verification code with Spin's
-a option, is to defer the interpretation of the
include directives by the Spin preprocessor, and to copy them through into the generated
code unseen.
This can be accomplished as follows, by placing a backslash before
the pound sign of any
include directive that appears inside a
c_code primitive.
c_code {
\#include "someheaders.h"
\#include "someCcode.c"
};
Functionally, this is identical to the previous version, but it
makes sure that the Spin preprocessor will not read in the text
of the included files when the model is parsed.
SEE ALSO
c_expr
c_decl
c_state
c_track
macros
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |