search for: cousot

Hi all, I am currently working on a static analysis aimed at integer arithmetic overflow/underflow detection. We are attempting to build a sound abstract domain (based on Cousot & Cousot-style abstract interpretation), but practically speaking this really requires the ability to figure out the word size and signedness of values in the intermediate representation. I'm well aware that LLVM leverages the (usual) equivalence of certain arithmetic operations in...