summaryrefslogtreecommitdiffstats
path: root/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
diff options
context:
space:
mode:
Diffstat (limited to 'security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h')
-rw-r--r--security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
index 33cff6b6d4..51c2325854 100644
--- a/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
+++ b/security/nss/lib/freebl/verified/karamel/krmllib/dist/minimal/fstar_uint128_gcc64.h
@@ -148,7 +148,7 @@ FStar_UInt128_eq_mask(uint128_t x, uint128_t y)
{
uint64_t mask =
FStar_UInt64_eq_mask((uint64_t)(x >> 64), (uint64_t)(y >> 64)) &
- FStar_UInt64_eq_mask(x, y);
+ FStar_UInt64_eq_mask((uint64_t)x, (uint64_t)y);
return ((uint128_t)mask) << 64 | mask;
}
@@ -158,7 +158,7 @@ FStar_UInt128_gte_mask(uint128_t x, uint128_t y)
uint64_t mask =
(FStar_UInt64_gte_mask(x >> 64, y >> 64) &
~(FStar_UInt64_eq_mask(x >> 64, y >> 64))) |
- (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask(x, y));
+ (FStar_UInt64_eq_mask(x >> 64, y >> 64) & FStar_UInt64_gte_mask((uint64_t)x, (uint64_t)y));
return ((uint128_t)mask) << 64 | mask;
}