seahorn / crab

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

feat(domain): add missing parameterized constructor #55

Closed LinerSu closed 1 year ago

LinerSu commented 1 year ago

One parameterized constructor for the product domain needs to be included, which should take a constant reference for each subdomain.

caballa commented 1 year ago

I like to have in this case only the move constructor. Any reason for this? You can make a copy and move the abstract states which is what your constructor will do

LinerSu commented 1 year ago

I sometimes need to construct a new product domain object by taking a subdomain which is a constant reference. For example,

const product_domain_t *prod_ref = ...;
const Domain1 &dom_val1 = prod_ref->fist();
Domain2 dom_val2 = prod_ref->second();
...
product_domain_t output(dom_val1, dom_val2);

But I agree with your solution, copy and move is an alternative solution.