seahorn/crab

Create tree expressions and adapt abstract domains to use them

caballa opened this issue · 0 comments

Abstract domains only support arithmetic operations in three-address form (e.g., +,-,*,/) and addition of linear constraints.

Abstract domains do not support addition of non-linear constraints. Moreover, linear constraints are simplified on-the-fly to keep a normalized form. This does not work well if linear constraints are defined over machine arithmetic because those simplifications are not sound. To address these issues, we should have tree expressions (similar to those defined by Apron) which can be converted to linear constraints (if possible/wanted) by each abstract domain.