Add operation names to integer overflow messages and checks

[sim642]

TODO

• Extend for Add cast kinds in CIL #1894: Add cast kinds to integer overflow messages #1896.

[michael-schwarz]

Why introduce polymorphic variants here? In other places we got rid of them for performance reasons.

[Copilot]

Pull request overview

This PR adds operation names to integer overflow warning messages, making them more informative by indicating which specific operation (e.g., +, -, *, /, <<, cast) caused the potential overflow. The implementation refactors the overflow checking infrastructure to pass operation information through the analysis pipeline.

Key Changes

• Refactored set_overflow_flag to add_overflow_check with a new overflow_op type that captures the operation (binary op, unary op, cast, or internal)
• Updated all overflow-checked operations to pass the appropriate operation identifier
• Enhanced warning messages to include operation names (e.g., "Signed integer overflow in +" instead of just "Signed integer overflow")

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/cdomain/value/cdomains/intDomain0.ml	Introduces overflow_op type and refactors set_overflow_flag to add_overflow_check with operation name formatting logic and improved safe message handling
src/cdomain/value/cdomains/int/intDomTuple.ml	Updates overflow checking to pass operation identifiers; includes optimization in create2_ovc to reuse computed overflow values instead of recomputing them
tests/regression/cfg/issue-1356.t/run.t	Updates test expectation for subtraction overflow message to include " in -"
tests/regression/cfg/foo.t/run.t	Updates test expectations for addition and subtraction overflow messages
tests/regression/39-signed-overflows/15-div-minus-1.t	Updates test expectations for division overflow messages to include " in /"
tests/regression/29-svcomp/36-svcomp-arch.t	Updates test expectation for multiplication overflow message to include " in *"
tests/regression/29-svcomp/34-verifier-assert-def.t	Updates test expectation for left shift overflow message to include " in <<"
tests/regression/29-svcomp/32-no-ov.t	Updates test expectations for multiple operations (left shift, subtraction, cast) to include operation names

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[sim642]

Why introduce polymorphic variants here? In other places we got rid of them for performance reasons.

I think I expected that perhaps with #1896 it might allow more type-safety but I don't think it became relevant anywhere, so I can just change it.