C++: Range analysis guard improvement

[paldepind]

This PR changes how bounds are adjusted for integral types.

As an example, if we have a strict lower bound > 1 on an integer then the lower bound is 2. As of now, this is achieved by adding 1 to the lower bound. However, this adjustment is not always correct.

For this guard, where e is an integer:

(2 * e + 1) > 0

We deduce a lower bound of > -0.5 and after adding 1 we get 0.5. For such a fractional lower bound adding 1 doesn't really make sense. This PR tweaks this slightly, such that the lower bound ends up being 0. A similar adjustment is made for upper bounds.

I ran into this when debugging a performance issue where this showed up. This adjustment didn't fix the performance issue, but I think it's still worthwhile.

Per-commit review is suggested — I also snuck in a few orthogonal changes.

I think the DCA report seems uneventful.

[Copilot]

Pull Request Overview

This PR improves how bounds are adjusted for integral types in C++ range analysis. Instead of simply adding/subtracting 1 to adjust bounds from fractional values like -0.5 to 0.5, it now properly handles the conversion to integer bounds by using floor operations to compute more accurate integer bounds.

Key changes:

• Introduces new helper functions adjustLowerBoundIntegral and adjustUpperBoundIntegral for proper bound adjustment
• Replaces simple arithmetic adjustment with floor-based calculations that handle fractional bounds correctly

Reviewed Changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
SimpleRangeAnalysis.qll	Adds new adjustment functions and updates bound calculation logic for integral types
RangeAnalysisUtils.qll	Adds toString method to RelationStrictness class and improves documentation
test.c	Adds new test cases for inequality-derived integer bounds
upperBound.expected	Updated test expectations reflecting improved bound calculations
ternaryUpper.expected	Updated test expectations for ternary expressions
ternaryLower.expected	Updated test expectations for ternary expressions
lowerBound.expected	Updated test expectations reflecting improved bound calculations

[paldepind]

I'm putting this PR back in draft. I have an internal PR that adds new ceilFloat and floorFloat member predicates to float. If these are added we could do a cleaner implementation here.

[paldepind]

I've rebased the PR and updated it to use the new ceilFloat and floorFloat predicates.

[jketema]

LGTM

[paldepind]

Thanks for reviewing :)