Currently, the default (range-based) constrain manager supports symbolic expressions of the format "symbol + integer" or "symbol - integer" to compare them to another integer. However, multiplication and division is not supported yet.
An example where this lack of support causes false positives is the following:
```
unsigned size = 32;
int init(int *s);
void assert(int);
static void test(void)
{
int val;
if (size>10 && size<=100){
for (unsigned j = 0; j<size/2; j++)
init(&val);
assert((int) (val == 1)); //False positive: val may be uninitialized
}
}
```
In this example the loop executes at least 5 times, but the analyzer cannot deduce this so it assumes that it may be completely skipped, since it cannot reason about `size/2` even if it knows that size has a range of (10..100] which is [11..100] among integers.
This patch solves this problem by introducing support for symbols such as "symbol * integer" or "symbol / integer". In this patch only positive integers are supported. On the long-term our goal is to extend this support to more generic first-degree symbolic expressionsAdd support for multiplications and divisions of symbols when using comparison operators `>`, e.g.`>=`, "symbol * integer + another integer"`<` and `<=` in the range-based constraint manager.