davidtr1037 / sa-utils Goto Github PK

The se-slicing project should be actually put inside KLEE where it belongs.

Currently, the mod/ref analysis is not considering the CFG.
It just computes the intersection of the mod-set of the skipped functions with the ref-set of the whole program.
For example:

void foo(p) {
  p->x = 100;
}

main() {
  if (p->x == 0) {
    ...
  }
  foo(p);
}

In this example, the load before the call to f will be considered as blocking.

This is especially relevant when we have more than one skipped function.