Debug information when using LLVM IR as an input

[hernanponcedeleon]

When using smack to convert C code to boogie (smack -t ...), the generated boogie codecontains "debug information" such as from which file and line in the code an instructions comes from. I have been using this for a few years and works quite well.

Now I am trying to feed smack directly with llvm bytecode. While the transformation seems to work as expected. The problem is that it does not generate any debug information. Is there any way smack can generate such information when giving llvm bytecode as an input (probably already in the command I am using to generate the bytecode, something like using -g in clang)?