Lines Matching defs:t01
293 uint64_t *t01;
307 t01 = buf + (uint32_t)5U;
310 Hacl_Bignum_Fmul_fmul(b1, t01, b1);
311 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)10U);
312 Hacl_Bignum_Fmul_fmul(c0, t01, b1);
313 Hacl_Bignum_Fsquare_fsquare_times(t01, c0, (uint32_t)20U);
314 Hacl_Bignum_Fmul_fmul(t01, t01, c0);
315 Hacl_Bignum_Fsquare_fsquare_times_inplace(t01, (uint32_t)10U);
316 Hacl_Bignum_Fmul_fmul(b1, t01, b1);
317 Hacl_Bignum_Fsquare_fsquare_times(t01, b1, (uint32_t)50U);