Symbolic index fix

[domainexpert]

Fixes crashes due to symbolic index. This is done by assuming that retrieved error for symbolic indices is 0, as it can be assumed that the value is non-approximable in that case.

Secondly, this also fixes crashes due to mismatched type returned by ErrorState::propagateError(), which sometimes returns Boolean expression, from the construction of path condition constraint with error, when the expected return type is 8-bits. The path condition constraint with error is now separated from the actual error value (which is 0 in case of conditional). ErrorState::propagateError() has been made to return a pair of them.

Tested on get_sign.c, same output before and after this patch:

#include <klee/klee.h>

int calculate_output(int x, int y)
{
    int z;

    if (x < 5) {
        z = x + y;
    } else {
        z = x * y;
    }
    return z;
}

int main()
{
    int output;
    int input_x, input_y;

    klee_make_symbolic(&input_x, sizeof(input_x), "input_x");
    klee_make_symbolic(&input_y, sizeof(input_y), "input_y");

    klee_track_error(&input_x, "input_x_error");
    klee_track_error(&input_y, "input_y_error");

    output = calculate_output(input_x, input_y);

    klee_bound_error(output, "output", 1.3);

    return 0;
}

[Himeshi]

Brilliant idea! Thanks @domainexpert!