1
1
use cxx:: { CxxString , CxxVector } ;
2
2
3
3
#[ cxx:: bridge]
4
- pub mod ffi {
4
+ pub mod cprover_api {
5
5
6
6
unsafe extern "C++" {
7
7
include ! ( "libcprover-cpp/api.h" ) ;
@@ -58,7 +58,7 @@ mod tests {
58
58
59
59
#[ test]
60
60
fn it_works ( ) {
61
- let client = ffi :: new_api_session ( ) ;
61
+ let client = cprover_api :: new_api_session ( ) ;
62
62
let result = client. get_api_version ( ) ;
63
63
64
64
let_cxx_string ! ( expected_version = "0.1" ) ;
@@ -69,21 +69,21 @@ mod tests {
69
69
fn translate_vector_of_rust_string_to_cpp ( ) {
70
70
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) , "/tmp/example2.c" . to_owned( ) ] ;
71
71
72
- let vect = ffi :: translate_vector_of_string ( vec) ;
72
+ let vect = cprover_api :: translate_vector_of_string ( vec) ;
73
73
assert_eq ! ( vect. len( ) , 2 ) ;
74
74
}
75
75
76
76
#[ test]
77
77
fn it_can_load_model_from_file ( ) {
78
- let binding = ffi :: new_api_session ( ) ;
78
+ let binding = cprover_api :: new_api_session ( ) ;
79
79
let client = match binding. as_ref ( ) {
80
80
Some ( api_ref) => api_ref,
81
81
None => panic ! ( "Failed to acquire API session handle" ) ,
82
82
} ;
83
83
84
84
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
85
85
86
- let vect = ffi :: translate_vector_of_string ( vec) ;
86
+ let vect = cprover_api :: translate_vector_of_string ( vec) ;
87
87
assert_eq ! ( vect. len( ) , 1 ) ;
88
88
89
89
// Invoke load_model_from_files and see if the model
@@ -104,7 +104,7 @@ mod tests {
104
104
// This is also why a print instruction is commented out (as a guide for someone
105
105
// else in case they want to inspect the output).
106
106
let validation_msg = "Validating consistency of goto-model supplied to API session" ;
107
- let msgs = ffi :: get_messages ( ) ;
107
+ let msgs = cprover_api :: get_messages ( ) ;
108
108
let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
109
109
110
110
assert ! ( msgs_assert. contains( & String :: from( validation_msg) ) ) ;
@@ -114,11 +114,11 @@ mod tests {
114
114
115
115
#[ test]
116
116
fn it_can_verify_the_loaded_model ( ) {
117
- let client = ffi :: new_api_session ( ) ;
117
+ let client = cprover_api :: new_api_session ( ) ;
118
118
119
119
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
120
120
121
- let vect = ffi :: translate_vector_of_string ( vec) ;
121
+ let vect = cprover_api :: translate_vector_of_string ( vec) ;
122
122
123
123
if let Err ( _) = client. load_model_from_files ( vect) {
124
124
eprintln ! ( "Failed to load model from files: {:?}" , vect) ;
@@ -138,23 +138,23 @@ mod tests {
138
138
139
139
let verification_msg = "VERIFICATION FAILED" ;
140
140
141
- let msgs = ffi :: get_messages ( ) ;
141
+ let msgs = cprover_api :: get_messages ( ) ;
142
142
let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
143
143
144
144
assert ! ( msgs_assert. contains( & String :: from( verification_msg) ) ) ;
145
145
}
146
146
147
147
#[ test]
148
148
fn it_can_drop_unused_functions_from_model ( ) {
149
- let binding = ffi :: new_api_session ( ) ;
149
+ let binding = cprover_api :: new_api_session ( ) ;
150
150
let client = match binding. as_ref ( ) {
151
151
Some ( api_ref) => api_ref,
152
152
None => panic ! ( "Failed to acquire API session handle" ) ,
153
153
} ;
154
154
155
155
let vec: Vec < String > = vec ! [ "other/example.c" . to_owned( ) ] ;
156
156
157
- let vect = ffi :: translate_vector_of_string ( vec) ;
157
+ let vect = cprover_api :: translate_vector_of_string ( vec) ;
158
158
assert_eq ! ( vect. len( ) , 1 ) ;
159
159
160
160
if let Err ( _) = client. load_model_from_files ( vect) {
@@ -171,7 +171,7 @@ mod tests {
171
171
let instrumentation_msg = "Performing instrumentation pass: dropping unused functions" ;
172
172
let instrumentation_msg2 = "Dropping 8 of 11 functions (3 used)" ;
173
173
174
- let msgs = ffi :: get_messages ( ) ;
174
+ let msgs = cprover_api :: get_messages ( ) ;
175
175
let msgs_assert = translate_response_buffer ( msgs) . clone ( ) ;
176
176
177
177
assert ! ( msgs_assert. contains( & String :: from( instrumentation_msg) ) ) ;
0 commit comments