diff --git a/.github/workflows/syntax-checks.yaml b/.github/workflows/syntax-checks.yaml index eb0479ef5b1..4e259aaeec4 100644 --- a/.github/workflows/syntax-checks.yaml +++ b/.github/workflows/syntax-checks.yaml @@ -47,3 +47,18 @@ jobs: BASE_BRANCH: ${{ github.base_ref }} MERGE_BRANCH: ${{ github.ref }} run: ./.github/workflows/pull-request-check-cpplint.sh + + # This job should take about a minute (est) + check-rustfmt: + runs-on: ubuntu-latest + steps: + - name: Checkout CBMC repository + uses: actions/checkout@v3 + - name: Install latest stable Rust toolchain + uses: actions-rs/toolchain@v1 + with: + toolchain: stable + override: true + components: rustfmt, clippy + - name: Run `cargo fmt` on top of Rust API project + run: cd src/libcprover-rust; cargo fmt --all -- --check diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs index dbeea41efd1..a845ba3cc72 100644 --- a/src/libcprover-rust/build.rs +++ b/src/libcprover-rust/build.rs @@ -20,7 +20,10 @@ fn get_library_build_dir() -> std::io::Result { path.push("lib/"); return Ok(path); } - Err(Error::new(ErrorKind::Other, "failed to get build output directory")) + Err(Error::new( + ErrorKind::Other, + "failed to get build output directory", + )) } fn get_cadical_build_dir() -> std::io::Result { @@ -31,7 +34,10 @@ fn get_cadical_build_dir() -> std::io::Result { path.push("cadical-src/build/"); return Ok(path); } - Err(Error::new(ErrorKind::Other, "failed to get build output directory")) + Err(Error::new( + ErrorKind::Other, + "failed to get build output directory", + )) } fn get_sat_library() -> std::io::Result<&'static str> { @@ -40,13 +46,19 @@ fn get_sat_library() -> std::io::Result<&'static str> { if let Ok(sat_impl) = env_var_fetch_result { let solver_lib = match sat_impl.as_str() { "minisat2" => Ok("minisat2-condensed"), - "glucose" => Ok("glucose-condensed"), - "cadical" => Ok("cadical"), - _ => Err(Error::new(ErrorKind::Other, "no identifiable solver detected")) + "glucose" => Ok("glucose-condensed"), + "cadical" => Ok("cadical"), + _ => Err(Error::new( + ErrorKind::Other, + "no identifiable solver detected", + )), }; return solver_lib; } - Err(Error::new(ErrorKind::Other, "SAT_IMPL environment variable not set")) + Err(Error::new( + ErrorKind::Other, + "SAT_IMPL environment variable not set", + )) } fn main() { @@ -65,12 +77,12 @@ fn main() { let libraries_path = match get_library_build_dir() { Ok(path) => path, - Err(err) => panic!("Error: {}", err) + Err(err) => panic!("Error: {}", err), }; let solver_lib = match get_sat_library() { Ok(solver) => solver, - Err(err) => panic!("Error: {}", err) + Err(err) => panic!("Error: {}", err), }; // Cadical is being built in its own directory, with the resultant artefacts being @@ -79,12 +91,18 @@ fn main() { if solver_lib == "cadical" { let cadical_build_dir = match get_cadical_build_dir() { Ok(cadical_directory) => cadical_directory, - Err(err) => panic!("Error: {}", err) + Err(err) => panic!("Error: {}", err), }; - println!("cargo:rustc-link-search=native={}", cadical_build_dir.display()); + println!( + "cargo:rustc-link-search=native={}", + cadical_build_dir.display() + ); } - println!("cargo:rustc-link-search=native={}", libraries_path.display()); + println!( + "cargo:rustc-link-search=native={}", + libraries_path.display() + ); println!("cargo:rustc-link-lib=static=goto-programs"); println!("cargo:rustc-link-lib=static=util"); println!("cargo:rustc-link-lib=static=langapi"); diff --git a/src/libcprover-rust/src/lib.rs b/src/libcprover-rust/src/lib.rs index a5c35f8fce1..c871ca31166 100644 --- a/src/libcprover-rust/src/lib.rs +++ b/src/libcprover-rust/src/lib.rs @@ -1,4 +1,4 @@ -use cxx::{CxxVector, CxxString}; +use cxx::{CxxString, CxxVector}; #[cxx::bridge] pub mod ffi { @@ -31,7 +31,7 @@ fn print_response(vec: &CxxVector) { .iter() .map(|s| s.to_string_lossy().into_owned()) .collect(); - + for s in vec { println!("{}", s); } @@ -54,14 +54,12 @@ mod tests { #[test] fn translate_vector_of_rust_string_to_cpp() { - let vec: Vec = vec![ - "other/example.c".to_owned(), - "/tmp/example2.c".to_owned()]; + let vec: Vec = vec!["other/example.c".to_owned(), "/tmp/example2.c".to_owned()]; let vect = ffi::translate_vector_of_string(vec); assert_eq!(vect.len(), 2); } - + #[test] fn it_can_load_model_from_file() { let binding = ffi::new_api_session(); @@ -69,9 +67,8 @@ mod tests { Some(api_ref) => api_ref, None => panic!("Failed to acquire API session handle"), }; - - let vec: Vec = vec![ - "other/example.c".to_owned()]; + + let vec: Vec = vec!["other/example.c".to_owned()]; let vect = ffi::translate_vector_of_string(vec); assert_eq!(vect.len(), 1); @@ -87,11 +84,10 @@ mod tests { } #[test] - fn it_can_verify_the_loaded_model() { + fn it_can_verify_the_loaded_model() { let client = ffi::new_api_session(); - - let vec: Vec = vec![ - "other/example.c".to_owned()]; + + let vec: Vec = vec!["other/example.c".to_owned()]; let vect = ffi::translate_vector_of_string(vec); client.load_model_from_files(vect); @@ -112,9 +108,8 @@ mod tests { Some(api_ref) => api_ref, None => panic!("Failed to acquire API session handle"), }; - - let vec: Vec = vec![ - "other/example.c".to_owned()]; + + let vec: Vec = vec!["other/example.c".to_owned()]; let vect = ffi::translate_vector_of_string(vec); assert_eq!(vect.len(), 1);