seahorn / sea-dsa

A new context, field, and array-sensitive heap analysis for LLVM bitcode based on DSA.
Other
157 stars 29 forks source link

Fix issue129 #130

Closed pietroborrello closed 3 years ago

pietroborrello commented 3 years ago

Fix for issue #129 Added a check on srcTy->isSized() so that transfersNoPointers returns false in case of opaque structs as well, without crashing. Not sure if the warning should be emitted, or the check should be in a separate condition, just before.

agurfinkel commented 3 years ago

It will take me some time to review. The fix for crash is good, but the warning seems misplaced.

pietroborrello commented 3 years ago

Yes, the warning wasn't a good fit,I moved the check outside, and no warnings emitted, is it better?

agurfinkel commented 3 years ago

thank you!