Lines Matching refs:bits
66 /* Cache the values that we calculated for bits that need to be set high
175 print_bits(word_t bits)
178 while (bits) {
179 int index = seL4_WordBits - 1 - clzl(bits);
186 bits &= ~BIT(index);
195 /* check if any bits that should be high, are not
196 * high & val represents the set of bits that are
199 * bits were not high we can invert and mask with
205 printf("Failed to set bits: ");
213 printf("Incorrectly cleared bits: ");
256 /* Read out the fixed high and low bits from the MSRs */
315 /* See if the hardware requires bits that require to be high to be low */
338 /* Force the bits we require to be high */
381 /* We want to check that any bits that there are no bits that this core
384 * Also need to make sure that the BSP has not determined that any bits should
1170 /* the basic exit reason is the bottom 16 bits of the exit reason field */
1196 /* The exception number is the bottom 8 bits of the interrupt info */
1207 * manipulate bits that are not task switch, so we still have to be careful and propogate
1233 * to consider bits that the hardware will not have handled without faulting, which
1235 * bits that the VCPU owner has declared that they want to own (via the cr0_shadow)
1256 * to consider bits that the hardware will not have handled without faulting, which
1258 * bits that the VCPU owner has declared that they want to own (via the cr0_shadow).
1259 * Additionally since LMSW only loads the bottom 4 bits of CR0 we only consider
1260 * the low 4 bits
1397 /* if the vcpu actually owns the fpu then we do not need to change any bits