Embedding C Code: Promela supports the use of embedded C code fragments inside the models through the use of the c_code primitive.
For example:
If the logical expression is specified, its value is evaluated before the c_code fragment inside the curly braces is executed. If the result of the assessment is non-zero, the c_code fragment is executed. If the outcome of the evaluation is zero, the code between curly braces is ignored, and the statement is treated as an assertion violation. The example above adds checks for null pointers and bounds on array indices.
Many other code verifiers which do not necessarily use Promela as their modeling language use SPIN as a back-end verifier.