1- use cxx:: { CxxString , CxxVector } ;
2-
31#[ cxx:: bridge]
42pub mod cprover_api {
53
@@ -21,31 +19,31 @@ pub mod cprover_api {
2119 fn translate_vector_of_string ( elements : Vec < String > ) -> & ' static CxxVector < CxxString > ;
2220 fn get_messages ( ) -> & ' static CxxVector < CxxString > ;
2321 }
24-
25- extern "Rust" {
26- fn print_response ( vec : & CxxVector < CxxString > ) ;
27- fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > ;
28- }
2922}
3023
31- /// This is a utility function, whose job is to translate the responses from the C++
32- /// API ( which we get in the form of a C ++ std:: vector<std: string>) into a form that
33- /// can be easily consumed by other Rust programs.
34- pub fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > {
35- vec. iter ( )
36- . map ( |s| s. to_string_lossy ( ) . into_owned ( ) )
37- . collect ( )
38- }
24+ pub mod ffi_util {
25+ use cxx:: CxxString ;
26+ use cxx:: CxxVector ;
27+
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+ vec. iter ( )
33+ . map ( |s| s. to_string_lossy ( ) . into_owned ( ) )
34+ . collect ( )
35+ }
3936
40- /// This is a utility function, whose aim is to simplify direct printing of the messages
41- /// that we get from CBMC's C++ API. Underneath, it's using translate_response_buffer
42- /// to translate the C++ types into Rust types and then prints out the strings contained
43- /// in the resultant rust vector.
44- pub fn print_response ( vec : & CxxVector < CxxString > ) {
45- let vec: Vec < String > = translate_response_buffer ( vec) ;
37+ /// This is a utility function, whose aim is to simplify direct printing of the messages
38+ /// that we get from CBMC's C++ API. Underneath, it's using translate_response_buffer
39+ /// to translate the C++ types into Rust types and then prints out the strings contained
40+ /// in the resultant rust vector.
41+ pub fn print_response ( vec : & CxxVector < CxxString > ) {
42+ let vec: Vec < String > = translate_response_buffer ( vec) ;
4643
47- for s in vec {
48- println ! ( "{}" , s) ;
44+ for s in vec {
45+ println ! ( "{}" , s) ;
46+ }
4947 }
5048}
5149
@@ -105,7 +103,7 @@ mod tests {
105103 // else in case they want to inspect the output).
106104 let validation_msg = "Validating consistency of goto-model supplied to API session" ;
107105 let msgs = cprover_api:: get_messages ( ) ;
108- let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
106+ let msgs_assert = ffi_util :: translate_response_buffer ( msgs) . clone ( ) ;
109107
110108 assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
111109
@@ -139,7 +137,7 @@ mod tests {
139137 let verification_msg = "VERIFICATION FAILED" ;
140138
141139 let msgs = cprover_api:: get_messages ( ) ;
142- let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
140+ let msgs_assert = ffi_util :: translate_response_buffer ( msgs) . clone ( ) ;
143141
144142 assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
145143 }
@@ -172,7 +170,7 @@ mod tests {
172170 let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
173171
174172 let msgs = cprover_api:: get_messages ( ) ;
175- let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
173+ let msgs_assert = ffi_util :: translate_response_buffer ( msgs) . clone ( ) ;
176174
177175 assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
178176 assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg2) ) ) ;
0 commit comments