Skip to content

Commit 761d62e

Browse files
committed
Add a unit test for catching exceptions from C++ and returning Rust Result types.
1 parent b34e991 commit 761d62e

File tree

1 file changed

+17
-1
lines changed

1 file changed

+17
-1
lines changed

src/libcprover-rust/src/lib.rs

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
pub mod cprover_api {
77

88
unsafe extern "C++" {
9-
include!("libcprover-cpp/api.h");
9+
include!("cprover/api.h");
1010
include!("include/c_api.h");
1111

1212
/// Central organisational handle of the API. This directly corresponds to the
@@ -101,6 +101,22 @@ mod tests {
101101
assert_eq!(vect.len(), 2);
102102
}
103103

104+
// This test will capture a `system_exceptiont` from CBMC's end at the C++ shim that this
105+
// library depends on, and it will be correctly translated into the Result type for Rust.
106+
// This also validates that our type definition include of the base class for the exceptions
107+
// works as we expect it to.
108+
#[test]
109+
fn it_translates_exceptions_to_errors() {
110+
let client = cprover_api::new_api_session();
111+
112+
// The vector of string is supposed to contain a string denoting
113+
// a filepath that is erroneous.
114+
let vec: Vec<String> = vec!["/fkjsdlkjfisudifoj2309".to_owned()];
115+
let vect = ffi_util::translate_rust_vector_to_cpp(vec);
116+
117+
assert!(client.load_model_from_files(vect).is_err());
118+
}
119+
104120
#[test]
105121
fn it_can_load_model_from_file() {
106122
let binding = cprover_api::new_api_session();

0 commit comments

Comments
 (0)