[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


Hi,

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
generality.

Please take a look at the following discussions for background
information on why I created these patches:
http://lists.cs.uiuc.edu/pipermail/llvmdev/2014-May/072986.html
http://lists.cs.uiuc.edu/pipermail/cfe-dev/2014-May/037120.html

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.

Thanks!

Best,
-- Zvonimir

--
http://zvonimir.info
http://soarlab.org/
-------------- 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