seahorn/crab

Should we add the bitwise complement (~) operation in Crab?

Closed this issue · 2 comments

I noticed that this bitwise operation type is not included in Crab, and there is no need to add specialized abstraction design of this operation for each abstract domain in Crab. So, should we add the bitwise complement (~) operation in Crab? Or perhaps we have already implemented this operation in some other way, since -x = ~x +1 ?

CrabIR was defined from the beginning to be a good target for LLVM IR which doesn't have bitwise complement.
Note that in CrabIR you have the xor bitwise operator. So you can implement ~x = x xor all 1's so there is no need to have another abstract operation for the bitwise complement

Thanks for taking the time to reply!