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

Alp Toker alp at nuanti.com
Sat Jun 7 14:58:44 PDT 2014

On 04/06/2014 03:16, Zvonimir Rakamaric wrote:
> 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.

Hi Zvonimir,

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:
> 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/
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits

the browser experts

More information about the cfe-commits mailing list