Skip to content

Non-const static variables in headers #729

Description

@protz

Files: FStar_UInt128_Verified.h:121,286, fstar_uint128_msvc.h:216,424

static uint32_t FStar_UInt128_u32_64 = 64U;
static uint32_t FStar_UInt128_u32_32 = 32U;

Each translation unit gets its own mutable copy. Should be const to enable constant-folding and prevent accidental modification.

Test snippet:

// This compiles and silently corrupts all subsequent shift operations:
FStar_UInt128_u32_64 = 32;  // Oops -- now all 128-bit shifts are wrong

Suggested fix:

static const uint32_t FStar_UInt128_u32_64 = 64U;
static const uint32_t FStar_UInt128_u32_32 = 32U;

This issue was found by Claude (Opus 4.6)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions