[PATCH] Adding SMACK software verifier specific target to clang that disallows type coercions
alp at nuanti.com
Sat Jun 7 14:58:44 PDT 2014
On 04/06/2014 03:16, Zvonimir Rakamaric wrote:
> 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
I don't have a strong idea of what the right fix should be, but adding
SMACK as an OS Triple doesn't feel right beyond a quick-fix.
You'll probably want to use your tool for analysing different frontend
architectures and the proposed approach would make it difficult to
specify a suitable backend target in an ordinary build system. It also
relies on what's so far been a changeable implementation detail.
Reid's line of questioning was going well and if we follow to its
conclusion it seems we'll achieve a more sustainable solution to your
problem. Someone on the LLVM side should download your tool and get a
feel for the requirements -- I'll try to find time for that.
This isn't to hold up the idea, rather to make sure we specify it
correctly because it's in fact a really important use case that we
should support explicitly in LLVM without tying it to a single tool.
> 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
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
the browser experts
More information about the cfe-commits