Promela V4 Reference -- c_expr(7)




c_expr - conditional expressions as embedded C code.

c_expr { /* c code */ }
c_expr '[' /* c expr */ ']' { /* c code */ }

If the return value of the arbitrary C code fragment that appears between the curly braces is non-zero, then true; otherwise false.

As defined by the semantics of the C code fragment that is placed between the curly braces. The evaluation of the C code fragment should have no side effects.

This primitive supports the use of embedded C code inside Promela models. A c_expr can be used to express guard conditions that are not necessarily expressible in Promela with its more restrictive data types and language constructs.

There are two forms of the c_expr primitive: with or without an additional assertion expression in square brackets. A missing assertion expression is equivalent to [ 1 ] . If an assertion expression is specified, its value is evaluated as a general C expression before the code inside the curly braces is evaluated. The normal (expected) case is that the assertion expression evaluates to a non-zero value (that is to an equivalent of the boolean value true). If so, the C code between the curly braces is evaluated next to determine the executability of the c_expr as a whole.

If the evaluation value of the assertion expression is zero (equivalent to false), the code between the curly braces is ignored and the statement is treated as an assertion violation.

The typical use of the assertion expression clause is to add checks for nil-pointers or for possible array bound violations in expressions. For example:

Note that there is no semicolon at the end of either C expression. If the expression between square brackets yields false (zero), then an assertion violation is reported. Only if this expression yields true (non-zero), is the C expression between curly braces evaluated. If the value of this second expression yields true, the c_expr as a whole is deemed executable and can be passed; if false, the c_expr is unexecutable and blocks.

The following example contains a do-loop with four options. The first two options are equivalent, the only difference being in the way that local variable x is accessed: either via an embedded C code fragment or with the normal Promela constructs.

The local variable x is declared here as a Promela variable. Other primitives, such as c_decl , c_state , and c_track allow for the declaration of data types that are not directly supported in Promela.

The references to local variable x have a pointer prefix that always starts with a fixed capital letter P that is followed by the name of the proctype and an pointer arrow. This prefix locates the variable in the local state vector of the proctype instantiation.

The guard of the third option sequence invokes an externally defined C function named fct() that is presumed to return an integer value. This function can be declared in a global c_code fragment elsewhere in the model, or it can be declared externally in separately compiled code that is linked with the pan.[chtmb] verifier when it is compiled.

Note that there is no semicolon before the closing curly brace of a c_expr construct. It causes a C syntax error if such a semicolon appears here. All syntax errors on embedded C code fragments are reported during the compilation of the generated pan.[chtmb] files. These errors are not detectable by the Spin parser.

Because embedded C code is not processed 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.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 15 January 2013)