133       uint64_t i1;  in Hacl_Bignum_Fmul_fmul()  local
146       i1 = output[1U];  in Hacl_Bignum_Fmul_fmul()
148       i1_ = i1 + (i0 >> (uint32_t)51U);  in Hacl_Bignum_Fmul_fmul()
186   uint64_t i1;  in Hacl_Bignum_Fsquare_fsquare_()  local
199   i1 = output[1U];  in Hacl_Bignum_Fsquare_fsquare_()
201   i1_ = i1 + (i0 >> (uint32_t)51U);  in Hacl_Bignum_Fsquare_fsquare_()
419   uint64_t i1 = load64_le(x00);  in Hacl_EC_Format_fexpand()  local
427   uint64_t output1 = i1 >> (uint32_t)3U & (uint64_t)0x7ffffffffffffU;  in Hacl_EC_Format_fexpand()
491   uint64_t i1;  in Hacl_EC_Format_fcontract_second_carry_full()  local
497   i1 = input[1U];  in Hacl_EC_Format_fcontract_second_carry_full()
499   i1_ = i1 + (i0 >> (uint32_t)51U);  in Hacl_EC_Format_fcontract_second_carry_full()
704     uint32_t i1 = i - (uint32_t)1U;  in Hacl_EC_Ladder_BigLoop_cmult_big_loop()  local
705     uint8_t byte = n1[i1];  in Hacl_EC_Ladder_BigLoop_cmult_big_loop()
707     Hacl_EC_Ladder_BigLoop_cmult_big_loop(n1, nq, nqpq, nq2, nqpq2, q, i1);  in Hacl_EC_Ladder_BigLoop_cmult_big_loop()