| | 776 | This is a function-like macro of one argument. |
| | 777 | The argument should be a side-effect-free expression of integer type. |
| | 778 | The macro expands to text which, when followed by `;`, yields a statement. |
| | 779 | The definition is: |
| | 780 | {{{ |
| | 781 | #define $elaborate(x) for(int _i = 0; _i < (x); _i++) |
| | 782 | }}} |
| | 783 | In the concrete semantics, this is no-op. |
| | 784 | However, in the symbolic semantics, it has the effect of forcing ''x'' to take on a concrete value. |
| | 785 | Let us assume ''x''≥0 is implied by the path condition. |
| | 786 | Then, each time the process completes one iteration of this loop, a nondeterministic choice is made to decide ''n''<''x'', where ''n'' is the current concrete value of `_i`. |
| | 787 | If the true branch is taken, then ''x''>''n'' is recorded in the path condition and control moves to the next iteration. |
| | 788 | If the false branch is taken, then ''x''=''n'' is recorded and control exits the loop with ''x'' now assigned a concrete value. |
| | 789 | Hence this effectively enumerates all possible concrete values of ''x''. |
| | 790 | As long as the path condition implies some concrete upper bound on ''x'', this will be a finite enumeration. |
| | 791 | If there is no such bound, the symbolic state space will be infinite, since the loop can iterate indefinitely. |
| | 792 | |
