Hello everyone,<br>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:<br><br><font face="courier new, monospace">/*@ ensures x == 5 */</font><div>
<font face="courier new, monospace">if(x>5){</font></div><div><font face="courier new, monospace">  {...}<br>}</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="arial, helvetica, sans-serif">where the comment is written in <a href="http://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language">ACSL</a>. 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.<br>
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?<br>
<br>Thank you<br>Giacomo Tagliabue</font></div>