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)?

[shaobo-he]

Sorry for the late reply. Yes, you would probably need something like -g when compiling the bytecode to enable debug information. If the debug information does not show up in the Boogie code, it's probably because the bytecode you fed to SMACK doesn't have it.

[hernanponcedeleon]

Using -g alone is not enough. However using both -g -gcolumn-info works.