Lines Matching refs:tmp
1093 uint64_t tmp = output[4U];
1101 output[0U] = tmp;
1129 uint64_t tmp[5U] = { 0U };
1140 memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1146 Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input21);
1216 Hacl_Bignum_Fsquare_fsquare_(FStar_UInt128_t *tmp, uint64_t *output)
1226 Hacl_Bignum_Fsquare_fsquare__(tmp, output);
1227 Hacl_Bignum_Fproduct_carry_wide_(tmp);
1228 - FStar_UInt128_t b4 = tmp[4U];
1229 - FStar_UInt128_t b0 = tmp[0U];
1234 + b4 = tmp[4U];
1235 + b0 = tmp[0U];
1241 tmp[4U] = b4_;
1242 tmp[0U] = b0_;
1243 Hacl_Bignum_Fproduct_copy_from_wide_(output, tmp);
1257 Hacl_Bignum_Fsquare_fsquare_times_(uint64_t *input, FStar_UInt128_t *tmp, uint32_t count1)
1260 Hacl_Bignum_Fsquare_fsquare_(tmp, input);
1263 Hacl_Bignum_Fsquare_fsquare_(tmp, input);
1336 uint64_t tmp[5U] = { 0U };
1342 memcpy(tmp, b, (uint32_t)5U * sizeof b[0U]);
1343 - uint64_t b0 = tmp[0U];
1344 - uint64_t b1 = tmp[1U];
1345 - uint64_t b2 = tmp[2U];
1346 - uint64_t b3 = tmp[3U];
1347 - uint64_t b4 = tmp[4U];
1348 + b0 = tmp[0U];
1349 + b1 = tmp[1U];
1350 + b2 = tmp[2U];
1351 + b3 = tmp[3U];
1352 + b4 = tmp[4U];
1353 tmp[0U] = b0 + (uint64_t)0x3fffffffffff68U;
1354 tmp[1U] = b1 + (uint64_t)0x3ffffffffffff8U;
1355 tmp[2U] = b2 + (uint64_t)0x3ffffffffffff8U;
1361 FStar_UInt128_t tmp[5U];
1370 tmp[_i] = FStar_UInt128_uint64_to_uint128((uint64_t)0U);
1374 tmp[4U] = FStar_UInt128_mul_wide(xi, s);
1376 Hacl_Bignum_Fproduct_carry_wide_(tmp);
1377 - FStar_UInt128_t b4 = tmp[4U];
1378 - FStar_UInt128_t b0 = tmp[0U];
1383 + b4 = tmp[4U];
1384 + b0 = tmp[0U];
1588 Hacl_Bignum_Fproduct_carry_wide_(uint64_t *tmp)
1594 uint64_t tctr = tmp[ctr];
1595 uint64_t tctrp1 = tmp[ctr + (uint32_t)1U];
1598 Hacl_Bignum_Fproduct_carry_limb_(uint32_t *tmp)
1604 uint32_t tctr = tmp[ctr];
1605 uint32_t tctrp1 = tmp[ctr + (uint32_t)1U];
1609 uint32_t tmp = output[4U];
1638 uint32_t tmp[5U] = { 0U };
1639 - memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1645 + memcpy(tmp, input, (uint32_t)5U * sizeof input[0U]);
1646 Hacl_Bignum_Fmul_mul_shift_reduce_(t, tmp, input2);
1677 tmp[0U] = r0;
1678 tmp[1U] = r1;
1679 tmp[2U] = r2;
1680 tmp[3U] = r3;
1681 tmp[4U] = r4;
1682 - uint32_t b4 = tmp[4U];
1684 + b4 = tmp[4U];
1686 tmp[4U] = b4_;
1687 Hacl_Bignum_AddAndMultiply_add_and_multiply(acc, tmp, r5);
1697 tmp[0U] = r0;
1698 tmp[1U] = r1;
1699 tmp[2U] = r2;
1700 tmp[3U] = r3;
1701 tmp[4U] = r4;
1710 Hacl_Bignum_AddAndMultiply_add_and_multiply(h, tmp, r);