4244 	u64 high_bits_rsvd;  in __reset_rsvds_bits_mask()  local
4252 		high_bits_rsvd = pa_bits_rsvd & rsvd_bits(0, 62);  in __reset_rsvds_bits_mask()
4254 		high_bits_rsvd = pa_bits_rsvd & rsvd_bits(0, 51);  in __reset_rsvds_bits_mask()
4258 		high_bits_rsvd |= rsvd_bits(63, 63);  in __reset_rsvds_bits_mask()
4289 						   high_bits_rsvd |  in __reset_rsvds_bits_mask()
4292 		rsvd_check->rsvd_bits_mask[0][1] = high_bits_rsvd;	/* PDE */  in __reset_rsvds_bits_mask()
4293 		rsvd_check->rsvd_bits_mask[0][0] = high_bits_rsvd;	/* PTE */  in __reset_rsvds_bits_mask()
4294 		rsvd_check->rsvd_bits_mask[1][1] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4300 		rsvd_check->rsvd_bits_mask[0][4] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4307 		rsvd_check->rsvd_bits_mask[0][3] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4310 		rsvd_check->rsvd_bits_mask[0][2] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4312 		rsvd_check->rsvd_bits_mask[0][1] = high_bits_rsvd;  in __reset_rsvds_bits_mask()
4313 		rsvd_check->rsvd_bits_mask[0][0] = high_bits_rsvd;  in __reset_rsvds_bits_mask()
4316 		rsvd_check->rsvd_bits_mask[1][2] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4319 		rsvd_check->rsvd_bits_mask[1][1] = high_bits_rsvd |  in __reset_rsvds_bits_mask()
4357 	u64 high_bits_rsvd = pa_bits_rsvd & rsvd_bits(0, 51);  in __reset_rsvds_bits_mask_ept()  local
4360 	rsvd_check->rsvd_bits_mask[0][4] = high_bits_rsvd | rsvd_bits(3, 7);  in __reset_rsvds_bits_mask_ept()
4361 	rsvd_check->rsvd_bits_mask[0][3] = high_bits_rsvd | rsvd_bits(3, 7);  in __reset_rsvds_bits_mask_ept()
4362 	rsvd_check->rsvd_bits_mask[0][2] = high_bits_rsvd | rsvd_bits(3, 6);  in __reset_rsvds_bits_mask_ept()
4363 	rsvd_check->rsvd_bits_mask[0][1] = high_bits_rsvd | rsvd_bits(3, 6);  in __reset_rsvds_bits_mask_ept()
4364 	rsvd_check->rsvd_bits_mask[0][0] = high_bits_rsvd;  in __reset_rsvds_bits_mask_ept()
4369 	rsvd_check->rsvd_bits_mask[1][2] = high_bits_rsvd | rsvd_bits(12, 29);  in __reset_rsvds_bits_mask_ept()
4370 	rsvd_check->rsvd_bits_mask[1][1] = high_bits_rsvd | rsvd_bits(12, 20);  in __reset_rsvds_bits_mask_ept()