Using LLBMC for non functional property verification

[bishoksan kafle]

Hi,
   Verification of non functional properties like time and energy is getting more importance in the recent days. The energy models of programs can be precisely known in low level language. So we need some model checkers which work in low level to verify energy related properties like energy budgets. In my opinion, LLBMC stands in the right place for this. But here is a small gap. We need to somehow annotate LLVM IR, bitcode used by LLBMC with energy models. I think LLVM IR can be annotated, but no idea about LLVM IR, bitcode. Can you suggest me how this bit code can be annotated? or not possible? I would be grateful to hear from you.
Many thanks in advance!!
Bishoksan