Maintain symbolic expressions containing error for path conditions

[Himeshi]

New pull request for issue #47

[domainexpert]

@Himeshi I tried the following example that you sent before:

#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;
}

But I did not see the difference in the output error expression from before.

[Himeshi]

Sorry I forgot to mention that this should be run with --write-kqueries option. In that case the .kquery file will contain the path condition with error.

I moved the path condition with error expression to the .kquery file since that's where the path conditions are written.