Low-Hanging Fruits in SV-COMP No-Overflow: CWE190-*-square*.i

[michael-schwarz]

I compared our results with Mopsa and noticed that there is >100 simple CWE tasks where we fail to show that no overflow can occur, even though the code looks simple enough:
https://sv-comp.sosy-lab.org/2023/results/results-verified/META_NoOverflows.table.html#/table?filter=9(0*status*(category(in(unknown,error)))),13(0*status*(category(in(correct))))

The core boils down to the following check, which is a bit nasty as it requires relationality through a call of a library function abs (similar to what was done in #1041), and us implementing some sort of constant folding for functions like sqrt. However, this should definitely be within reach.

int data;
if (data > (-0x7fffffff - 1) && abs(data) < (long)sqrt((double)0x7fffffff))
{
    int result = data * data;
    printIntLine(result);
}

Maybe @stilscher this is something for you? It would be a good way to get comfortable with implementing analyses and should be doable in an afternoon or a rainy weekend.