search

seahorn / crab

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

Improve precision and performance of backward operations #15

Open caballa opened 7 years ago

caballa commented 5 years ago

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 5 years ago

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

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