Hi. I understand from [1] (part 4.4) that instruction reordering is verified in vellvm. I download vellvm, but I dont know where instruction reordering has considered. And I would like to apply just that to my input. Can anyone help me? I am unfamiliar with coq and newbie in formal methods. [1] http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20141215/8172ed19/attachment.html>