[PATCH] Adding SMACK software verifier specific target to clang that disallows type coercions

Zvonimir Rakamaric zvonimir at cs.utah.edu
Tue Jun 3 17:16:23 PDT 2014


So I created two tiny patches (see attached) for LLVM and clang that
allow target triples of the form e.g. x86_64-unknown-smack to be used,
which in turn disables various type coercions. Basically, SMACK
software verifier that I've been working on is not happy when it
encounters type coercions, which are not easy to handle in their full

Please take a look at the following discussions for background
information on why I created these patches:

I tested the patches on both LLVM and clang regressions suites, and
they seem to be working fine.

Please let me know how to proceed with this.


-- Zvonimir

-------------- next part --------------
A non-text attachment was scrubbed...
Name: clang-smack.patch
Type: text/x-patch
Size: 1184 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140603/21bb851e/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: llvm-smack.patch
Type: text/x-patch
Size: 1097 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140603/21bb851e/attachment-0001.bin>

More information about the cfe-commits mailing list