IBM
Contents Index Previous Next



Using Assertions


Like most other run-time libraries to the SDL to C Compiler, the Explorer library gives the user a possibility to define his own run-time errors or assertions. An assertion is a test that is performed at run-time, for example to check that the value of a specific variable is within the expected range. Assertions are described by introducing #CODE directives with calls to the C function xAssertError in a TASK. See the following example.

Example 345 : Assertion in C Code

TASK '' /*#CODE
#ifdef XASSERT
  if (#(I) < #(K))
    xAssertError("I is less than K");
#endif
*/ ;

In the SDL Explorer, the assertions are checked during state space exploration. Whenever xAssertError is called during the execution of a transition, a report is generated. The advantage of using this way to define assertions, as opposed to using user-defined rules, is that in-line assertions are computed much more efficiently by the explorer than the user-defined rules.

The xAssertError function, which has the following prototype:

extern void xAssertError ( char *Descr )

takes a string describing the assertion as parameter and will produce an SDL run-time error similar to the normal run-time errors. The function is only available if the compilation switch XASSERT is defined. For the standard libraries this is true for all libraries except the Application Library.


http://www.ibm.com/rational
Contents Index Previous Next