search

seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
234 stars 32 forks source link

General question on "backward_assign_operations" #38

Closed aytey closed 4 years ago

aytey commented 4 years ago

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"
}
  1. Are there any domains which support wrapped bit vectors and "work backwards"?
caballa commented 4 years ago

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.