@@ -151,6 +151,41 @@ private class CastEnumToIntegerSimpleRange extends SimpleRangeAnalysisExpr, Cast
151151 override predicate dependsOnChild ( Expr child ) { child = getExpr ( ) }
152152}
153153
154+ /**
155+ * A range analysis extension that supports `%=`.
156+ */
157+ private class RemAssignSimpleRange extends SimpleRangeAnalysisExpr , AssignRemExpr {
158+ override float getLowerBounds ( ) {
159+ exists ( float maxDivisorNegated , float dividendLowerBounds |
160+ // Find the max divisor, negated e.g. `%= 32` would be `-31`
161+ maxDivisorNegated = ( getFullyConvertedUpperBounds ( getRValue ( ) ) .abs ( ) - 1 ) * - 1 and
162+ // Find the lower bounds of the dividend
163+ dividendLowerBounds = getFullyConvertedLowerBounds ( getLValue ( ) ) and
164+ // The lower bound is caluclated in two steps:
165+ // 1. Determine the maximum of the dividend lower bound and maxDivisorNegated.
166+ // When the dividend is negative this will result in a negative result
167+ // 2. Find the minimum with 0. If the divided is always >0 this will produce 0
168+ // otherwise it will produce the lowest negative number that can be held
169+ // after the modulo.
170+ result = 0 .minimum ( dividendLowerBounds .maximum ( maxDivisorNegated ) )
171+ )
172+ }
173+
174+ override float getUpperBounds ( ) {
175+ // TODO rem zero?
176+ exists ( float maxDivisor , float maxDividend |
177+ // The maximum divisor value is the absolute value of the divisor minus 1
178+ maxDivisor = getFullyConvertedUpperBounds ( getRValue ( ) ) .abs ( ) - 1 and
179+ // value if > 0 otherwise 0
180+ maxDividend = getFullyConvertedUpperBounds ( getLValue ( ) ) .maximum ( 0 ) and
181+ // In the case the numerator is definitely less than zero, the result could be negative
182+ result = maxDividend .minimum ( maxDivisor )
183+ )
184+ }
185+
186+ override predicate dependsOnChild ( Expr expr ) { expr = getAChild ( ) }
187+ }
188+
154189/**
155190 * <stdio.h> functions that read a character from the STDIN,
156191 * or return EOF if it fails to do so.
0 commit comments