Promela primitives implementing C code: Several Promela primitives can be used to connect a verification model to implementation-level C code:
c_decl introduces the types and names of externally declared C data objects that are referenced in the model.
c_track defines the data objects that appear in the embedded C code that should be considered to hold state information during model checking.
c_code encloses an arbitrary fragment of C code.
c_expr evaluates a C expression to a Boolean value.