Boogie 3.x reserved identifiers are missing from Naming::BPL_KW #842

Summary

SMACK's manually maintained Naming::BPL_KW list is behind the Boogie 3.x grammar. A source/LLVM identifier that is missing from this list can be emitted unchanged even when Boogie now tokenizes it as a keyword, making otherwise valid generated BPL fail during parsing.

This occurred with a C global named action:

static char action[16];

SMACK emitted:

const {:allocSize 16} action: ref;

Corral using Boogie 3.5.7 rejected the action token with:

error: invalid Ident

The same generated BPL is accepted by the older Boogie 2.9.1 backend. Boogie 3.5.6 rejects it as well, so this appears to be a Boogie 2.x-to-3.x compatibility issue in SMACK's identifier sanitization rather than a 3.5.7-only problem.

The current list is here:
https://github.com/smackers/smack/blob/main/lib/smack/Naming.cpp#L156-L161

Rough keyword audit

Comparing Naming::BPL_KW with the literals recognized by Boogie 3.5.7's Scanner.CheckLiteral gives 29 Boogie keywords that are absent from SMACK:

RNE RNA RTN RTP RTZ
action asserts atomic both datatype hide hideable is left measure pop
preserves pure push refines reveal revealed right
roundNearestTiesToAway roundNearestTiesToEven
roundTowardNegative roundTowardPositive roundTowardZero
uses

Boogie's current Ident grammar contextually converts these eight tokens back into identifiers:

atomic both hide left pop push reveal right

That leaves roughly 21 plausible hard collisions:

RNE RNA RTN RTP RTZ
action asserts datatype hideable is measure preserves pure refines revealed
roundNearestTiesToAway roundNearestTiesToEven
roundTowardNegative roundTowardPositive roundTowardZero
uses

This is a lexical/parser audit, not a claim that all 21 names have been reproduced individually.

SMACK also retains complete, finite, and par, which are not scanner literals in Boogie 3.5.7. Keeping those conservatively escaped appears harmless.

Expected behavior

All source/LLVM names should be mapped to identifiers that are valid for the supported Boogie version. In particular, action should be emitted according to SMACK's existing suffix policy as action_ (or otherwise escaped consistently) rather than as a bare keyword.

Suggested direction

• Add action and the other hard-reserved Boogie 3.x identifiers to BPL_KW.
• Preserve the existing _ suffix policy used by Naming::get.
• Add a small regression test containing a file-scope object named action.
• Consider a test or generated list that reduces future drift between SMACK and its supported Boogie grammar.

Related: #45, which addressed the same class of collision for older Boogie keywords.