dc45444e |
1 | #define rwoff1 (write_off - read_off >= 0) |
2 | #define rwoff2 (write_off - read_off < HALF_UCHAR) |
3 | |
4 | #define wcsum1 (write_off - _commit_sum >= 0) |
5 | #define wcsum2 (write_off - _commit_sum < HALF_UCHAR) |
6 | |
7 | #define buffer_large_enough (NUMPROCS + NUMSWITCH <= BUFSIZE) |
8 | #define have_events_lost (events_lost != 0) |
9 | never { /* !( []((buffer_large_enough) -> (!have_events_lost))) */ |
10 | T0_init: |
11 | if |
12 | :: ((buffer_large_enough) && (have_events_lost)) -> goto accept_all |
13 | :: (1) -> goto T0_init |
14 | fi; |
15 | accept_all: |
16 | skip |
17 | } |