@@ -23,14 +23,25 @@ pub mod ffi {
23
23
24
24
extern "Rust" {
25
25
fn print_response ( vec : & CxxVector < CxxString > ) ;
26
+ fn translate_response_buffer ( vec : & CxxVector < CxxString > ) -> Vec < String > ;
26
27
}
27
28
}
28
29
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 ( )
32
35
. 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) ;
34
45
35
46
for s in vec {
36
47
println ! ( "{}" , s) ;
@@ -82,10 +93,22 @@ mod tests {
82
93
}
83
94
84
95
// 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
+ }
86
100
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" ;
87
106
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);
89
112
}
90
113
91
114
#[ test]
@@ -102,15 +125,22 @@ mod tests {
102
125
}
103
126
104
127
// 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
+ }
106
132
107
133
if let Err ( _) = client. verify_model ( ) {
108
134
eprintln ! ( "Failed to verify model from files: {:?}" , vect) ;
109
135
process:: exit ( 1 ) ;
110
136
}
111
137
138
+ let verification_msg = "VERIFICATION FAILED" ;
139
+
112
140
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) ) ) ;
114
144
}
115
145
116
146
#[ test]
@@ -130,14 +160,20 @@ mod tests {
130
160
eprintln ! ( "Failed to load model from files: {:?}" , vect) ;
131
161
process:: exit ( 1 ) ;
132
162
}
163
+
133
164
// Perform a drop of any unused functions.
134
165
if let Err ( err) = client. drop_unused_functions ( ) {
135
166
eprintln ! ( "Error during client call: {:?}" , err) ;
136
167
process:: exit ( 1 ) ;
137
168
}
138
169
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
+
140
173
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) ) ) ;
142
178
}
143
179
}
0 commit comments