@@ -23,14 +23,25 @@ pub mod ffi {
2323
2424 extern "Rust" {
2525 fn print_response ( vec : & CxxVector < CxxString > ) ;
26+ fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > ;
2627 }
2728}
2829
29- fn print_response ( vec : & CxxVector < CxxString > ) {
30- let vec: Vec < String > = vec
31- . iter ( )
30+ /// This is a utility function, whose job is to translate the responses from the C++
31+ /// API ( which we get in the form of a C ++ std:: vector<std: string>) into a form that
32+ /// can be easily consumed by other Rust programs.
33+ pub fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > {
34+ vec. iter ( )
3235 . map ( |s| s. to_string_lossy ( ) . into_owned ( ) )
33- . collect ( ) ;
36+ . collect ( )
37+ }
38+
39+ /// This is a utility function, whose aim is to simplify direct printing of the messages
40+ /// that we get from CBMC's C++ API. Underneath, it's using translate_response_buffer
41+ /// to translate the C++ types into Rust types and then prints out the strings contained
42+ /// in the resultant rust vector.
43+ pub fn print_response ( vec : & CxxVector < CxxString > ) {
44+ let vec: Vec < String > = translate_response_buffer ( vec) ;
3445
3546 for s in vec {
3647 println ! ( "{}" , s) ;
@@ -82,10 +93,22 @@ mod tests {
8293 }
8394
8495 // Validate integrity of passed goto-model.
85- client. validate_goto_model ( ) ;
96+ if let Err ( _) = client. validate_goto_model ( ) {
97+ eprintln ! ( "Failed to validate goto model from files: {:?}" , vect) ;
98+ process:: exit ( 1 ) ;
99+ }
86100
101+ // ATTENTION: The following `.clone()` is unneeded - I keep it here in order to
102+ // make potential printing of the message buffer easier (because of borrowing).
103+ // This is also why a print instruction is commented out (as a guide for someone
104+ // else in case they want to inspect the output).
105+ let validation_msg = "Validating consistency of goto-model supplied to API session" ;
87106 let msgs = ffi:: get_messages ( ) ;
88- print_response ( msgs) ;
107+ let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
108+
109+ assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
110+
111+ // print_response(msgs);
89112 }
90113
91114 #[ test]
@@ -102,15 +125,22 @@ mod tests {
102125 }
103126
104127 // Validate integrity of goto-model
105- client. validate_goto_model ( ) ;
128+ if let Err ( _) = client. validate_goto_model ( ) {
129+ eprintln ! ( "Failed to validate goto model from files: {:?}" , vect) ;
130+ process:: exit ( 1 ) ;
131+ }
106132
107133 if let Err ( _) = client. verify_model ( ) {
108134 eprintln ! ( "Failed to verify model from files: {:?}" , vect) ;
109135 process:: exit ( 1 ) ;
110136 }
111137
138+ let verification_msg = "VERIFICATION FAILED" ;
139+
112140 let msgs = ffi:: get_messages ( ) ;
113- print_response ( msgs) ;
141+ let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
142+
143+ assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
114144 }
115145
116146 #[ test]
@@ -130,14 +160,20 @@ mod tests {
130160 eprintln ! ( "Failed to load model from files: {:?}" , vect) ;
131161 process:: exit ( 1 ) ;
132162 }
163+
133164 // Perform a drop of any unused functions.
134165 if let Err ( err) = client. drop_unused_functions ( ) {
135166 eprintln ! ( "Error during client call: {:?}" , err) ;
136167 process:: exit ( 1 ) ;
137168 }
138169
139- println ! ( "Just before we print the messages" ) ;
170+ let instrumentation_msg = "Performing instrumentation pass: dropping unused functions" ;
171+ let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
172+
140173 let msgs = ffi:: get_messages ( ) ;
141- print_response ( msgs) ;
174+ let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
175+
176+ assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
177+ assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg2) ) ) ;
142178 }
143179}
0 commit comments