File: krmllib/c/fstar_uint128_msvc.h:107
Missing ) in the non-optimized path of FStar_UInt128_add_underspec. This path is compiled when targeting 32-bit MSVC (_MSC_VER defined but _M_X64 not defined).
// CURRENT (BROKEN):
lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low;
// ^ missing ')'
Test snippet:
// Compile on 32-bit MSVC (cl /c /D_MSC_VER /DKRML_VERIFIED_UINT128 test.c):
// error C2143: syntax error: missing ')' before ';'
Suggested fix:
lit.high = a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low);
This issue was found by Claude (Opus 4.6)
File:
krmllib/c/fstar_uint128_msvc.h:107Missing
)in the non-optimized path ofFStar_UInt128_add_underspec. This path is compiled when targeting 32-bit MSVC (_MSC_VERdefined but_M_X64not defined).Test snippet:
Suggested fix:
This issue was found by Claude (Opus 4.6)