search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Rewrite memcpy of structures/arrays into load-then-store sequences #752

Closed shaobo-he closed 3 years ago

shaobo-he commented 3 years ago

Fixes #749

shaobo-he commented 3 years ago

Would it be possible to add a simple regression that checks that the pass indeed works?

Yes, it should be doable. In the meanwhile, I think this pass is worth of more discussion. So I converted it into a draft.