General question on "backward_assign_operations"

[aytey]

Two questions:

1. Is it possible to use crab's "backwards assignment"s to calculate inputs at the "beginning" of a program? For example:

void foo(int y)
{
    y++;
    if (y > 10); // <-- if this was SSA, it would be something like "y__0 > 9"
}

2. Are there any domains which support wrapped bit vectors and "work backwards"?

[caballa]

For your first point, the answer is yes. Crab is able to produce necessary preconditions. Having said that, that part of Crab needs to be improved a lot and the code is probably rusty since AFIK, nobody really uses it.

For your second point, there is no support for wrapped intervals. In terms of backward transfer functions most of the support is for arithmetic operations that are invertible (basically, linear assignments). Wrapped intervals are tricky because of the wraparound issue.