Export goto-lib instrument passes to Rust API and use them in test

Author: NlightNFotis

src/libcprover-cpp/api.cpp

@@ -166,7 +166,7 @@ void api_sessiont::verify_model() const
   verifier.report();
 }
 
-void api_sessiont::drop_unused_functions()
+void api_sessiont::drop_unused_functions() const
 {
   INVARIANT(
     implementation->model != nullptr,
@@ -181,7 +181,7 @@ void api_sessiont::drop_unused_functions()
     *implementation->model, *implementation->message_handler);
 }
 
-void api_sessiont::validate_goto_model()
+void api_sessiont::validate_goto_model() const
 {
   INVARIANT(
     implementation->model != nullptr,

src/libcprover-cpp/api.h

@@ -72,10 +72,10 @@ struct api_sessiont
   void verify_model() const;
 
   /// Drop unused functions from the loaded goto_model simplifying it
-  void drop_unused_functions();
+  void drop_unused_functions() const;
 
   /// Validate the loaded goto model
-  void validate_goto_model();
+  void validate_goto_model() const;
 
   // A simple API version information function.
   std::unique_ptr<std::string> get_api_version() const;

src/libcprover-rust/src/lib.rs

@@ -13,6 +13,8 @@ pub mod ffi {
         fn get_api_version(&self) -> UniquePtr<CxxString>;
         fn load_model_from_files(&self, files: &CxxVector<CxxString>);
         fn verify_model(&self);
+        fn validate_goto_model(&self);
+        fn drop_unused_functions(&self);
 
         // Helper/Utility functions
         fn translate_vector_of_string(elements: Vec<String>) -> &'static CxxVector<CxxString>;
@@ -35,7 +37,7 @@ fn print_response(vec: &CxxVector<CxxString>) {
     }
 }
 
-// To test run "cargo test -- --nocapture"
+// To test run "CBMC_LIB_DIR=<path_to_build/libs> cargo test -- --test-threads=1 --nocapture"
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -51,7 +53,7 @@ mod tests {
     }
 
     #[test]
-    fn translate_vector_of_rust_string_to_CPP() {
+    fn translate_vector_of_rust_string_to_cpp() {
         let vec: Vec<String> = vec![
             "/tmp/example.c".to_owned(),
             "/tmp/example2.c".to_owned()];
@@ -77,6 +79,11 @@ mod tests {
         // Invoke load_model_from_files and see if the model
         // has been loaded.
         client.load_model_from_files(vect);
+        // Validate integrity of passed goto-model.
+        client.validate_goto_model();
+
+        let msgs = ffi::get_messages();
+        print_response(msgs);
     }
 
     #[test]
@@ -89,9 +96,34 @@ mod tests {
         let vect = ffi::translate_vector_of_string(vec);
         client.load_model_from_files(vect);
 
+        // Validate integrity of goto-model
+        client.validate_goto_model();
+
         client.verify_model();
 
         let msgs = ffi::get_messages();
         print_response(msgs);
     }
+
+    #[test]
+    fn it_can_drop_unused_functions_from_model() {
+        let binding = ffi::new_api_session();
+        let client = match binding.as_ref() {
+            Some(api_ref) => api_ref,
+            None => panic!("Failed to acquire API session handle"),
+        };
+    
+        let vec: Vec<String> = vec![
+            "/tmp/example.c".to_owned()];
+
+        let vect = ffi::translate_vector_of_string(vec);
+        assert_eq!(vect.len(), 1);
+
+        client.load_model_from_files(vect);
+        // Perform a drop of any unused functions.
+        client.drop_unused_functions();
+
+        let msgs = ffi::get_messages();
+        print_response(msgs);
+    }
 }