seahorn/crab

Improve precision and performance of backward operations

caballa opened this issue · 2 comments

caballa commented
Improve precision and performance of backward operations
caballa commented

Only apron and elina domains are reasonably precise.
For our own domains, we need to implement at least the case x := e where x appears in e.

caballa commented

In commit 1fe7b1b, the precision of invertible assignments is improved (all crab domains benefit from this).

In commit 4f29bae, backward array transfer functions are implemented for array_expansion domain.