-
Notifications
You must be signed in to change notification settings - Fork 33
Open
Labels
CrabIRRelated to CrabIRRelated to CrabIRdomainsRelated to abstract domainsRelated to abstract domainsenhancement
Description
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.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
CrabIRRelated to CrabIRRelated to CrabIRdomainsRelated to abstract domainsRelated to abstract domainsenhancement