Programs can be automatically analysed at various levels: some tools work directly with the source code, while others load a compiled, executable binary. However, both those approaches have substantial downsides. For complex languages (like C++ or Rust), working with source code is too difficult. Binary code, on the other hand, is often too hard to analyse because most of the high-level structure of the program has been erased at this point, and is tied to a particular CPU ISA. For this reason, many analysis tools opt to instead work with an intermediate representation -- the LLVM IR in the case of DIVINE. However, this means that the software to be analysed must be compiled to this intermediate representation, and this currently needs to be done by hand. The goal of this thesis is to design and implement an extension to the C and C++ compiler toolchain based on LLVM and CLang, which would store the bitcode along standard machine code. The extended compiler, linker and related tools should transparently work with existing build systems. The hybrid binaries produced this way should be directly executable, but it should also be possible to load them into the DIVINE model checker (and possibly other LLVM-based tools) for analysis.