Searched defs:vcpu_write_reg (Results 1 - 1 of 1) sorted by relevance
| /seL4-refos-master/kernel/include/arch/arm/arch/object/ | ||
| H A D | vcpu.h | 178 static inline void vcpu_write_reg(vcpu_t *vcpu, word_t reg, word_t value) function |
Completed in 22 milliseconds