diff --git a/rustfmt.toml b/rustfmt.toml index 480b19a5e933..e243743efca4 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -13,7 +13,15 @@ ignore = [ # tests for now are not formatted, as they are sometimes pretty-printing constrained # (and generally rustfmt can move around comments in UI-testing incompatible ways) - "src/test", + "src/test/*", + "!src/test/cargo-rmc", + "!src/test/cbmc", + "!src/test/expected", + "!src/test/firecracker", + "!src/test/prusti", + "!src/test/rmc-prelude.rs", + "!src/test/serial", + "!src/test/smack", # do not format submodules "library/backtrace", diff --git a/src/bootstrap/format.rs b/src/bootstrap/format.rs index 2408344487bb..4d529b8382c5 100644 --- a/src/bootstrap/format.rs +++ b/src/bootstrap/format.rs @@ -58,9 +58,9 @@ pub fn format(build: &Build, check: bool, paths: &[PathBuf]) { } let rustfmt_config = t!(std::fs::read_to_string(&rustfmt_config)); let rustfmt_config: RustfmtConfig = t!(toml::from_str(&rustfmt_config)); - let mut ignore_fmt = ignore::overrides::OverrideBuilder::new(&build.src); + let mut ignore_fmt = ignore::gitignore::GitignoreBuilder::new(&build.src); for ignore in rustfmt_config.ignore { - ignore_fmt.add(&format!("!{}", ignore)).expect(&ignore); + ignore_fmt.add_line(None, &ignore).expect(&ignore); } let git_available = match Command::new("git") .arg("--version") @@ -129,7 +129,9 @@ pub fn format(build: &Build, check: bool, paths: &[PathBuf]) { None => WalkBuilder::new(src.clone()), } .types(matcher) - .overrides(ignore_fmt) + .filter_entry(move |e| { + !ignore_fmt.matched(e.path(), e.file_type().unwrap().is_dir()).is_ignore() + }) .build_parallel(); // there is a lot of blocking involved in spawning a child process and reading files to format. diff --git a/src/test/cbmc/DynTrait/different_crates.rs b/src/test/cbmc/DynTrait/different_crates.rs index a007860ea0f7..396659289a89 100644 --- a/src/test/cbmc/DynTrait/different_crates.rs +++ b/src/test/cbmc/DynTrait/different_crates.rs @@ -13,7 +13,7 @@ impl std::iter::Iterator for Counter { type Item = usize; fn next(&mut self) -> Option { - // Increment our count. + // Increment our count. self.count += 1; Some(self.count) } @@ -30,24 +30,24 @@ impl Iterator for Counter { } } -trait Combined : Iterator + std::iter::Iterator {} +trait Combined: Iterator + std::iter::Iterator {} impl Combined for Counter {} -fn std_count(c : &mut dyn std::iter::Iterator) -> usize { +fn std_count(c: &mut dyn std::iter::Iterator) -> usize { c.next().unwrap() } -fn weird_count(c : &mut dyn Iterator) -> usize { +fn weird_count(c: &mut dyn Iterator) -> usize { c.next().unwrap() } fn main() { - let counter : &mut Counter = &mut Counter { count: 0 }; + let counter: &mut Counter = &mut Counter { count: 0 }; assert!(std_count(counter as &mut dyn std::iter::Iterator) == 1); assert!(weird_count(counter as &mut dyn Iterator) == 42); - + let counter_combined = counter as &mut dyn Combined; assert!(std::iter::Iterator::next(counter_combined).unwrap() == 2); assert!(Iterator::next(counter_combined).unwrap() == 42); -} \ No newline at end of file +} diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs index ea51fddb21be..2a8211b4da97 100644 --- a/src/test/cbmc/DynTrait/different_crates_fail.rs +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -13,7 +13,7 @@ impl std::iter::Iterator for Counter { type Item = usize; fn next(&mut self) -> Option { - // Increment our count. + // Increment our count. self.count += 1; Some(self.count) } @@ -30,24 +30,24 @@ impl Iterator for Counter { } } -trait Combined : Iterator + std::iter::Iterator {} +trait Combined: Iterator + std::iter::Iterator {} impl Combined for Counter {} -fn std_count(c : &mut dyn std::iter::Iterator) -> usize { +fn std_count(c: &mut dyn std::iter::Iterator) -> usize { c.next().unwrap() } -fn weird_count(c : &mut dyn Iterator) -> usize { +fn weird_count(c: &mut dyn Iterator) -> usize { c.next().unwrap() } fn main() { - let counter : &mut Counter = &mut Counter { count: 0 }; + let counter: &mut Counter = &mut Counter { count: 0 }; assert!(std_count(counter as &mut dyn std::iter::Iterator) == 0); // Should be 1 assert!(weird_count(counter as &mut dyn Iterator) == 0); // Should be 42 - + let counter_combined = counter as &mut dyn Combined; assert!(std::iter::Iterator::next(counter_combined).unwrap() == 0); // Should be 2 assert!(Iterator::next(counter_combined).unwrap() == 0); // Should be 42 -} \ No newline at end of file +} diff --git a/src/test/cbmc/DynTrait/nested_boxes.rs b/src/test/cbmc/DynTrait/nested_boxes.rs index a4e768dbdf92..90ceb903bc98 100644 --- a/src/test/cbmc/DynTrait/nested_boxes.rs +++ b/src/test/cbmc/DynTrait/nested_boxes.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks the size and align fields for 3-deep nested trait pointers. The +// This test checks the size and align fields for 3-deep nested trait pointers. The // outter 2 dynamic trait objects have fat pointers as their backing data. #![feature(core_intrinsics)] @@ -20,33 +20,33 @@ struct Foo { } fn main() { - let dyn_trait1 : Box = Box::new(Foo{ _a : 1, _b : 2}); - let dyn_trait2 : Box = Box::new(dyn_trait1); - let dyn_trait3 : Box = Box::new(dyn_trait2); + let dyn_trait1: Box = Box::new(Foo { _a: 1, _b: 2 }); + let dyn_trait2: Box = Box::new(dyn_trait1); + let dyn_trait3: Box = Box::new(dyn_trait2); // Do some unsafe magic to check that we generate the right three vtables unsafe { let trait_object3: TraitObject = transmute(dyn_trait3); - + // Outermost trait object // The size is 16, because the data is another fat pointer let vtable3: *mut usize = trait_object3.vtable as *mut usize; assert!(size_from_vtable(vtable3) == 16); assert!(align_from_vtable(vtable3) == 8); - + // Inspect the data pointer from dyn_trait3 let data_ptr3 = trait_object3.data as *mut usize; - + // The second half of this fat pointer is another vtable, for dyn_trait2 let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize); // The size is 16, because the data is another fat pointer assert!(size_from_vtable(vtable2) == 16); assert!(align_from_vtable(vtable2) == 8); - + // Inspect the data pointer from dyn_trait2 let data_ptr2 = *(data_ptr3 as *mut *mut usize); - + // The second half of this fat pointer is another vtable, for dyn_trait1 let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize); diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs index 1a688776bc6f..0c1095b4f1c6 100644 --- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs +++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks the size and align fields for 3-deep nested trait pointers. The +// This test checks the size and align fields for 3-deep nested trait pointers. The // outter 2 dynamic trait objects have fat pointers as their backing data. // In this failing tests, assertions are inverted to use !=. @@ -22,33 +22,33 @@ struct Foo { } fn main() { - let dyn_trait1 : Box = Box::new(Foo{ _a : 1, _b : 2}); - let dyn_trait2 : Box = Box::new(dyn_trait1); - let dyn_trait3 : Box = Box::new(dyn_trait2); + let dyn_trait1: Box = Box::new(Foo { _a: 1, _b: 2 }); + let dyn_trait2: Box = Box::new(dyn_trait1); + let dyn_trait3: Box = Box::new(dyn_trait2); // Do some unsafe magic to check that we generate the right three vtables unsafe { let trait_object3: TraitObject = transmute(dyn_trait3); - + // Outermost trait object // The size is 16, because the data is another fat pointer let vtable3: *mut usize = trait_object3.vtable as *mut usize; assert!(size_from_vtable(vtable3) != 16); assert!(align_from_vtable(vtable3) != 8); - + // Inspect the data pointer from dyn_trait3 let data_ptr3 = trait_object3.data as *mut usize; - + // The second half of this fat pointer is another vtable, for dyn_trait2 let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize); // The size is 16, because the data is another fat pointer assert!(size_from_vtable(vtable2) != 16); assert!(align_from_vtable(vtable2) != 8); - + // Inspect the data pointer from dyn_trait2 let data_ptr2 = *(data_ptr3 as *mut *mut usize); - + // The second half of this fat pointer is another vtable, for dyn_trait1 let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize); diff --git a/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs b/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs index 37293b5d7178..4a378506eb35 100644 --- a/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs +++ b/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -trait WeirdAdd { +trait WeirdAdd { fn add(&self, rhs: i32) -> i32; } impl WeirdAdd for i32 { fn add(&self, other: i32) -> i32 { - self/2 + other/2 + self / 2 + other / 2 } } diff --git a/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs b/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs index 2ca65f1aaa20..982f943f7a7c 100644 --- a/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs +++ b/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs @@ -9,7 +9,7 @@ trait B { } trait T: A + B { - fn foo(&self) -> i32; + fn foo(&self) -> i32; } struct S { diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs index 48d576fd0be5..1db127c57708 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -46,11 +46,7 @@ impl Animal for Cow { // Returns some struct that implements Animal, but we don't know which one at compile time. fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num: 7 }) - } else { - Box::new(Cow { cow_num: 9 }) - } + if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) } } fn main() { diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs index 126e5e0a135d..8c094d428845 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs @@ -49,11 +49,7 @@ impl Animal for Cow { // Returns some struct that implements Animal, but we don't know which one at compile time. fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num: 7 }) - } else { - Box::new(Cow { cow_num: 9 }) - } + if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) } } fn main() { diff --git a/src/test/cbmc/FatPointers/boxmuttrait.rs b/src/test/cbmc/FatPointers/boxmuttrait.rs index fe7a86e31de4..500b158ed8e8 100644 --- a/src/test/cbmc/FatPointers/boxmuttrait.rs +++ b/src/test/cbmc/FatPointers/boxmuttrait.rs @@ -4,9 +4,9 @@ #![feature(raw)] #![allow(deprecated)] +use std::io::{sink, Write}; use std::mem::transmute; use std::raw::TraitObject; -use std::io::{sink, Write}; include!("../Helpers/vtable_utils_ignore.rs"); @@ -19,21 +19,20 @@ fn main() { let num_bytes = log2.write(&buffer).unwrap(); assert!(num_bytes == 5); - // Do some unsafe magic to check that we generate the right two vtables unsafe { let dest_trait_object: TraitObject = transmute(&*dest); - + // The vtable has [&drop, size, align, ....] let dest_vtable_ptr = dest_trait_object.vtable as *mut usize; - + // The size is 16, because the data is another fat pointer assert!(size_from_vtable(dest_vtable_ptr) == 16); assert!(align_from_vtable(dest_vtable_ptr) == 8); - + // Inspect the data pointer from dest let dest_data_ptr = dest_trait_object.data as *mut usize; - + // // The second half of this fat pointer is another vtable, for log let second_vtable_ptr = dest_data_ptr.offset(1) as *mut *mut usize; let second_vtable = *second_vtable_ptr; diff --git a/src/test/cbmc/Helpers/vtable_utils_ignore.rs b/src/test/cbmc/Helpers/vtable_utils_ignore.rs index 74c60d5305c2..8c38d62d6ee7 100644 --- a/src/test/cbmc/Helpers/vtable_utils_ignore.rs +++ b/src/test/cbmc/Helpers/vtable_utils_ignore.rs @@ -1,25 +1,19 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Because each regression test does not share a crate, we just use +// Because each regression test does not share a crate, we just use // an import! to share this code across test directories. -fn drop_from_vtrable(vtable_ptr : *mut usize) -> *mut () { +fn drop_from_vtrable(vtable_ptr: *mut usize) -> *mut () { // 1st pointer-sized position - unsafe { - *vtable_ptr as *mut () - } + unsafe { *vtable_ptr as *mut () } } -fn size_from_vtable(vtable_ptr : *mut usize) -> usize { +fn size_from_vtable(vtable_ptr: *mut usize) -> usize { // 2nd usize-sized position - unsafe { - *(vtable_ptr.offset(1)) - } + unsafe { *(vtable_ptr.offset(1)) } } -fn align_from_vtable(vtable_ptr : *mut usize) -> usize { +fn align_from_vtable(vtable_ptr: *mut usize) -> usize { // 3rd usize-sized position - unsafe { - *(vtable_ptr.offset(2)) - } + unsafe { *(vtable_ptr.offset(2)) } } diff --git a/src/test/expected/assert-eq/main.rs b/src/test/expected/assert-eq/main.rs index b42f7cefce08..1c71877aab15 100644 --- a/src/test/expected/assert-eq/main.rs +++ b/src/test/expected/assert-eq/main.rs @@ -5,14 +5,14 @@ /// This leads us to the land of foreign types, ReifyFnPointer, and transmute. /// The "C" output from RMC is about 1KLOC, vs 80LOC for the same version with straight `assert!`. /// https://github.com/model-checking/rmc/issues/14 -/// The assertion message printed to the user on success is uninformative: +/// The assertion message printed to the user on success is uninformative: /// "library/std/src/macros.rs line 17 a panicking function core::panicking::panic_fmt is invoked: SUCCESS" /// https://github.com/model-checking/rmc/issues/13 fn main() { let x = 1; let y = 2; - assert_eq!(x+1, y); - assert_eq!(x,y);//Expected failure + assert_eq!(x + 1, y); + assert_eq!(x, y); //Expected failure assert_ne!(x, y); } diff --git a/src/test/expected/binop/main.rs b/src/test/expected/binop/main.rs index 806f672f182a..5ab5e26aca59 100644 --- a/src/test/expected/binop/main.rs +++ b/src/test/expected/binop/main.rs @@ -71,4 +71,4 @@ fn main() { iband_test(3, 10, 2, 3); ibor_test(0, 2389034, 2389034, 0); ibxor_test(0, 2389034, 2389034, 0); -} \ No newline at end of file +} diff --git a/src/test/expected/closure/main.rs b/src/test/expected/closure/main.rs index 127d348c4c98..23f6b6446254 100644 --- a/src/test/expected/closure/main.rs +++ b/src/test/expected/closure/main.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // cbmc-flags: --signed-overflow-check fn call_with_one(mut some_closure: F) -> () - where - F: FnMut(i64, i64) -> (), +where + F: FnMut(i64, i64) -> (), { some_closure(1, 1); } diff --git a/src/test/expected/closure3/main.rs b/src/test/expected/closure3/main.rs index 04606228b5a7..a8de5624036d 100644 --- a/src/test/expected/closure3/main.rs +++ b/src/test/expected/closure3/main.rs @@ -1,8 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn call_with_one(f: F) -> T - where - F: FnOnce(i64) -> T, +where + F: FnOnce(i64) -> T, { f(10) } diff --git a/src/test/expected/comp/main.rs b/src/test/expected/comp/main.rs index dad03af40029..ee9803ad673b 100644 --- a/src/test/expected/comp/main.rs +++ b/src/test/expected/comp/main.rs @@ -21,4 +21,4 @@ fn main() { eq1(a, b); eq2(a, b); } -} \ No newline at end of file +} diff --git a/src/test/expected/generics/expected b/src/test/expected/generics/expected index 1f233ac60a3c..b778feee4fe4 100644 --- a/src/test/expected/generics/expected +++ b/src/test/expected/generics/expected @@ -1,2 +1,2 @@ -line 24 assertion failed: x == y.data: SUCCESS -line 25 assertion failed: z == w.data: SUCCESS +line 21 assertion failed: x == y.data: SUCCESS +line 22 assertion failed: z == w.data: SUCCESS diff --git a/src/test/expected/generics/main.rs b/src/test/expected/generics/main.rs index 7814ea3920a7..b8edeedf1fd2 100644 --- a/src/test/expected/generics/main.rs +++ b/src/test/expected/generics/main.rs @@ -10,10 +10,7 @@ fn ident(x: T) -> T { } fn wrapped(x: T) -> Foo { - Foo { - data: ident(x), - i: 0, - } + Foo { data: ident(x), i: 0 } } fn main() { diff --git a/src/test/expected/replace-hashmap/expected b/src/test/expected/replace-hashmap/expected index 0ef1d94c6f99..835bdfb4723a 100644 --- a/src/test/expected/replace-hashmap/expected +++ b/src/test/expected/replace-hashmap/expected @@ -1,5 +1,5 @@ -line 26 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS -line 26 arithmetic overflow on unsigned + in self->len + 1: SUCCESS +line 31 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS +line 31 arithmetic overflow on unsigned + in self->len + 1: SUCCESS line 56 assertion failed: a.is_some(): FAILURE line 57 assertion failed: a.is_none(): FAILURE line 59 assertion failed: b.is_some(): SUCCESS diff --git a/src/test/expected/replace-hashmap/main.rs b/src/test/expected/replace-hashmap/main.rs index 5ff7ad55d0fa..bb18944e5696 100644 --- a/src/test/expected/replace-hashmap/main.rs +++ b/src/test/expected/replace-hashmap/main.rs @@ -1,25 +1,30 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // cbmc-flags: --unsigned-overflow-check +use std::borrow::Borrow; +use std::collections::hash_map::RandomState; use std::collections::HashMap; use std::hash::Hash; -use std::collections::hash_map::RandomState; -use std::borrow::Borrow; include!("../../rmc-prelude.rs"); use std::marker::PhantomData; -struct CbmcHashMap {len: usize, _k : PhantomData, _s : PhantomData, last : Option} +struct CbmcHashMap { + len: usize, + _k: PhantomData, + _s: PhantomData, + last: Option, +} -impl CbmcHashMap { - fn new() -> CbmcHashMap { - CbmcHashMap {len: 0, _k: PhantomData, _s: PhantomData, last: None} +impl CbmcHashMap { + fn new() -> CbmcHashMap { + CbmcHashMap { len: 0, _k: PhantomData, _s: PhantomData, last: None } } - fn len(&self) -> usize { + fn len(&self) -> usize { self.len } } -impl CbmcHashMap { +impl CbmcHashMap { pub fn insert(&mut self, k: K, v: V) -> Option { self.last = Some(v); if __nondet() { @@ -29,30 +34,25 @@ impl CbmcHashMap { } pub fn get(&self, k: &Q) -> Option<&V> where - K: Borrow,{ - if false { - __nondet() - } else { - self.last.as_ref() - } - } + K: Borrow, + { + if false { __nondet() } else { self.last.as_ref() } + } } -fn make_map_visible() -{ - let mut v : CbmcHashMap = CbmcHashMap::new(); +fn make_map_visible() { + let mut v: CbmcHashMap = CbmcHashMap::new(); v.len; v.insert(__nondet(), __nondet()); - let k : K = __nondet(); + let k: K = __nondet(); v.get(&k); } -fn test_actual_map(key: K, value: V) -{ - make_map_visible::(); +fn test_actual_map(key: K, value: V) { + make_map_visible::(); - let mut v : HashMap = HashMap::new(); - let a = v.insert(key,value); + let mut v: HashMap = HashMap::new(); + let a = v.insert(key, value); assert!(a.is_some()); assert!(a.is_none()); let b = v.get(&key); @@ -61,5 +61,5 @@ fn test_actual_map(key: K, value: V) } fn main() { - test_actual_map::(1,3); + test_actual_map::(1, 3); } diff --git a/src/test/expected/replace-vec/expected b/src/test/expected/replace-vec/expected index 37cd7312c8f2..7a98f73b07a9 100644 --- a/src/test/expected/replace-vec/expected +++ b/src/test/expected/replace-vec/expected @@ -1,8 +1,8 @@ -line 22 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS -line 32 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS -line 51 assertion failed: v.len() == 1: SUCCESS -line 52 assertion failed: v.len() == 11: FAILURE -line 54 assertion failed: p != None: SUCCESS -line 55 assertion failed: p == None: FAILURE -line 56 assertion failed: p == Some(to_push): SUCCESS -line 57 assertion failed: p == Some(not_pushed): FAILURE +line 25 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS +line 35 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS +line 53 assertion failed: v.len() == 1: SUCCESS +line 54 assertion failed: v.len() == 11: FAILURE +line 56 assertion failed: p != None: SUCCESS +line 57 assertion failed: p == None: FAILURE +line 58 assertion failed: p == Some(to_push): SUCCESS +line 59 assertion failed: p == Some(not_pushed): FAILURE diff --git a/src/test/expected/replace-vec/main.rs b/src/test/expected/replace-vec/main.rs index f30c7b59a4a1..0f5f10957771 100644 --- a/src/test/expected/replace-vec/main.rs +++ b/src/test/expected/replace-vec/main.rs @@ -4,25 +4,28 @@ include!("../../rmc-prelude.rs"); -use std::marker::PhantomData; use std::alloc::Allocator; use std::alloc::Global; +use std::marker::PhantomData; struct CbmcVec { - len: usize, _x : PhantomData, last : Option, _y : PhantomData + len: usize, + _x: PhantomData, + last: Option, + _y: PhantomData, } -impl CbmcVec { +impl CbmcVec { fn new() -> CbmcVec { - CbmcVec {len: 0, _x: PhantomData, last: None, _y: PhantomData} + CbmcVec { len: 0, _x: PhantomData, last: None, _y: PhantomData } } } -impl CbmcVec { - fn push(&mut self, val : T){ +impl CbmcVec { + fn push(&mut self, val: T) { self.len += 1; self.last = Some(val); } - fn len(&self) -> usize { + fn len(&self) -> usize { self.len } fn pop(&mut self) -> Option { @@ -35,18 +38,17 @@ impl CbmcVec { } } } -fn make_vec_visible() -{ - let mut v : CbmcVec = CbmcVec::new(); +fn make_vec_visible() { + let mut v: CbmcVec = CbmcVec::new(); v.push(__nondet()); v.len(); v.pop(); } -fn test_actual_vec(to_push:T, not_pushed:T){ +fn test_actual_vec(to_push: T, not_pushed: T) { make_vec_visible::(); - let mut v : Vec = Vec::new(); + let mut v: Vec = Vec::new(); v.push(to_push); assert!(v.len() == 1); assert!(v.len() == 11); @@ -59,7 +61,7 @@ fn test_actual_vec(to_push:T, not_pushed:T){ fn main() { test_actual_vec::('a', 'b'); - test_actual_vec::(true,false); + test_actual_vec::(true, false); test_actual_vec::(1, 3); test_actual_vec::(1.1, 3.14); test_actual_vec::(1.1, 3.14); diff --git a/src/test/expected/static-mutable-struct/expected b/src/test/expected/static-mutable-struct/expected index 7aebe5d2cef1..2ce4276890b6 100644 --- a/src/test/expected/static-mutable-struct/expected +++ b/src/test/expected/static-mutable-struct/expected @@ -1,12 +1,12 @@ -line 25 assertion failed: foo().x == 12: SUCCESS -line 26 assertion failed: foo().y == 12: FAILURE -line 27 assertion failed: foo().x == 14: FAILURE -line 28 assertion failed: foo().y == 14: SUCCESS -line 31 assertion failed: foo().x == 1: SUCCESS -line 32 assertion failed: foo().y == 1: FAILURE -line 33 assertion failed: foo().x == 2: FAILURE -line 34 assertion failed: foo().y == 2: SUCCESS -line 37 assertion failed: foo().x == 1 << 62: SUCCESS -line 38 assertion failed: foo().x == 1 << 31: FAILURE -line 39 assertion failed: foo().y == 1 << 31: SUCCESS +line 23 assertion failed: foo().x == 12: SUCCESS +line 24 assertion failed: foo().y == 12: FAILURE +line 25 assertion failed: foo().x == 14: FAILURE +line 26 assertion failed: foo().y == 14: SUCCESS +line 29 assertion failed: foo().x == 1: SUCCESS +line 30 assertion failed: foo().y == 1: FAILURE +line 31 assertion failed: foo().x == 2: FAILURE +line 32 assertion failed: foo().y == 2: SUCCESS +line 35 assertion failed: foo().x == 1 << 62: SUCCESS +line 36 assertion failed: foo().x == 1 << 31: FAILURE +line 37 assertion failed: foo().y == 1 << 31: SUCCESS diff --git a/src/test/expected/static-mutable-struct/main.rs b/src/test/expected/static-mutable-struct/main.rs index 3c74016fc2dd..963063136306 100644 --- a/src/test/expected/static-mutable-struct/main.rs +++ b/src/test/expected/static-mutable-struct/main.rs @@ -1,20 +1,18 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT #[derive(Copy, Clone)] -struct TestStruct { - x : i64, - y : i32 +struct TestStruct { + x: i64, + y: i32, } -static mut X : TestStruct = TestStruct {x : 12, y: 14}; +static mut X: TestStruct = TestStruct { x: 12, y: 14 }; fn foo() -> TestStruct { - unsafe { - X - } + unsafe { X } } -fn mutate_the_thing(nx : i64, ny : i32) { +fn mutate_the_thing(nx: i64, ny: i32) { unsafe { X.x = nx; X.y = ny; @@ -27,15 +25,14 @@ fn main() { assert!(foo().x == 14); assert!(foo().y == 14); - mutate_the_thing(1,2); + mutate_the_thing(1, 2); assert!(foo().x == 1); assert!(foo().y == 1); assert!(foo().x == 2); - assert!(foo().y == 2); + assert!(foo().y == 2); mutate_the_thing(1 << 62, 1 << 31); assert!(foo().x == 1 << 62); assert!(foo().x == 1 << 31); - assert!(foo().y == 1 << 31); - + assert!(foo().y == 1 << 31); } diff --git a/src/test/expected/static-mutable/expected b/src/test/expected/static-mutable/expected index 689193329edf..1e47840833bb 100644 --- a/src/test/expected/static-mutable/expected +++ b/src/test/expected/static-mutable/expected @@ -1,4 +1,4 @@ -line 18 assertion failed: 10 == foo(): FAILURE -line 19 assertion failed: 12 == foo(): SUCCESS -line 21 assertion failed: 10 == foo(): SUCCESS -line 22 assertion failed: 12 == foo(): FAILURE +line 16 assertion failed: 10 == foo(): FAILURE +line 17 assertion failed: 12 == foo(): SUCCESS +line 19 assertion failed: 10 == foo(): SUCCESS +line 20 assertion failed: 12 == foo(): FAILURE diff --git a/src/test/expected/static-mutable/main.rs b/src/test/expected/static-mutable/main.rs index f3a27b15672e..6fbe66149fb8 100644 --- a/src/test/expected/static-mutable/main.rs +++ b/src/test/expected/static-mutable/main.rs @@ -3,12 +3,10 @@ static mut X: i32 = 12; fn foo() -> i32 { - unsafe { - X - } + unsafe { X } } -fn mutate_the_thing(new : i32) { +fn mutate_the_thing(new: i32) { unsafe { X = new; } diff --git a/src/test/expected/transmute/expected b/src/test/expected/transmute/expected index 84f0c9c72b85..43617fc39881 100644 --- a/src/test/expected/transmute/expected +++ b/src/test/expected/transmute/expected @@ -1,2 +1,2 @@ -line 7 assertion failed: bitpattern == 0x3F800000: SUCCESS -line 13 assertion failed: f == 1.0: SUCCESS +line 5 assertion failed: bitpattern == 0x3F800000: SUCCESS +line 11 assertion failed: f == 1.0: SUCCESS diff --git a/src/test/expected/transmute/main.rs b/src/test/expected/transmute/main.rs index 3debebef0269..809f91c9050d 100644 --- a/src/test/expected/transmute/main.rs +++ b/src/test/expected/transmute/main.rs @@ -1,13 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT fn main() { - let bitpattern = unsafe { - std::mem::transmute::(1.0) - }; + let bitpattern = unsafe { std::mem::transmute::(1.0) }; assert!(bitpattern == 0x3F800000); let f = unsafe { - let i :u32 = 0x3F800000; + let i: u32 = 0x3F800000; std::mem::transmute::(i) }; assert!(f == 1.0);