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

[Alp Toker]

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.

Alp.


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

-- 
http://www.nuanti.com
the browser experts