-
|
How to save the metadata information in llvm ir during the transformation from llvm ir to boogie code? |
Beta Was this translation helpful? Give feedback.
Answered by
zvonimir
Mar 31, 2022
Replies: 1 comment
-
|
Thanks for your question. Could you please clarify what you mean by this and/or maybe give an example? In short, SMACK already uses certain kinds of LLVM IR metadata when generating Boogie code. For example, we use LLVM IT debug info to add debug (source code lines, variable names, etc.) info into the generated Boogie code. So we can certainly generate Boogie code based on the LLVM IR metadata. Is that your question? |
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
Luweicai
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Thanks for your question. Could you please clarify what you mean by this and/or maybe give an example?
In short, SMACK already uses certain kinds of LLVM IR metadata when generating Boogie code. For example, we use LLVM IT debug info to add debug (source code lines, variable names, etc.) info into the generated Boogie code. So we can certainly generate Boogie code based on the LLVM IR metadata.
Is that your question?