diff options
Diffstat (limited to 'security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h')
| -rw-r--r-- | security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h index c3e86ca512..162dd66edf 100644 --- a/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h +++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum25519_51.h @@ -84,6 +84,7 @@ Hacl_Impl_Curve25519_Field51_fmul( uint64_t *f2, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -166,6 +167,7 @@ Hacl_Impl_Curve25519_Field51_fmul2( uint64_t *f2, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f1[0U]; uint64_t f11 = f1[1U]; uint64_t f12 = f1[2U]; @@ -371,6 +373,7 @@ Hacl_Impl_Curve25519_Field51_fmul1(uint64_t *out, uint64_t *f1, uint64_t f2) static inline void Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f0 = f[0U]; uint64_t f1 = f[1U]; uint64_t f2 = f[2U]; @@ -446,6 +449,7 @@ Hacl_Impl_Curve25519_Field51_fsqr(uint64_t *out, uint64_t *f, FStar_UInt128_uint static inline void Hacl_Impl_Curve25519_Field51_fsqr2(uint64_t *out, uint64_t *f, FStar_UInt128_uint128 *uu___) { + KRML_HOST_IGNORE(uu___); uint64_t f10 = f[0U]; uint64_t f11 = f[1U]; uint64_t f12 = f[2U]; |