[LLVMdev] annotations for optimization?

[Giacomo Tagliabue]

Hello everyone,
As a research project we are trying to figure out how to insert some
annotations in the compiler in order to optimize the code. For example:

/*@ ensures x == 5 */
if(x>5){
  {...}
}

where the comment is written in
ACSL<http://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language>.
The example is trivial, but gives the idea, if LLVM is be able to read the
annotation, it would optimize the code removing the if below.
The question is: does exist an annotation language to do that? if it
doesnt't exist, what should be modified in order to carry the information
of the annotations into LLVM? In other words, how can we let LLVM "know"
about these assertion?

Thank you
Giacomo Tagliabue
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20121113/b9e5e491/attachment.html>