smackers / smack

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

Externalize entry points that are marked internal #753

Closed keram88 closed 3 years ago

keram88 commented 3 years ago

This adds a utility extern-statics that transforms input LLVM files to have functions which are entry-points to always be externally linkable. SMACK's front-end is changed to process input bit-codes before running llvm-link on them in order to keep these functions from being erased during linking.

The usage of extern-statics is: