To model 'abs' and 'labs' functions in klee-libc and suggest to KLEE mainline

[operasfantom]

This is a follow-up of that thread.

Currently, 'abs' and 'labs' function calls lead to concretization. Therefore important paths remain uncovered, as in the following example:

Code

int foo(int x) 
{
  int y = abs(x);
  if (y == 1234) {
    return -1;
  }
  return +1;
}

Generated tests

TEST(regression, foo_test_1)
{
    int actual = foo(0);
    EXPECT_EQ(1, actual);
}

[ladisgin]

Moved to UnitTestBot/klee#66