CURRENT_CPU_INDEX() is supported to return a word_t. The C parser from the verification toolchain requires declaring word_t constants without casting integer values to word_t. Signed-off-by: Axel Heider <axelheider@gmx.de> |
||
|---|---|---|
| .. | ||
| preemption.h | ||
| smp.h | ||
| statedata.h | ||