@@ -15,20 +15,24 @@ pub mod cprover_api {
15
15
fn validate_goto_model ( & self ) -> Result < ( ) > ;
16
16
fn drop_unused_functions ( & self ) -> Result < ( ) > ;
17
17
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 > ;
20
23
fn get_messages ( ) -> & ' static CxxVector < CxxString > ;
21
24
}
22
25
}
23
26
24
27
pub mod ffi_util {
28
+ use crate :: cprover_api:: _translate_vector_of_string;
25
29
use cxx:: CxxString ;
26
30
use cxx:: CxxVector ;
27
31
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 > {
32
36
vec. iter ( )
33
37
. map ( |s| s. to_string_lossy ( ) . into_owned ( ) )
34
38
. collect ( )
@@ -45,6 +49,12 @@ pub mod ffi_util {
45
49
println ! ( "{}" , s) ;
46
50
}
47
51
}
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
+ }
48
58
}
49
59
50
60
// 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 {
67
77
fn translate_vector_of_rust_string_to_cpp ( ) {
68
78
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) , "/tmp/example2.c" . to_owned( ) ] ;
69
79
70
- let vect = cprover_api :: translate_vector_of_string ( vec) ;
80
+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
71
81
assert_eq ! ( vect. len( ) , 2 ) ;
72
82
}
73
83
@@ -81,7 +91,7 @@ mod tests {
81
91
82
92
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
83
93
84
- let vect = cprover_api :: translate_vector_of_string ( vec) ;
94
+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
85
95
assert_eq ! ( vect. len( ) , 1 ) ;
86
96
87
97
// Invoke load_model_from_files and see if the model
@@ -103,7 +113,7 @@ mod tests {
103
113
// else in case they want to inspect the output).
104
114
let validation_msg = "Validating consistency of goto-model supplied to API session" ;
105
115
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 ( ) ;
107
117
108
118
assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
109
119
@@ -116,7 +126,7 @@ mod tests {
116
126
117
127
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
118
128
119
- let vect = cprover_api :: translate_vector_of_string ( vec) ;
129
+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
120
130
121
131
if let Err ( _) = client. load_model_from_files ( vect) {
122
132
eprintln ! ( "Failed to load model from files: {:?}" , vect) ;
@@ -137,7 +147,7 @@ mod tests {
137
147
let verification_msg = "VERIFICATION FAILED" ;
138
148
139
149
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 ( ) ;
141
151
142
152
assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
143
153
}
@@ -152,7 +162,7 @@ mod tests {
152
162
153
163
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
154
164
155
- let vect = cprover_api :: translate_vector_of_string ( vec) ;
165
+ let vect = ffi_util :: translate_rust_vector_to_cpp ( vec) ;
156
166
assert_eq ! ( vect. len( ) , 1 ) ;
157
167
158
168
if let Err ( _) = client. load_model_from_files ( vect) {
@@ -170,7 +180,7 @@ mod tests {
170
180
let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
171
181
172
182
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 ( ) ;
174
184
175
185
assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
176
186
assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg2) ) ) ;
0 commit comments