search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Debug information when using LLVM IR as an input #790

Closed hernanponcedeleon closed 2 years ago

hernanponcedeleon commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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