1
- use cxx:: { CxxString , CxxVector } ;
2
-
3
1
#[ cxx:: bridge]
4
2
pub mod cprover_api {
5
3
@@ -21,31 +19,31 @@ pub mod cprover_api {
21
19
fn translate_vector_of_string ( elements : Vec < String > ) -> & ' static CxxVector < CxxString > ;
22
20
fn get_messages ( ) -> & ' static CxxVector < CxxString > ;
23
21
}
24
-
25
- extern "Rust" {
26
- fn print_response ( vec : & CxxVector < CxxString > ) ;
27
- fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > ;
28
- }
29
22
}
30
23
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
+ }
39
36
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) ;
46
43
47
- for s in vec {
48
- println ! ( "{}" , s) ;
44
+ for s in vec {
45
+ println ! ( "{}" , s) ;
46
+ }
49
47
}
50
48
}
51
49
@@ -105,7 +103,7 @@ mod tests {
105
103
// else in case they want to inspect the output).
106
104
let validation_msg = "Validating consistency of goto-model supplied to API session" ;
107
105
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 ( ) ;
109
107
110
108
assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
111
109
@@ -139,7 +137,7 @@ mod tests {
139
137
let verification_msg = "VERIFICATION FAILED" ;
140
138
141
139
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 ( ) ;
143
141
144
142
assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
145
143
}
@@ -172,7 +170,7 @@ mod tests {
172
170
let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
173
171
174
172
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 ( ) ;
176
174
177
175
assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
178
176
assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg2) ) ) ;
0 commit comments