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.
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.