@@ -15,20 +15,24 @@ pub mod cprover_api {
1515 fn validate_goto_model ( & self ) -> Result < ( ) > ;
1616 fn drop_unused_functions ( & self ) -> Result < ( ) > ;
1717
18- // Helper/Utility functions
19- fn translate_vector_of_string ( elements : Vec < String > ) -> & ' static CxxVector < CxxString > ;
18+ // WARNING: Please don't use this function - use its public interface in [ffi_util::translate_rust_vector_to_cpp].
19+ // The reason this is here is that it's implemented on the C++ shim, and to link this function against
20+ // its implementation it needs to be declared within the `unsafe extern "C++"` block of the FFI bridge.
21+ #[ doc( hidden) ]
22+ fn _translate_vector_of_string ( elements : Vec < String > ) -> & ' static CxxVector < CxxString > ;
2023 fn get_messages ( ) -> & ' static CxxVector < CxxString > ;
2124 }
2225}
2326
2427pub mod ffi_util {
28+ use crate :: cprover_api:: _translate_vector_of_string;
2529 use cxx:: CxxString ;
2630 use cxx:: CxxVector ;
2731
28- /// This is a utility function, whose job is to translate the responses from the C++
29- /// API (which we get in the form of a C++ std::vector<std:string>) into a form that
30- /// can be easily consumed by other Rust programs .
31- pub fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > {
32+ /// This function translates the responses from the C++ API (which we get in the
33+ /// form of a C++ std::vector<std:string>) into the equivalent Rust type `Vec<String>`.
34+ /// Dual to [translate_rust_vector_to_cpp] .
35+ pub fn translate_cpp_vector_to_rust ( vec : & CxxVector < CxxString > ) -> Vec < String > {
3236 vec. iter ( )
3337 . map ( |s| s. to_string_lossy ( ) . into_owned ( ) )
3438 . collect ( )
@@ -45,6 +49,12 @@ pub mod ffi_util {
4549 println ! ( "{}" , s) ;
4650 }
4751 }
52+
53+ /// Translate a Rust `Vec<String>` into a C++ acceptable `std::vector<std::string>`.
54+ /// Dual to [translate_cpp_vector_to_rust].
55+ pub fn translate_rust_vector_to_cpp ( elements : Vec < String > ) -> & ' static CxxVector < CxxString > {
56+ _translate_vector_of_string ( elements)
57+ }
4858}
4959
5060// To test run "CBMC_LIB_DIR=<path_to_build/libs> SAT_IMPL=minisat2 cargo test -- --test-threads=1 --nocapture"
@@ -67,7 +77,7 @@ mod tests {
6777 fn translate_vector_of_rust_string_to_cpp ( ) {
6878 let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) , "/tmp/example2.c" . to_owned( ) ] ;
6979
70- let vect = cprover_api :: translate_vector_of_string ( vec) ;
80+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
7181 assert_eq ! ( vect. len( ) , 2 ) ;
7282 }
7383
@@ -81,7 +91,7 @@ mod tests {
8191
8292 let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
8393
84- let vect = cprover_api :: translate_vector_of_string ( vec) ;
94+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
8595 assert_eq ! ( vect. len( ) , 1 ) ;
8696
8797 // Invoke load_model_from_files and see if the model
@@ -103,7 +113,7 @@ mod tests {
103113 // else in case they want to inspect the output).
104114 let validation_msg = "Validating consistency of goto-model supplied to API session" ;
105115 let msgs = cprover_api:: get_messages ( ) ;
106- let msgs_assert = ffi_util:: translate_response_buffer ( msgs) . clone ( ) ;
116+ let msgs_assert = ffi_util:: translate_cpp_vector_to_rust ( msgs) . clone ( ) ;
107117
108118 assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
109119
@@ -116,7 +126,7 @@ mod tests {
116126
117127 let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
118128
119- let vect = cprover_api :: translate_vector_of_string ( vec) ;
129+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
120130
121131 if let Err ( _) = client. load_model_from_files ( vect) {
122132 eprintln ! ( "Failed to load model from files: {:?}" , vect) ;
@@ -137,7 +147,7 @@ mod tests {
137147 let verification_msg = "VERIFICATION FAILED" ;
138148
139149 let msgs = cprover_api:: get_messages ( ) ;
140- let msgs_assert = ffi_util:: translate_response_buffer ( msgs) . clone ( ) ;
150+ let msgs_assert = ffi_util:: translate_cpp_vector_to_rust ( msgs) . clone ( ) ;
141151
142152 assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
143153 }
@@ -152,7 +162,7 @@ mod tests {
152162
153163 let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
154164
155- let vect = cprover_api :: translate_vector_of_string ( vec) ;
165+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
156166 assert_eq ! ( vect. len( ) , 1 ) ;
157167
158168 if let Err ( _) = client. load_model_from_files ( vect) {
@@ -170,7 +180,7 @@ mod tests {
170180 let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
171181
172182 let msgs = cprover_api:: get_messages ( ) ;
173- let msgs_assert = ffi_util:: translate_response_buffer ( msgs) . clone ( ) ;
183+ let msgs_assert = ffi_util:: translate_cpp_vector_to_rust ( msgs) . clone ( ) ;
174184
175185 assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
176186 assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg2) ) ) ;
0 commit comments