Promela V4 Reference -- c_decl(7)

Promela

Extension

c_decl


NAME
c_decl , c_state , c_track - embedded C data declarations.

SYNTAX
c_decl { /* c declaration */ }
c_state string string [ string ]
c_track string string [ string ]

EXECUTABILITY
true

DESCRIPTION
The primitives c_decl , c_state , and c_track are global primitives that can only appear in a model as global declarations outside all proctype declarations.

The c_decl primitive provides a capability to embed general C data type declarations into a model. These type declarations are placed in the generated pan.h file before the declaration of the state-vector structure, which is also included in that file. This means that the data types introduced in a c_decl primitive can be referenced anywhere in the generated code, including inside the state vector with the help of c_state primitives. Data type declarations can also be introduced in global c_code fragments, but in this case the generated code is placed in the pan.c file, and therefore appears necessarily after the declaration of the state-vector structure. Therefore, these declarations cannot be used inside the state vector.

The c_state keyword is followed by either two or three quoted strings. The first argument specifies the type and the name of a data object. The second argument the scope of that object. A third argument can optionally be used to specify an initial value for the data object. (It is best not to assume a known default initial value for objects that are declared in this way.)

There are three possible scopes: global, local, or hidden. A global scope is indicated by the use of the quoted string "Global." If local, the name Local must be followed by the name of the proctype in which the declaration is to appear, as in "Local ex2." If the quoted string "Hidden" is used for the second argument, the data object will be declared as a global object that remains outside the state vector.

The primitive c_track is a global primitive that can declare any state object, or more generally any piece of memory, as holding state information. This primitive takes two string arguments. The first argument specifies an address, typically a pointer to a data object declared elsewhere. The second argument gives the size in bytes of that object, or more generally the number of bytes starting at the address that must be tracked as part of the system state.

EXAMPLES
The first example illustrates how c_decl , c_code and c_state declarations can be used to define either visible or hidden state variables, referring to type definitions that must precede the internal Spin state-vector declaration. For an explanation of the rules for prefixing global and local variables inside c_code and c_expr statements, see the manual pages for these two statements.

The c_track statement can have a third argument that must be one of the words: "UnMatched" or "StackOnly" in double quotes. For instance Without the third argument, the default behavior for c_track is equivalent to "Matched".

If "UnMatched" or "StackOnly" is present, it means that the data object is tracked on the stack, but its value is not considered to be part of the system state. So, the concrete value is accurately maintained during the depth-first search, while separately an abstract version of the same value can be stored in the statespace, as explained in this paper on Model Driven Software Verification.

NOTES
Spin instruments the code of the verifier to copy all data pointed to via c_track primitives into and out of the state vector on forward and backward moves during the depth-first search that it performs. Where there is a choice, the use of c_state primitives will always result in more efficiently executed code, since Spin can instrument the generated verifier to directly embed data objects into the state vector itself, avoiding the copying process.

To get a better feeling for how precisely these primitives are interpreted by Spin, consider generating code from the last example, and look in the generated files pan.h and pan.c for all appearances of variables R1 , R2 , P1 , and up0 .

Avoid using type-names that clash with internal types used within the Spin-generated verifiers. This includes names such as State , P0 , P1 , etc., and Q0 , Q1 , etc. Name clashes caused by unfortunate choices of type names are reliably caught by the C compiler when the verification code is compiled.

SEE ALSO
c_expr
c_code


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 15 October 2014)