Integer Promotion Rejects Enum Operands

[mgordon]

CodeHawk-C Issue: Integer Promotion Rejects Enum Operands

Summary

CodeHawk-C can crash while checking arithmetic proof obligations involving enum
values. C allows enum values in integer arithmetic, but
get_integer_promotion only accepts TInt operands.

SPEC Trigger

SPEC CPU2017 perlbench, ext/re/re_exec.c, function S_isGCB:

#define GCBcase(before, after) ((GCB_ENUM_COUNT * before) + after)
switch (GCBcase(before, after)) {

Observed failure:

CCHFailure in function: S_isGCB:
Failure Unexpected types for integer promotion:
int and enum __anonenum_GCB_enum_...
for ppo 8: uint-overflow(...)

Small Reproducer

See repros/enum_integer_promotion.c.

Likely Cause

cCHTypesUtil.ml:get_integer_promotion matches only:

TInt (ik1, _), TInt (ik2, _)

It rejects TEnum operands rather than converting the enum to its underlying
integer kind for the usual arithmetic conversions.

Minimal Fix

Normalize TEnum operands to TInt (enum.ekind, []) before applying existing
integer-promotion logic.

enum_integer_promotion.c