Skip to content

Commit 850e941

Browse files
committed
Add environment variable for include folder in build and update build docs
1 parent ac02ab8 commit 850e941

File tree

2 files changed

+37
-8
lines changed

2 files changed

+37
-8
lines changed

src/libcprover-rust/build.rs

+32-5
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
use std::env;
22
use std::env::VarError;
33
use std::io::{Error, ErrorKind};
4-
use std::path::Path;
54
use std::path::PathBuf;
65

76
fn get_current_working_dir() -> std::io::Result<PathBuf> {
@@ -37,12 +36,40 @@ fn get_library_build_dir() -> std::io::Result<PathBuf> {
3736
))
3837
}
3938

39+
// This is needed so that cargo can find the include folder for the C++
40+
// API headers at compile time.
41+
fn get_include_directory_envvar() -> Result<String, VarError> {
42+
env::var("CBMC_INCLUDE_DIR")
43+
}
44+
45+
fn get_include_directory() -> std::io::Result<PathBuf> {
46+
let env_var_fetch_result = get_include_directory_envvar();
47+
if let Ok(build_dir) = env_var_fetch_result {
48+
let mut path = PathBuf::new();
49+
path.push(build_dir);
50+
return Ok(path);
51+
}
52+
Err(Error::new(
53+
ErrorKind::Other,
54+
"Environment variable `CBMC_INCLUDE_DIR' not set",
55+
))
56+
}
57+
4058
fn main() {
41-
let cbmc_source_path = Path::new("..");
42-
let cpp_api_path = Path::new("../libcprover-cpp/");
59+
let cpp_api_include_path = match get_include_directory() {
60+
Ok(path) => path,
61+
Err(err) => {
62+
let error_message = &format!(
63+
"Error: {}.\n Advice: {}.",
64+
err,
65+
"Please set the environment variable `CBMC_INCLUDE_DIR' with the path that contains cprover/api.h on your system"
66+
);
67+
panic!("{}", error_message);
68+
}
69+
};
70+
4371
let _build = cxx_build::bridge("src/lib.rs")
44-
.include(cbmc_source_path)
45-
.include(cpp_api_path)
72+
.include(cpp_api_include_path)
4673
.include(get_current_working_dir().unwrap())
4774
.file("src/c_api.cc")
4875
.flag_if_supported("-std=c++11")

src/libcprover-rust/readme.md

+5-3
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,9 @@ project:
1515

1616
* `CBMC_LIB_DIR`, for selecting where the `libcprover-x.y.z.a` is located
1717
(say, if you have downloaded a pre-packaged release which contains
18-
the static library), and
18+
the static library),
19+
* `CBMC_INCLUDE_DIR`, for selecting where the `cprover/api.h` is located,
20+
and
1921
* `CBMC_VERSION`, for selecting the version of the library to link against
2022
(this is useful if you have multiple versions of the library in the same
2123
location and you want to control which version you compile against).
@@ -27,7 +29,7 @@ directory of the CBMC project.)
2729
```sh
2830
$ cd src/libcprover-rust
2931
$ cargo clean
30-
$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
32+
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo build
3133
```
3234

3335
To build the project and run its associated tests, the command sequence would
@@ -36,7 +38,7 @@ look like this:
3638
```sh
3739
$ cd src/libcprover-rust
3840
$ cargo clean
39-
$ CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
41+
$ CBMC_INCLUDE_DIR=../../build/include CBMC_LIB_DIR=../../build/lib CBMC_VERSION=5.78.0 cargo test -- --test-threads=1 --nocapture
4042
```
4143

4244
## Notes

0 commit comments

Comments
 (0)