|
| 1 | +# CProver (CBMC) Rust API |
| 2 | + |
| 3 | +This folder contains the implementation of the Rust API of the CProver (CBMC) project. |
| 4 | + |
| 5 | +## Building instructions |
| 6 | + |
| 7 | +There are two ways to build the project: |
| 8 | + |
| 9 | +1. As part of the CBMC project (using `cmake`) by building CBMC with the flag |
| 10 | + `-DWITH_RUST_API=ON`. The outcome of this process is a compilation artefact |
| 11 | + `libcprover-x.y.z.a` under the `<build>/lib` directory. |
| 12 | +2. By executing `cargo build` under this (`src/libcprover-rust`) directory. |
| 13 | + |
| 14 | + For this to work, you need to supply two environment variables to the |
| 15 | + project: |
| 16 | + |
| 17 | + * `CBMC_LIB_DIR`, for selecting where the `libcprover-x.y.z.a` is located |
| 18 | + (say, if you have downloaded a pre-packaged release which contains |
| 19 | + the static library), and |
| 20 | + * `CBMC_VERSION`, for selecting the version of the library to link against |
| 21 | + (this is useful if you have multiple versions of the library in the same |
| 22 | + location and you want to control which version you compile against). |
| 23 | + |
| 24 | +As an example, a command sequence to build the API through `cargo` would look |
| 25 | +like this (assuming you're executing these instructions from the root level |
| 26 | +directory of the CBMC project.) |
| 27 | + |
| 28 | +```sh |
| 29 | +$ cd src/libcprover-rust |
| 30 | +$ cargo clean |
| 31 | +$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build |
| 32 | +``` |
| 33 | + |
| 34 | +To build the project and run its associated tests, the command sequence would |
| 35 | +look like this: |
| 36 | + |
| 37 | +```sh |
| 38 | +$ cd src/libcprover-rust |
| 39 | +$ cargo clean |
| 40 | +$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture |
| 41 | +``` |
| 42 | + |
| 43 | +## Notes |
| 44 | + |
| 45 | +* The functions supported by the Rust API are catalogued within the `ffi` module within |
| 46 | + `lib.rs`. |
| 47 | +* The API supports exception handling from inside CBMC by catching the exceptions in |
| 48 | + a C++ shim, and then translating the exception into the Rust `Result` type. |
| 49 | +* Because of limitations from the C++ side of CBMC, the API is not thread-safe. |
0 commit comments