| | 429 | The system function `$assert` has the signature |
| | 430 | {{{ |
| | 431 | void $assert(_Bool expr, ...); |
| | 432 | }}} |
| | 433 | It consumes a boolean expression and any number of optional expressions which are used to construct an error message. |
| | 434 | Note that CIVL-C boolean expressions have a richer syntax than C expressions, and may include universal or existential quantifiers. |
| | 435 | During verification, the assertion is checked. |
| | 436 | If it cannot be proved that it must hold, a violation is reported, and, if additional arguments are present, a specific message is printed. |
| | 437 | These additional arguments are similar in form to those used in C’s `printf` statement: |
| | 438 | a format string, followed by some number of arguments which are evaluated and substituted for successive codes in the format string. |
| | 439 | For example, |
| | 440 | {{{ |
| | 441 | $assert(x<=B, "x-coordinate %f exceeds bound %f", x, B); |
| | 442 | }}} |
| | 443 | If x=3 and B=2, the assertion is violated and CIVL prints the error message “x-coordinate 3 exceeds bound 2”. |
| | 444 | |
