LL2GB

LL2GB is a translator from LLVM IR to CProver/CBMC's GOTO IR.

Build Steps:

    $ mkdir build
    $ cd build
    $ cmake -DCBMC_DIR=<cbmc_path> -DLLVM_CONFIG=<llvm-config> ../
    $ make
    $ ./ll2gb --help

Dependencies:

LLVM 14.x (or above)
CBMC 5.54 (or above)

Check

    $ cd regression/c_regression
    $ make test

Acknowledgement

An earlier version of the tool can be found in the old branch. We thank Rasika Sapate for her contributions in developing this earlier version. We also thank Dr Saurabh Joshi for their valuable insignts and guidance in developing this tool.

License

MIT License, see LICENSE file.