Lines Matching refs:t
133 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fmul_fmul() local
137 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fmul_fmul()
148 Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2); in Hacl_Bignum_Fmul_fmul()
149 Hacl_Bignum_Fproduct_carry_wide_(t); in Hacl_Bignum_Fmul_fmul()
150 b4 = t[4U]; in Hacl_Bignum_Fmul_fmul()
151 b0 = t[0U]; in Hacl_Bignum_Fmul_fmul()
157 t[4U] = b4_; in Hacl_Bignum_Fmul_fmul()
158 t[0U] = b0_; in Hacl_Bignum_Fmul_fmul()
159 Hacl_Bignum_Fproduct_copy_from_wide_(output, t); in Hacl_Bignum_Fmul_fmul()
262 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fsquare_fsquare_times() local
266 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fsquare_fsquare_times()
269 Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1); in Hacl_Bignum_Fsquare_fsquare_times()
277 FStar_UInt128_uint128 t[5U]; in Hacl_Bignum_Fsquare_fsquare_times_inplace() local
281 t[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U); in Hacl_Bignum_Fsquare_fsquare_times_inplace()
283 Hacl_Bignum_Fsquare_fsquare_times_(output, t, count1); in Hacl_Bignum_Fsquare_fsquare_times_inplace()