Chapter 17. Embedded C Code
“The purpose of analysis is not to compel belief but rather to suggest doubt.”
|--(Imre Lakatos, Proofs and Refutations)|
SPIN, versions 4.0 and later, support the inclusion of embedded C code into PROMELA models through the following five new primitives:
c_expr, c_code, c_decl, c_state, c_track
The purpose of these new primitives is primarily to provide support for automatic model extraction from C code. This means that it is not the intent of these extensions to be used in manually constructed models. The primitives provide a powerful extension, opening SPIN models to the full power of, and all the dangers of, arbitrary C code. The contents of the embedded code fragments cannot be checked by SPIN, neither in the parsing ...