From 810d0aad8c3fca6eb7e77ea5c7d8e8a77ca9a989 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 22 Nov 2021 20:04:44 +0000 Subject: [PATCH] Testing: Revert `pub` changes in main function --- rmc-docs/src/install-guide.md | 2 +- src/test/expected/allocation/main.rs | 2 +- src/test/expected/array/main.rs | 2 +- src/test/expected/assert-eq/main.rs | 2 +- src/test/expected/binop/main.rs | 2 +- src/test/expected/closure/main.rs | 2 +- src/test/expected/closure2/main.rs | 2 +- src/test/expected/closure3/main.rs | 2 +- src/test/expected/comp/main.rs | 2 +- src/test/expected/copy/main.rs | 2 +- src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs | 2 +- src/test/expected/dry-run-flag-conflict/main.rs | 2 +- src/test/expected/dry-run/main.rs | 2 +- src/test/expected/dynamic-error-trait/main.rs | 2 +- src/test/expected/dynamic-trait-static-dispatch/main.rs | 2 +- src/test/expected/dynamic-trait/main.rs | 2 +- src/test/expected/enum/main.rs | 2 +- src/test/expected/float-nan/main.rs | 2 +- src/test/expected/generics/main.rs | 2 +- src/test/expected/iterator/main.rs | 2 +- src/test/expected/niche/main.rs | 2 +- src/test/expected/niche2/main.rs | 2 +- src/test/expected/nondet/main.rs | 2 +- src/test/expected/references/main.rs | 2 +- src/test/expected/slice/main.rs | 2 +- src/test/expected/static-mutable-struct/main.rs | 2 +- src/test/expected/static-mutable/main.rs | 2 +- src/test/expected/static/main.rs | 2 +- src/test/expected/test1/main.rs | 2 +- src/test/expected/test2/main.rs | 2 +- src/test/expected/test3/main.rs | 2 +- src/test/expected/test4/main.rs | 2 +- src/test/expected/test5/main.rs | 2 +- src/test/expected/test6/main.rs | 2 +- src/test/expected/transmute/main.rs | 2 +- src/test/expected/unwind_tip/main.rs | 2 +- src/test/expected/vec/main.rs | 2 +- src/test/expected/vecdq/main.rs | 2 +- src/test/firecracker/virtio-block-parse/main.rs | 2 +- src/test/prusti/100_doors.rs | 2 +- src/test/prusti/Ackermann_function.rs | 2 +- src/test/prusti/Binary_search.rs | 2 +- src/test/prusti/Fibonacci_sequence.rs | 2 +- src/test/prusti/Heapsort.rs | 2 +- src/test/prusti/Selection_sort.rs | 2 +- src/test/prusti/Tower_of_Hanoi.rs | 2 +- src/test/prusti/borrow_first.rs | 2 +- src/test/rmc/ArithEqualOperators/main.rs | 2 +- src/test/rmc/Asm/main_fixme.rs | 2 +- src/test/rmc/Assert/UninitValid/fixme_main.rs | 2 +- src/test/rmc/Assert/ZeroValid/fixme_main.rs | 2 +- src/test/rmc/Assert/ZeroValid/main.rs | 2 +- src/test/rmc/Assume/main.rs | 2 +- src/test/rmc/Assume/main_fail.rs | 2 +- src/test/rmc/Atomics/Stable/CompareExchange/main.rs | 2 +- src/test/rmc/Atomics/Stable/Exchange/main.rs | 2 +- src/test/rmc/Atomics/Stable/Fence/main.rs | 2 +- src/test/rmc/Atomics/Stable/FetchAdd/main.rs | 2 +- src/test/rmc/Atomics/Stable/FetchAnd/main.rs | 2 +- src/test/rmc/Atomics/Stable/FetchOr/main.rs | 2 +- src/test/rmc/Atomics/Stable/FetchSub/main.rs | 2 +- src/test/rmc/Atomics/Stable/FetchXor/main.rs | 2 +- src/test/rmc/Atomics/Stable/Load/main.rs | 2 +- src/test/rmc/Atomics/Stable/Store/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicAdd/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicAnd/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicCxchg/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicFence/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicLoad/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicOr/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicStore/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicSub/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicXchg/main.rs | 2 +- src/test/rmc/Atomics/Unstable/AtomicXor/main.rs | 2 +- src/test/rmc/BinOp_Offset/main.rs | 2 +- src/test/rmc/BinOp_Offset/main_fail.rs | 4 ++-- src/test/rmc/BitManipulation/Stable/fixme_main.rs | 2 +- src/test/rmc/BitManipulation/Unstable/Rotate/main.rs | 2 +- src/test/rmc/BitManipulation/Unstable/fixme_main.rs | 2 +- src/test/rmc/BitwiseArithOperators/bool.rs | 2 +- src/test/rmc/BitwiseArithOperators/main.rs | 2 +- src/test/rmc/BitwiseEqualOperators/main.rs | 2 +- src/test/rmc/BitwiseShiftOperators/Usize/main.rs | 2 +- src/test/rmc/BitwiseShiftOperators/main.rs | 2 +- src/test/rmc/Bool-BoolOperators/main.rs | 2 +- src/test/rmc/Cast/cast_abstract_args_to_concrete.rs | 2 +- src/test/rmc/Cast/from_be_bytes.rs | 2 +- src/test/rmc/Cast/main.rs | 2 +- src/test/rmc/Cast/path.rs | 2 +- src/test/rmc/Closure/main.rs | 2 +- src/test/rmc/CodegenConstValue/bigints.rs | 2 +- src/test/rmc/CodegenConstValue/main.rs | 2 +- src/test/rmc/CodegenConstValue/u128.rs | 2 +- src/test/rmc/CodegenMisc/main.rs | 2 +- src/test/rmc/CodegenStatic/main.rs | 2 +- src/test/rmc/CodegenStatic/struct.rs | 2 +- src/test/rmc/CopyIntrinsics/main.rs | 2 +- src/test/rmc/Count/Unstable/Ctlz/bounds.rs | 2 +- src/test/rmc/Count/Unstable/Ctlz/main.rs | 2 +- src/test/rmc/Count/Unstable/Cttz/bounds.rs | 2 +- src/test/rmc/Count/Unstable/Cttz/main.rs | 2 +- src/test/rmc/DynTrait/any_cast_int.rs | 2 +- src/test/rmc/DynTrait/any_cast_int_fail.rs | 2 +- src/test/rmc/DynTrait/boxed_closure.rs | 2 +- src/test/rmc/DynTrait/boxed_closure_fail.rs | 2 +- src/test/rmc/DynTrait/boxed_debug_cast.rs | 2 +- src/test/rmc/DynTrait/boxed_trait.rs | 2 +- src/test/rmc/DynTrait/boxed_trait_fail.rs | 2 +- src/test/rmc/DynTrait/different_crates.rs | 2 +- src/test/rmc/DynTrait/different_crates_fail.rs | 2 +- src/test/rmc/DynTrait/drop_boxed_dyn.rs | 2 +- src/test/rmc/DynTrait/drop_concrete.rs | 2 +- src/test/rmc/DynTrait/drop_dyn_pointer.rs | 2 +- src/test/rmc/DynTrait/drop_nested_boxed_dyn.rs | 2 +- src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_mut.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_mut_fail.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_once.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_once_fail.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param_closure.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param_closure_capture.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs | 2 +- src/test/rmc/DynTrait/dyn_fn_param_fail.rs | 2 +- src/test/rmc/DynTrait/generic_duplicate_names.rs | 2 +- src/test/rmc/DynTrait/generic_duplicate_names_fail.rs | 2 +- src/test/rmc/DynTrait/generic_duplicate_names_impl.rs | 2 +- src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs | 2 +- src/test/rmc/DynTrait/main.rs | 2 +- src/test/rmc/DynTrait/main_fail.rs | 2 +- src/test/rmc/DynTrait/nested_boxes.rs | 2 +- src/test/rmc/DynTrait/nested_boxes_fail.rs | 2 +- src/test/rmc/DynTrait/nested_closures.rs | 2 +- src/test/rmc/DynTrait/nested_closures_fail.rs | 2 +- src/test/rmc/DynTrait/object_safe_generics.rs | 2 +- src/test/rmc/DynTrait/object_safe_trait.rs | 2 +- src/test/rmc/DynTrait/std_lib_add_duplicate.rs | 2 +- src/test/rmc/DynTrait/vtable_duplicate_field_override.rs | 2 +- src/test/rmc/DynTrait/vtable_duplicate_fields.rs | 2 +- src/test/rmc/DynTrait/vtable_size_align_drop.rs | 2 +- src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs | 2 +- src/test/rmc/EQ-NE/main.rs | 2 +- src/test/rmc/Enum/main.rs | 2 +- src/test/rmc/Enum/min_offset.rs | 2 +- src/test/rmc/Enum/result1.rs | 2 +- src/test/rmc/Enum/result2.rs | 2 +- src/test/rmc/Enum/result3.rs | 2 +- src/test/rmc/Enum/variants_multiple_len_2.rs | 2 +- src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_0.rs | 2 +- src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_1.rs | 2 +- src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_2.rs | 2 +- src/test/rmc/Enum/variants_single_len_2_fields_arbitrary_1.rs | 2 +- src/test/rmc/ExactDiv/main.rs | 2 +- src/test/rmc/FatPointers/boxmuttrait.rs | 2 +- src/test/rmc/FatPointers/boxmuttrait_fail.rs | 2 +- src/test/rmc/FatPointers/boxslice1.rs | 2 +- src/test/rmc/FatPointers/boxslice2.rs | 2 +- src/test/rmc/FatPointers/boxtrait.rs | 2 +- src/test/rmc/FatPointers/boxtrait_fail.rs | 2 +- src/test/rmc/FatPointers/fixme_slice2.rs | 2 +- src/test/rmc/FatPointers/slice1.rs | 2 +- src/test/rmc/FatPointers/slice3.rs | 2 +- src/test/rmc/FatPointers/structslice.rs | 2 +- src/test/rmc/FatPointers/trait1.rs | 2 +- src/test/rmc/FatPointers/trait1_fail.rs | 2 +- src/test/rmc/FatPointers/trait2.rs | 2 +- src/test/rmc/FatPointers/trait2_fail.rs | 2 +- src/test/rmc/FatPointers/trait3.rs | 2 +- src/test/rmc/FatPointers/trait3_fail.rs | 2 +- src/test/rmc/FloatingPoint/main.rs | 2 +- src/test/rmc/ForeignItems/fixme_main.rs | 2 +- src/test/rmc/ForeignItems/fixme_varadic.rs | 2 +- src/test/rmc/ForeignItems/main.rs | 2 +- src/test/rmc/ForeignItems/missing_fn_fail.rs | 2 +- src/test/rmc/FunctionAbstractions/mem_replace.rs | 2 +- src/test/rmc/FunctionAbstractions/mem_swap.rs | 2 +- src/test/rmc/FunctionAbstractions/ptr_read.rs | 2 +- src/test/rmc/FunctionAbstractions/ptr_write.rs | 2 +- src/test/rmc/FunctionCall/FnPtr/main.rs | 2 +- src/test/rmc/FunctionCall/Variadic/fixme_main.rs | 2 +- src/test/rmc/FunctionCall/Variadic/main.rs | 2 +- src/test/rmc/FunctionCall_ImplicitReturn/main.rs | 2 +- src/test/rmc/FunctionCall_NoRet-NoParam/main.rs | 2 +- src/test/rmc/FunctionCall_NoRet-Param/main.rs | 2 +- src/test/rmc/FunctionCall_Ret-NoParam/main.rs | 2 +- src/test/rmc/FunctionCall_Ret-Param/main.rs | 2 +- src/test/rmc/Generator/main.rs | 2 +- src/test/rmc/IfElseifElse_NonReturning/main.rs | 2 +- src/test/rmc/IfElseifElse_Returning/main.rs | 2 +- src/test/rmc/Intrinsics/abort.rs | 2 +- src/test/rmc/Intrinsics/black_box.rs | 2 +- src/test/rmc/Intrinsics/fixme_catch_unwind.rs | 2 +- src/test/rmc/Intrinsics/fixme_try.rs | 2 +- src/test/rmc/Intrinsics/needs_drop.rs | 2 +- src/test/rmc/Intrinsics/raw_eq.rs | 2 +- src/test/rmc/Iterator/try_fold.rs | 2 +- src/test/rmc/LT-GT-LE-GE/main.rs | 2 +- src/test/rmc/LoopLoop_NonReturning/main.rs | 2 +- src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs | 2 +- src/test/rmc/LoopWhile_NonReturning/main.rs | 2 +- src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs | 2 +- src/test/rmc/MemReplace/main.rs | 2 +- src/test/rmc/Never/main.rs | 2 +- src/test/rmc/Never/never_return.rs | 2 +- src/test/rmc/NondetVectors/bytes.rs | 2 +- src/test/rmc/NondetVectors/fixme_main.rs | 2 +- src/test/rmc/Parenths/main.rs | 2 +- src/test/rmc/PointerOffset/Stable/main.rs | 2 +- src/test/rmc/PointerOffset/Unstable/main.rs | 2 +- src/test/rmc/PointerOffset/Unstable/main_fail.rs | 2 +- src/test/rmc/Pointers_Basic/fixme_from_raw.rs | 2 +- src/test/rmc/Pointers_Basic/main.rs | 2 +- src/test/rmc/Pointers_Functions/main.rs | 2 +- src/test/rmc/Pointers_InAssert/main.rs | 2 +- src/test/rmc/Pointers_OtherTypes/main.rs | 2 +- src/test/rmc/Pointers_OutOfScopeFail/fixme_main.rs | 2 +- src/test/rmc/ProjectionElem/ConstantIndex/main.rs | 2 +- src/test/rmc/Refs/fixme_main.rs | 2 +- src/test/rmc/Repr/main.rs | 2 +- src/test/rmc/SIMD/Compare/main.rs | 2 +- src/test/rmc/SIMD/Construction/main.rs | 2 +- src/test/rmc/SIMD/Operators/main.rs | 2 +- src/test/rmc/SIMD/Shuffle/main.rs | 2 +- src/test/rmc/SaturatingIntrinsics/fixme_128.rs | 2 +- src/test/rmc/SaturatingIntrinsics/main.rs | 2 +- src/test/rmc/Scopes_NonReturning/main.rs | 2 +- src/test/rmc/Scopes_Returning/main.rs | 2 +- src/test/rmc/Serde/main.rs | 2 +- src/test/rmc/SizeAndAlignOfDst/main_assert_fixme.rs | 2 +- src/test/rmc/SizeAndAlignOfDst/main_fixme.rs | 2 +- src/test/rmc/Slice/codegen.rs | 2 +- src/test/rmc/Slice/drop_in_place.rs | 2 +- src/test/rmc/Slice/main.rs | 2 +- src/test/rmc/Slice/pathbuf.rs | 2 +- src/test/rmc/Slice/slice.rs | 2 +- src/test/rmc/Slice/slice_from_raw.rs | 2 +- src/test/rmc/Static/main.rs | 2 +- src/test/rmc/Static/table_of_pairs.rs | 2 +- src/test/rmc/Static/table_of_pairs2.rs | 2 +- src/test/rmc/Strings/copy_empty_string_by_intrinsic.rs | 2 +- src/test/rmc/Strings/copy_empty_string_by_intrinsic_fixme.rs | 2 +- src/test/rmc/Strings/copy_empty_string_by_ref.rs | 2 +- src/test/rmc/Strings/fixme_boxed_str.rs | 2 +- src/test/rmc/Strings/fixme_main.rs | 2 +- src/test/rmc/Strings/fixme_os_str.rs | 2 +- src/test/rmc/Strings/main.rs | 2 +- src/test/rmc/Strings/os_str_reduced.rs | 2 +- src/test/rmc/SubSlice/subslice1.rs | 2 +- src/test/rmc/SubSlice/subslice2_fixme.rs | 2 +- src/test/rmc/SwitchInt/main.rs | 2 +- src/test/rmc/Transparent/transparent1.rs | 2 +- src/test/rmc/Transparent/transparent2.rs | 2 +- src/test/rmc/Transparent/transparent3.rs | 2 +- src/test/rmc/Transparent/transparent4.rs | 2 +- src/test/rmc/Unit/main.rs | 2 +- src/test/rmc/UnsafeBlocks_Useless/main.rs | 2 +- src/test/rmc/Vectors/fixme_main.rs | 2 +- src/test/rmc/Vectors/vector_extend.rs | 2 +- src/test/rmc/Vectors/vector_extend_fail.rs | 2 +- src/test/rmc/Vectors/vector_extend_in_new.rs | 2 +- src/test/rmc/VolatileIntrinsics/core_intrinsics.rs | 2 +- src/test/rmc/VolatileIntrinsics/main.rs | 2 +- src/test/rmc/Whitespace/main.rs | 2 +- src/test/rmc/i32-Unary-/main.rs | 2 +- 265 files changed, 266 insertions(+), 266 deletions(-) diff --git a/rmc-docs/src/install-guide.md b/rmc-docs/src/install-guide.md index 5d5c2163b719..9ce811182b7b 100644 --- a/rmc-docs/src/install-guide.md +++ b/rmc-docs/src/install-guide.md @@ -85,7 +85,7 @@ Create a test file: ```rust // File: test.rs -pub fn main() { +fn main() { assert!(1 == 2); } ``` diff --git a/src/test/expected/allocation/main.rs b/src/test/expected/allocation/main.rs index 26c7993179d4..4cc6c3194816 100644 --- a/src/test/expected/allocation/main.rs +++ b/src/test/expected/allocation/main.rs @@ -4,7 +4,7 @@ fn foo() -> Option { None } -pub fn main() { +fn main() { assert!(foo() == None); let x = foo(); let y: Option = None; diff --git a/src/test/expected/array/main.rs b/src/test/expected/array/main.rs index 288d1cfcd98a..4d65a7196884 100644 --- a/src/test/expected/array/main.rs +++ b/src/test/expected/array/main.rs @@ -5,7 +5,7 @@ fn foo(x: [i32; 5]) -> [i32; 2] { [x[0], x[1]] } -pub fn main() { +fn main() { let x = [1, 2, 3, 4, 5]; let y = foo(x); let z = 2; diff --git a/src/test/expected/assert-eq/main.rs b/src/test/expected/assert-eq/main.rs index 3efb3eca14d8..1c71877aab15 100644 --- a/src/test/expected/assert-eq/main.rs +++ b/src/test/expected/assert-eq/main.rs @@ -9,7 +9,7 @@ /// "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 -pub fn main() { +fn main() { let x = 1; let y = 2; assert_eq!(x + 1, y); diff --git a/src/test/expected/binop/main.rs b/src/test/expected/binop/main.rs index 637b2d2e25b7..5ab5e26aca59 100644 --- a/src/test/expected/binop/main.rs +++ b/src/test/expected/binop/main.rs @@ -55,7 +55,7 @@ fn ibxor_test(a: i32, b: i32, correct: i32, wrong: i32) { assert!(a ^ b == wrong); } -pub fn main() { +fn main() { iadd_test(1, 2, 3, 4); isub_test(3, 4, -1, 0); imul_test(5, 6, 30, 60); diff --git a/src/test/expected/closure/main.rs b/src/test/expected/closure/main.rs index df6d0fd13834..152b8b958e7b 100644 --- a/src/test/expected/closure/main.rs +++ b/src/test/expected/closure/main.rs @@ -8,7 +8,7 @@ where some_closure(1, 1); } -pub fn main() { +fn main() { let mut num: i32 = rmc::nondet(); let y = 2; if num <= std::i32::MAX - 100 { diff --git a/src/test/expected/closure2/main.rs b/src/test/expected/closure2/main.rs index 1c100a1947ad..4884c00943ad 100644 --- a/src/test/expected/closure2/main.rs +++ b/src/test/expected/closure2/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x = 2; let f = |y| x + y; let z = f(100); diff --git a/src/test/expected/closure3/main.rs b/src/test/expected/closure3/main.rs index fe76b9e14cac..afb1fde1ccd6 100644 --- a/src/test/expected/closure3/main.rs +++ b/src/test/expected/closure3/main.rs @@ -7,7 +7,7 @@ where f(10) } -pub fn main() { +fn main() { let num: i64 = rmc::nondet(); if num <= std::i64::MAX - 100 { // avoid overflow diff --git a/src/test/expected/comp/main.rs b/src/test/expected/comp/main.rs index 4f49318ba5a9..472b49ef8088 100644 --- a/src/test/expected/comp/main.rs +++ b/src/test/expected/comp/main.rs @@ -12,7 +12,7 @@ fn eq2(a: i32, b: i32) { assert!(a - b < a); } -pub fn main() { +fn main() { let a = rmc::nondet(); let b = rmc::nondet(); if a > -400 && a < 100 && b < 200 && b > 0 { diff --git a/src/test/expected/copy/main.rs b/src/test/expected/copy/main.rs index 3f606282bf61..c38f29332524 100644 --- a/src/test/expected/copy/main.rs +++ b/src/test/expected/copy/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::ptr; -pub fn main() { +fn main() { // TODO: make an overlapping set of locations, and check that it does the right thing for the overlapping region too. // https://github.com/model-checking/rmc/issues/12 let expected_val = 42; diff --git a/src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs b/src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs index 5187b15bbd43..8fe57ccdab32 100644 --- a/src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs +++ b/src/test/expected/dry-run-flag-conflict-auto-unwind/main.rs @@ -7,4 +7,4 @@ // `--dry-run` causes RMC to print out commands instead of running them // In `expected` you will find substrings of these commands because the // concrete paths depend on your working directory. -pub fn main() {} +fn main() {} diff --git a/src/test/expected/dry-run-flag-conflict/main.rs b/src/test/expected/dry-run-flag-conflict/main.rs index 1b329352352a..25b30d73294f 100644 --- a/src/test/expected/dry-run-flag-conflict/main.rs +++ b/src/test/expected/dry-run-flag-conflict/main.rs @@ -7,4 +7,4 @@ // `--dry-run` causes RMC to print out commands instead of running them // In `expected` you will find substrings of these commands because the // concrete paths depend on your working directory. -pub fn main() {} +fn main() {} diff --git a/src/test/expected/dry-run/main.rs b/src/test/expected/dry-run/main.rs index 362468b4b6d3..0530bb82ed2c 100644 --- a/src/test/expected/dry-run/main.rs +++ b/src/test/expected/dry-run/main.rs @@ -6,4 +6,4 @@ // `--dry-run` causes RMC to print out commands instead of running them // In `expected` you will find substrings of these commands because the // concrete paths depend on your working directory. -pub fn main() {} +fn main() {} diff --git a/src/test/expected/dynamic-error-trait/main.rs b/src/test/expected/dynamic-error-trait/main.rs index f92f63601cfc..59b368f47e26 100644 --- a/src/test/expected/dynamic-error-trait/main.rs +++ b/src/test/expected/dynamic-error-trait/main.rs @@ -23,7 +23,7 @@ impl MemoryMapping { } } -pub fn main() { +fn main() { let mm = MemoryMapping::new(2); if mm.is_ok() { let mm = mm.expect("foo"); diff --git a/src/test/expected/dynamic-trait-static-dispatch/main.rs b/src/test/expected/dynamic-trait-static-dispatch/main.rs index 501ac440d403..248b371729c0 100644 --- a/src/test/expected/dynamic-trait-static-dispatch/main.rs +++ b/src/test/expected/dynamic-trait-static-dispatch/main.rs @@ -20,7 +20,7 @@ impl Foo for Bar { } // this example works with static dispatch, so should work also while dynamic dispatch is not yet resolved -pub fn main() { +fn main() { let bar = Bar {}; assert!(bar.a() == 3); assert!(bar.b() == 5); diff --git a/src/test/expected/dynamic-trait/main.rs b/src/test/expected/dynamic-trait/main.rs index 18c2a33c1be8..9d4a89196e48 100644 --- a/src/test/expected/dynamic-trait/main.rs +++ b/src/test/expected/dynamic-trait/main.rs @@ -47,7 +47,7 @@ fn impl_area(a: impl Shape) -> u32 { a.area() } -pub fn main() { +fn main() { let rec = Rectangle { w: 10, h: 5 }; assert!(rec.vol(3) == 150); assert!(impl_area(rec.clone()) == 50); diff --git a/src/test/expected/enum/main.rs b/src/test/expected/enum/main.rs index 94847897672f..1b9e71ec2100 100644 --- a/src/test/expected/enum/main.rs +++ b/src/test/expected/enum/main.rs @@ -13,7 +13,7 @@ fn b() -> Foo { Foo::B { x: 30, y: 60.0 } } -pub fn main() { +fn main() { let x = a(); match x { Foo::A(x) => assert!(x == 10), diff --git a/src/test/expected/float-nan/main.rs b/src/test/expected/float-nan/main.rs index 4974bb77d1e5..4b6e27ce3e5e 100644 --- a/src/test/expected/float-nan/main.rs +++ b/src/test/expected/float-nan/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut f: f32 = 2.0; while f != 0.0 { f -= 1.0; diff --git a/src/test/expected/generics/main.rs b/src/test/expected/generics/main.rs index 30e01c1d842d..b8edeedf1fd2 100644 --- a/src/test/expected/generics/main.rs +++ b/src/test/expected/generics/main.rs @@ -13,7 +13,7 @@ fn wrapped(x: T) -> Foo { Foo { data: ident(x), i: 0 } } -pub fn main() { +fn main() { let x = 10; let y = wrapped(x); let z = 20.0; diff --git a/src/test/expected/iterator/main.rs b/src/test/expected/iterator/main.rs index 534672b83e55..0af1c28e6adb 100644 --- a/src/test/expected/iterator/main.rs +++ b/src/test/expected/iterator/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut z = 1; for i in 1..4 { z *= i; diff --git a/src/test/expected/niche/main.rs b/src/test/expected/niche/main.rs index e69d71a0e502..936b561fb06f 100644 --- a/src/test/expected/niche/main.rs +++ b/src/test/expected/niche/main.rs @@ -15,7 +15,7 @@ fn get_some<'a>(a: &'a i8) -> T<'a> { Option2::Some((*a, a)) } -pub fn main() { +fn main() { let x = get_opt(); match x { Option2::None => {} diff --git a/src/test/expected/niche2/main.rs b/src/test/expected/niche2/main.rs index 6558a81dc6c5..3c08a2c88e32 100644 --- a/src/test/expected/niche2/main.rs +++ b/src/test/expected/niche2/main.rs @@ -17,7 +17,7 @@ fn get_b() -> Option { Some(Foo::B([])) } -pub fn main() { +fn main() { match get_none() { None => {} Some(_) => assert!(false), diff --git a/src/test/expected/nondet/main.rs b/src/test/expected/nondet/main.rs index c715efc04ce9..e3e10e0c3a36 100644 --- a/src/test/expected/nondet/main.rs +++ b/src/test/expected/nondet/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x: i32 = rmc::nondet(); if (x > -500 && x < 500) { // x * x - 2 * x + 1 == 4 -> x == -1 || x == 3 diff --git a/src/test/expected/references/main.rs b/src/test/expected/references/main.rs index 70dffadea313..32592515bf32 100644 --- a/src/test/expected/references/main.rs +++ b/src/test/expected/references/main.rs @@ -11,7 +11,7 @@ impl Foo { } } -pub fn main() { +fn main() { let foo = Foo { a: 2, _b: 3.0 }; let z = foo.get_a(); assert!(z == 2); diff --git a/src/test/expected/slice/main.rs b/src/test/expected/slice/main.rs index d1858fae2ba6..a8a1d219c2c4 100644 --- a/src/test/expected/slice/main.rs +++ b/src/test/expected/slice/main.rs @@ -8,7 +8,7 @@ fn bar(x: &[i32; 5]) -> &[i32] { &x[1..4] } -pub fn main() { +fn main() { let x = [1, 2, 3, 4, 5]; let y = foo(&x); let z = bar(&x); diff --git a/src/test/expected/static-mutable-struct/main.rs b/src/test/expected/static-mutable-struct/main.rs index 3ef1b3d83d1b..963063136306 100644 --- a/src/test/expected/static-mutable-struct/main.rs +++ b/src/test/expected/static-mutable-struct/main.rs @@ -19,7 +19,7 @@ fn mutate_the_thing(nx: i64, ny: i32) { } } -pub fn main() { +fn main() { assert!(foo().x == 12); assert!(foo().y == 12); assert!(foo().x == 14); diff --git a/src/test/expected/static-mutable/main.rs b/src/test/expected/static-mutable/main.rs index 29da3e5f189e..6fbe66149fb8 100644 --- a/src/test/expected/static-mutable/main.rs +++ b/src/test/expected/static-mutable/main.rs @@ -12,7 +12,7 @@ fn mutate_the_thing(new: i32) { } } -pub fn main() { +fn main() { assert!(10 == foo()); assert!(12 == foo()); mutate_the_thing(10); diff --git a/src/test/expected/static/main.rs b/src/test/expected/static/main.rs index fcf1efe84d96..970b3b6df1a0 100644 --- a/src/test/expected/static/main.rs +++ b/src/test/expected/static/main.rs @@ -6,7 +6,7 @@ fn foo() -> i32 { X } -pub fn main() { +fn main() { assert!(10 == foo()); assert!(12 == foo()); } diff --git a/src/test/expected/test1/main.rs b/src/test/expected/test1/main.rs index 5c097ad1c7f6..e9b7ec7d74ec 100644 --- a/src/test/expected/test1/main.rs +++ b/src/test/expected/test1/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a: i32 = 0; let mut i: i32 = 10; while i != 0 { diff --git a/src/test/expected/test2/main.rs b/src/test/expected/test2/main.rs index 9d6a07de560a..935a08948e76 100644 --- a/src/test/expected/test2/main.rs +++ b/src/test/expected/test2/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a: i32 = 4; let mut i = 0; while a != 1 { diff --git a/src/test/expected/test3/main.rs b/src/test/expected/test3/main.rs index 5949d819ee85..04c18b308dee 100644 --- a/src/test/expected/test3/main.rs +++ b/src/test/expected/test3/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a: f32 = 0.0; let mut i = 10; diff --git a/src/test/expected/test4/main.rs b/src/test/expected/test4/main.rs index 86e80e89bc60..16ab5cf3e3e9 100644 --- a/src/test/expected/test4/main.rs +++ b/src/test/expected/test4/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a = 4; let mut i = 0; while a != 1 { diff --git a/src/test/expected/test5/main.rs b/src/test/expected/test5/main.rs index 86d87296dd57..a90eabbb7eb6 100644 --- a/src/test/expected/test5/main.rs +++ b/src/test/expected/test5/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { // should succeed assert!(div(4, 2) == 2); // should fail diff --git a/src/test/expected/test6/main.rs b/src/test/expected/test6/main.rs index ee3b96498d51..a5b86b5cbc02 100644 --- a/src/test/expected/test6/main.rs +++ b/src/test/expected/test6/main.rs @@ -4,7 +4,7 @@ fn add2(a: i32, b: i32) -> f32 { add(a, b as f32) } -pub fn main() { +fn main() { // should succeed: 1 + 1 = 2 assert!(add2(1, 1) == 2.0); // should fail: 2 + 1 = 3 diff --git a/src/test/expected/transmute/main.rs b/src/test/expected/transmute/main.rs index a49a6f9953a8..809f91c9050d 100644 --- a/src/test/expected/transmute/main.rs +++ b/src/test/expected/transmute/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let bitpattern = unsafe { std::mem::transmute::(1.0) }; assert!(bitpattern == 0x3F800000); diff --git a/src/test/expected/unwind_tip/main.rs b/src/test/expected/unwind_tip/main.rs index 20d1d8094cae..04bcef9c2d4a 100644 --- a/src/test/expected/unwind_tip/main.rs +++ b/src/test/expected/unwind_tip/main.rs @@ -10,7 +10,7 @@ // // In this test, we check that RMC warns the user about unwinding failures // and makes a recommendation to fix the issue. -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); if a < 1024 { diff --git a/src/test/expected/vec/main.rs b/src/test/expected/vec/main.rs index 7b241726344f..1cab83e0bfae 100644 --- a/src/test/expected/vec/main.rs +++ b/src/test/expected/vec/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut x: Vec = Vec::new(); x.push(10); assert!(x[0] == 10); diff --git a/src/test/expected/vecdq/main.rs b/src/test/expected/vecdq/main.rs index 74df92bcebc8..0e7d7f7ed3df 100644 --- a/src/test/expected/vecdq/main.rs +++ b/src/test/expected/vecdq/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::collections::VecDeque; -pub fn main() { +fn main() { let x = rmc::nondet(); let y = rmc::nondet(); let mut q: VecDeque = VecDeque::new(); diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index dc62555aa83a..c6384023786f 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -322,7 +322,7 @@ fn is_nonzero_pow2(x: u16) -> bool { unsafe { (x != 0) && ((x & (x - 1)) == 0) } } -pub fn main() { +fn main() { let mem = GuestMemoryMmap {}; let queue_size: u16 = rmc::nondet(); if !is_nonzero_pow2(queue_size) { diff --git a/src/test/prusti/100_doors.rs b/src/test/prusti/100_doors.rs index ddfda6bd35aa..86b234050276 100644 --- a/src/test/prusti/100_doors.rs +++ b/src/test/prusti/100_doors.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut door_open = [false; 10]; for pass in 1..11 { let mut door = pass; diff --git a/src/test/prusti/Ackermann_function.rs b/src/test/prusti/Ackermann_function.rs index c87c19c76bbf..b48da7f3ecb0 100644 --- a/src/test/prusti/Ackermann_function.rs +++ b/src/test/prusti/Ackermann_function.rs @@ -8,7 +8,7 @@ fn ack(m: u64, n: u64) -> u64 { } } -pub fn main() { +fn main() { let a = ack(2, 4); assert!(a == 11); } diff --git a/src/test/prusti/Binary_search.rs b/src/test/prusti/Binary_search.rs index 054c87c3bdf9..ae1f8ff8823d 100644 --- a/src/test/prusti/Binary_search.rs +++ b/src/test/prusti/Binary_search.rs @@ -47,7 +47,7 @@ fn get() -> [i32; 11] { [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] } -pub fn main() { +fn main() { let x = get(); let y = rmc::nondet(); if 1 <= y && y <= 11 { diff --git a/src/test/prusti/Fibonacci_sequence.rs b/src/test/prusti/Fibonacci_sequence.rs index bebe0c3198fa..67dd22e2dd9c 100644 --- a/src/test/prusti/Fibonacci_sequence.rs +++ b/src/test/prusti/Fibonacci_sequence.rs @@ -21,7 +21,7 @@ impl Iterator for Fib { } } -pub fn main() { +fn main() { let mut fib = Fib::new(); assert!(fib.nth(10).unwrap() == 55); } diff --git a/src/test/prusti/Heapsort.rs b/src/test/prusti/Heapsort.rs index e31827ac3c75..82891beb32ab 100644 --- a/src/test/prusti/Heapsort.rs +++ b/src/test/prusti/Heapsort.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut v = [3, 0, 1, 2]; create_heap(&mut v, |x, y| x < y); assert!(v == [3, 2, 1, 0]); diff --git a/src/test/prusti/Selection_sort.rs b/src/test/prusti/Selection_sort.rs index da619505b644..16e563190f82 100644 --- a/src/test/prusti/Selection_sort.rs +++ b/src/test/prusti/Selection_sort.rs @@ -18,7 +18,7 @@ fn selection_sort(array: &mut [i32]) { } } -pub fn main() { +fn main() { let mut array = [9, 4, 8, 3]; selection_sort(&mut array); assert!(array == [3, 4, 8, 9]); diff --git a/src/test/prusti/Tower_of_Hanoi.rs b/src/test/prusti/Tower_of_Hanoi.rs index c4d32bc45915..464f8115f194 100644 --- a/src/test/prusti/Tower_of_Hanoi.rs +++ b/src/test/prusti/Tower_of_Hanoi.rs @@ -7,6 +7,6 @@ fn move_(n: i32, from: i32, to: i32, via: i32) { } } -pub fn main() { +fn main() { move_(4, 1, 2, 3); } diff --git a/src/test/prusti/borrow_first.rs b/src/test/prusti/borrow_first.rs index f3fce885b585..c6802384758e 100644 --- a/src/test/prusti/borrow_first.rs +++ b/src/test/prusti/borrow_first.rs @@ -14,7 +14,7 @@ fn foo(vec: &mut Vec) -> &i32 { &vec[last] } -pub fn main() { +fn main() { let mut v = vec![-1, 2, 3]; let r = foo(&mut v); assert!(*r > 0); diff --git a/src/test/rmc/ArithEqualOperators/main.rs b/src/test/rmc/ArithEqualOperators/main.rs index 755aaf7a834c..3b8fa3798a68 100644 --- a/src/test/rmc/ArithEqualOperators/main.rs +++ b/src/test/rmc/ArithEqualOperators/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); a /= 2; let mut b: u32 = rmc::nondet(); diff --git a/src/test/rmc/Asm/main_fixme.rs b/src/test/rmc/Asm/main_fixme.rs index cfd1c7cf3d86..087df7806b06 100644 --- a/src/test/rmc/Asm/main_fixme.rs +++ b/src/test/rmc/Asm/main_fixme.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(asm)] -pub fn main() { +fn main() { unsafe { asm!("nop"); } diff --git a/src/test/rmc/Assert/UninitValid/fixme_main.rs b/src/test/rmc/Assert/UninitValid/fixme_main.rs index f685607d38cc..06c24dee9d53 100644 --- a/src/test/rmc/Assert/UninitValid/fixme_main.rs +++ b/src/test/rmc/Assert/UninitValid/fixme_main.rs @@ -4,7 +4,7 @@ use std::mem::{self, MaybeUninit}; -pub fn main() { +fn main() { // The compiler assumes that variables are properly initialized according to // the requirements of the variable's type (e.g., a variable of reference // type must be aligned and non-NULL). This is an invariant that must always diff --git a/src/test/rmc/Assert/ZeroValid/fixme_main.rs b/src/test/rmc/Assert/ZeroValid/fixme_main.rs index e767ecafe13d..805173c08f7d 100644 --- a/src/test/rmc/Assert/ZeroValid/fixme_main.rs +++ b/src/test/rmc/Assert/ZeroValid/fixme_main.rs @@ -7,7 +7,7 @@ use std::mem; use std::ptr; -pub fn main() { +fn main() { let x: &mut i32 = unsafe { mem::zeroed() }; //< undefined (should fail) let p: *mut i32 = x; assert!(p == ptr::null_mut()); //< verifies with RMC diff --git a/src/test/rmc/Assert/ZeroValid/main.rs b/src/test/rmc/Assert/ZeroValid/main.rs index 5522c55eec09..cd374d2cb8dd 100644 --- a/src/test/rmc/Assert/ZeroValid/main.rs +++ b/src/test/rmc/Assert/ZeroValid/main.rs @@ -18,7 +18,7 @@ fn do_test(init: T, expected: T) { assert!(expected == x); } -pub fn main() { +fn main() { do_test::(true, false); do_test::(-42, 0); do_test::(-42, 0); diff --git a/src/test/rmc/Assume/main.rs b/src/test/rmc/Assume/main.rs index 802905d01b9e..2e4b91c45431 100644 --- a/src/test/rmc/Assume/main.rs +++ b/src/test/rmc/Assume/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let i: i32 = rmc::nondet(); rmc::assume(i < 10); assert!(i < 20); diff --git a/src/test/rmc/Assume/main_fail.rs b/src/test/rmc/Assume/main_fail.rs index 3882f1f897b0..709500cd9ba1 100644 --- a/src/test/rmc/Assume/main_fail.rs +++ b/src/test/rmc/Assume/main_fail.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let i: i32 = rmc::nondet(); rmc::assume(i < 10); rmc::expect_fail(i > 20, "Blocked by assumption above."); diff --git a/src/test/rmc/Atomics/Stable/CompareExchange/main.rs b/src/test/rmc/Atomics/Stable/CompareExchange/main.rs index e65f1319424f..b902edc65e12 100644 --- a/src/test/rmc/Atomics/Stable/CompareExchange/main.rs +++ b/src/test/rmc/Atomics/Stable/CompareExchange/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // pub fn compare_exchange( // &self, // current: bool, diff --git a/src/test/rmc/Atomics/Stable/Exchange/main.rs b/src/test/rmc/Atomics/Stable/Exchange/main.rs index 9aeba57c44a1..92755b04ea0d 100644 --- a/src/test/rmc/Atomics/Stable/Exchange/main.rs +++ b/src/test/rmc/Atomics/Stable/Exchange/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { let a1 = AtomicBool::new(true); let a2 = AtomicBool::new(true); let a3 = AtomicBool::new(true); diff --git a/src/test/rmc/Atomics/Stable/Fence/main.rs b/src/test/rmc/Atomics/Stable/Fence/main.rs index 5ebfc2da96b7..fc91b9cd7533 100644 --- a/src/test/rmc/Atomics/Stable/Fence/main.rs +++ b/src/test/rmc/Atomics/Stable/Fence/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{fence, Ordering}; -pub fn main() { +fn main() { // pub fn fence(order: Ordering) // An atomic fence. // Depending on the specified order, a fence prevents the compiler diff --git a/src/test/rmc/Atomics/Stable/FetchAdd/main.rs b/src/test/rmc/Atomics/Stable/FetchAdd/main.rs index b30e1640c29d..e2e3ed7abdc3 100644 --- a/src/test/rmc/Atomics/Stable/FetchAdd/main.rs +++ b/src/test/rmc/Atomics/Stable/FetchAdd/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicIsize, Ordering}; -pub fn main() { +fn main() { // pub fn fetch_add(&self, val: isize, order: Ordering) -> isize // Adds to the current value, returning the previous value. let a1 = AtomicIsize::new(0); diff --git a/src/test/rmc/Atomics/Stable/FetchAnd/main.rs b/src/test/rmc/Atomics/Stable/FetchAnd/main.rs index 3c59da5463c5..dc1efa71a29f 100644 --- a/src/test/rmc/Atomics/Stable/FetchAnd/main.rs +++ b/src/test/rmc/Atomics/Stable/FetchAnd/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // pub fn fetch_and(&self, val: bool, order: Ordering) -> bool // Performs a logical "and" operation on the current value and // the argument val, and sets the new value to the result. diff --git a/src/test/rmc/Atomics/Stable/FetchOr/main.rs b/src/test/rmc/Atomics/Stable/FetchOr/main.rs index 3a210b3e1a76..c256a23f5024 100644 --- a/src/test/rmc/Atomics/Stable/FetchOr/main.rs +++ b/src/test/rmc/Atomics/Stable/FetchOr/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // pub fn fetch_or(&self, val: bool, order: Ordering) -> bool // Performs a logical "or" operation on the current value and // the argument val, and sets the new value to the result. diff --git a/src/test/rmc/Atomics/Stable/FetchSub/main.rs b/src/test/rmc/Atomics/Stable/FetchSub/main.rs index c37e8a7e7fa2..09e2c4dfaefb 100644 --- a/src/test/rmc/Atomics/Stable/FetchSub/main.rs +++ b/src/test/rmc/Atomics/Stable/FetchSub/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicIsize, Ordering}; -pub fn main() { +fn main() { // pub fn fetch_sub(&self, val: isize, order: Ordering) -> isize // Subtracts from the current value, returning the previous value. let a1 = AtomicIsize::new(1); diff --git a/src/test/rmc/Atomics/Stable/FetchXor/main.rs b/src/test/rmc/Atomics/Stable/FetchXor/main.rs index 904b1608192a..431fc6d458ed 100644 --- a/src/test/rmc/Atomics/Stable/FetchXor/main.rs +++ b/src/test/rmc/Atomics/Stable/FetchXor/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // pub fn fetch_xor(&self, val: bool, order: Ordering) -> bool // Performs a bitwise "xor" operation on the current value and // the argument val, and sets the new value to the result. diff --git a/src/test/rmc/Atomics/Stable/Load/main.rs b/src/test/rmc/Atomics/Stable/Load/main.rs index b19884053b74..7a9d41a8bef1 100644 --- a/src/test/rmc/Atomics/Stable/Load/main.rs +++ b/src/test/rmc/Atomics/Stable/Load/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // pub fn load(&self, order: Ordering) -> bool // Loads a value from the bool. // load takes an Ordering argument which describes the memory ordering diff --git a/src/test/rmc/Atomics/Stable/Store/main.rs b/src/test/rmc/Atomics/Stable/Store/main.rs index 43a71917f7d1..b2dd70d4b5f1 100644 --- a/src/test/rmc/Atomics/Stable/Store/main.rs +++ b/src/test/rmc/Atomics/Stable/Store/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::sync::atomic::{AtomicBool, Ordering}; -pub fn main() { +fn main() { // ppub fn store(&self, val: bool, order: Ordering) // Stores a value into the bool. // store takes an Ordering argument which describes the memory ordering diff --git a/src/test/rmc/Atomics/Unstable/AtomicAdd/main.rs b/src/test/rmc/Atomics/Unstable/AtomicAdd/main.rs index 4784b4a16d2f..49605328173b 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicAdd/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicAdd/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_xadd, atomic_xadd_acq, atomic_xadd_acqrel, atomic_xadd_rel, atomic_xadd_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 0 as u8; let mut a2 = 0 as u8; let mut a3 = 0 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicAnd/main.rs b/src/test/rmc/Atomics/Unstable/AtomicAnd/main.rs index cc9c36e2256b..7fe894f9b894 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicAnd/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicAnd/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_and, atomic_and_acq, atomic_and_acqrel, atomic_and_rel, atomic_and_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 1 as u8; let mut a2 = 1 as u8; let mut a3 = 1 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicCxchg/main.rs b/src/test/rmc/Atomics/Unstable/AtomicCxchg/main.rs index 426fa2e13a66..d1e32e3f11c9 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicCxchg/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicCxchg/main.rs @@ -7,7 +7,7 @@ use std::intrinsics::{ atomic_cxchg_rel, atomic_cxchg_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 0 as u8; let mut a2 = 0 as u8; let mut a3 = 0 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicFence/main.rs b/src/test/rmc/Atomics/Unstable/AtomicFence/main.rs index 90605838e775..5203b3dc9876 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicFence/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicFence/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{atomic_fence, atomic_fence_acq, atomic_fence_acqrel, atomic_fence_rel}; -pub fn main() { +fn main() { unsafe { atomic_fence(); atomic_fence_acq(); diff --git a/src/test/rmc/Atomics/Unstable/AtomicLoad/main.rs b/src/test/rmc/Atomics/Unstable/AtomicLoad/main.rs index ce0004e2d897..dcde0f430b32 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicLoad/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicLoad/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{atomic_load, atomic_load_acq, atomic_load_relaxed}; -pub fn main() { +fn main() { let a1 = 1 as u8; let a2 = 1 as u8; let a3 = 1 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicOr/main.rs b/src/test/rmc/Atomics/Unstable/AtomicOr/main.rs index a233b5f6613d..f7e5a289105f 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicOr/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicOr/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_or, atomic_or_acq, atomic_or_acqrel, atomic_or_rel, atomic_or_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 1 as u8; let mut a2 = 1 as u8; let mut a3 = 1 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicStore/main.rs b/src/test/rmc/Atomics/Unstable/AtomicStore/main.rs index 8993eb69ee46..ada3f81b88c3 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicStore/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicStore/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{atomic_store, atomic_store_rel, atomic_store_relaxed}; -pub fn main() { +fn main() { let mut a1 = 1 as u8; let mut a2 = 1 as u8; let mut a3 = 1 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicSub/main.rs b/src/test/rmc/Atomics/Unstable/AtomicSub/main.rs index b9b0540d402d..41d2b51edda1 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicSub/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicSub/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_xsub, atomic_xsub_acq, atomic_xsub_acqrel, atomic_xsub_rel, atomic_xsub_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 1 as u8; let mut a2 = 1 as u8; let mut a3 = 1 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicXchg/main.rs b/src/test/rmc/Atomics/Unstable/AtomicXchg/main.rs index 08faca314b1e..92fc0fc752af 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicXchg/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicXchg/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_xchg, atomic_xchg_acq, atomic_xchg_acqrel, atomic_xchg_rel, atomic_xchg_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 0 as u8; let mut a2 = 0 as u8; let mut a3 = 0 as u8; diff --git a/src/test/rmc/Atomics/Unstable/AtomicXor/main.rs b/src/test/rmc/Atomics/Unstable/AtomicXor/main.rs index 0502b6ec37cc..c129cd2a8c6e 100644 --- a/src/test/rmc/Atomics/Unstable/AtomicXor/main.rs +++ b/src/test/rmc/Atomics/Unstable/AtomicXor/main.rs @@ -5,7 +5,7 @@ use std::intrinsics::{ atomic_xor, atomic_xor_acq, atomic_xor_acqrel, atomic_xor_rel, atomic_xor_relaxed, }; -pub fn main() { +fn main() { let mut a1 = 1 as u8; let mut a2 = 1 as u8; let mut a3 = 1 as u8; diff --git a/src/test/rmc/BinOp_Offset/main.rs b/src/test/rmc/BinOp_Offset/main.rs index 98b44168eaed..a1ecd895a5e9 100644 --- a/src/test/rmc/BinOp_Offset/main.rs +++ b/src/test/rmc/BinOp_Offset/main.rs @@ -22,7 +22,7 @@ pub fn test_offset_str() { } } -pub fn main() { +fn main() { test_offset_array(); test_offset_str() } diff --git a/src/test/rmc/BinOp_Offset/main_fail.rs b/src/test/rmc/BinOp_Offset/main_fail.rs index 0319aa81c2a1..0d99d452f218 100644 --- a/src/test/rmc/BinOp_Offset/main_fail.rs +++ b/src/test/rmc/BinOp_Offset/main_fail.rs @@ -5,9 +5,9 @@ pub fn test_offset_in_double_array() { //let table: Vec> = Vec::with_capacity(1); let table: [[u64; 1]; 1] = [[rmc::nondet::()]]; - table[0][rmc::nondet::()]; // EXPCECTED FAIL + table[0][rmc::nondet::()]; // EXPECTED FAIL } -pub fn main() { +fn main() { test_offset_in_double_array(); } diff --git a/src/test/rmc/BitManipulation/Stable/fixme_main.rs b/src/test/rmc/BitManipulation/Stable/fixme_main.rs index 6f08774c23b8..928572cc1c2c 100644 --- a/src/test/rmc/BitManipulation/Stable/fixme_main.rs +++ b/src/test/rmc/BitManipulation/Stable/fixme_main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-verify-fail -pub fn main() { +fn main() { // Intrinsics implemented as integer primitives // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html // https://doc.rust-lang.org/core/intrinsics/fn.ctlz.html diff --git a/src/test/rmc/BitManipulation/Unstable/Rotate/main.rs b/src/test/rmc/BitManipulation/Unstable/Rotate/main.rs index 775cb88e9943..bd35a2f9a38c 100644 --- a/src/test/rmc/BitManipulation/Unstable/Rotate/main.rs +++ b/src/test/rmc/BitManipulation/Unstable/Rotate/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{rotate_left, rotate_right}; -pub fn main() { +fn main() { let vl8 = 0b0011_1000_u8; let vl16 = 0b0011_1000_0000_0000_u16; let vl32 = 0b0011_1000_0000_0000_0000_0000_0000_0000_u32; diff --git a/src/test/rmc/BitManipulation/Unstable/fixme_main.rs b/src/test/rmc/BitManipulation/Unstable/fixme_main.rs index 1b4c62f76673..b892b70121e0 100644 --- a/src/test/rmc/BitManipulation/Unstable/fixme_main.rs +++ b/src/test/rmc/BitManipulation/Unstable/fixme_main.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{ctlz, cttz, cttz_nonzero}; -pub fn main() { +fn main() { let v8 = 0b0011_1000_u8; let v16 = 0b0011_1000_0000_0000_u16; let v32 = 0b0011_1000_0000_0000_0000_0000_0000_0000_u32; diff --git a/src/test/rmc/BitwiseArithOperators/bool.rs b/src/test/rmc/BitwiseArithOperators/bool.rs index 3a9c2165f06c..f5311d95898b 100644 --- a/src/test/rmc/BitwiseArithOperators/bool.rs +++ b/src/test/rmc/BitwiseArithOperators/bool.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: bool = rmc::nondet(); let b: bool = rmc::nondet(); let c = a ^ b; diff --git a/src/test/rmc/BitwiseArithOperators/main.rs b/src/test/rmc/BitwiseArithOperators/main.rs index 13d7c34f0599..6288a8f881c9 100644 --- a/src/test/rmc/BitwiseArithOperators/main.rs +++ b/src/test/rmc/BitwiseArithOperators/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { assert!(3 | 5 == 7); assert!(7 & 9 == 1); assert!(9 ^ 7 == 14); diff --git a/src/test/rmc/BitwiseEqualOperators/main.rs b/src/test/rmc/BitwiseEqualOperators/main.rs index 728c17f8492e..7319e235d0a8 100644 --- a/src/test/rmc/BitwiseEqualOperators/main.rs +++ b/src/test/rmc/BitwiseEqualOperators/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut x = 0; x |= 1; assert!(x == 1); diff --git a/src/test/rmc/BitwiseShiftOperators/Usize/main.rs b/src/test/rmc/BitwiseShiftOperators/Usize/main.rs index 4d15b7945410..59bcd22b1058 100644 --- a/src/test/rmc/BitwiseShiftOperators/Usize/main.rs +++ b/src/test/rmc/BitwiseShiftOperators/Usize/main.rs @@ -5,7 +5,7 @@ fn bitmap_new(byte_size: usize, page_size: usize) -> usize { let map_size = ((bit_size - 1) >> 6) + 1; map_size } -pub fn main() { +fn main() { let map_size = bitmap_new(1024, 128); assert!(map_size == 1); } diff --git a/src/test/rmc/BitwiseShiftOperators/main.rs b/src/test/rmc/BitwiseShiftOperators/main.rs index 18f2e6519b74..984c4dde4b64 100644 --- a/src/test/rmc/BitwiseShiftOperators/main.rs +++ b/src/test/rmc/BitwiseShiftOperators/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { assert!(8 >> 4 == 0); assert!(1 << 4 == 16); diff --git a/src/test/rmc/Bool-BoolOperators/main.rs b/src/test/rmc/Bool-BoolOperators/main.rs index eae78f75247f..ba1cf37a5c93 100644 --- a/src/test/rmc/Bool-BoolOperators/main.rs +++ b/src/test/rmc/Bool-BoolOperators/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { assert!(true); assert!(true || false); assert!(!false); diff --git a/src/test/rmc/Cast/cast_abstract_args_to_concrete.rs b/src/test/rmc/Cast/cast_abstract_args_to_concrete.rs index 705581664af7..2813d6cf6e86 100644 --- a/src/test/rmc/Cast/cast_abstract_args_to_concrete.rs +++ b/src/test/rmc/Cast/cast_abstract_args_to_concrete.rs @@ -22,7 +22,7 @@ extern crate libc; use std::mem; -pub fn main() { +fn main() { let _x32 = 1.0f32.powi(2); let _x64 = 1.0f64.powi(2); diff --git a/src/test/rmc/Cast/from_be_bytes.rs b/src/test/rmc/Cast/from_be_bytes.rs index 80193919cd65..8d5f4c5bb4f4 100644 --- a/src/test/rmc/Cast/from_be_bytes.rs +++ b/src/test/rmc/Cast/from_be_bytes.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT use std::convert::TryInto; -pub fn main() { +fn main() { let input: &[u8] = &vec![ rmc::nondet(), rmc::nondet(), diff --git a/src/test/rmc/Cast/main.rs b/src/test/rmc/Cast/main.rs index f82348e9e923..a018f658a01a 100644 --- a/src/test/rmc/Cast/main.rs +++ b/src/test/rmc/Cast/main.rs @@ -5,7 +5,7 @@ pub enum Level { Error, } -pub fn main() { +fn main() { let left = Level::Error; assert!((left as u8).cmp(&0) == Ordering::Equal); } diff --git a/src/test/rmc/Cast/path.rs b/src/test/rmc/Cast/path.rs index 87b5150e5cb9..0c66d1d1e405 100644 --- a/src/test/rmc/Cast/path.rs +++ b/src/test/rmc/Cast/path.rs @@ -2,6 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::path::Path; -pub fn main() { +fn main() { let path = Path::new("./foo/bar.txt"); } diff --git a/src/test/rmc/Closure/main.rs b/src/test/rmc/Closure/main.rs index 3aa9675efe0b..4826b716c2d8 100644 --- a/src/test/rmc/Closure/main.rs +++ b/src/test/rmc/Closure/main.rs @@ -38,7 +38,7 @@ fn test_env() { assert!(r == 9); } -pub fn main() { +fn main() { closure_with_empty_args(); closure_with_1_arg(); test_three_args(); diff --git a/src/test/rmc/CodegenConstValue/bigints.rs b/src/test/rmc/CodegenConstValue/bigints.rs index 2788de6ac20a..0e79f39b3fe2 100644 --- a/src/test/rmc/CodegenConstValue/bigints.rs +++ b/src/test/rmc/CodegenConstValue/bigints.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x: u128 = u128::MAX; let x2: u128 = { // u128::MAX = 2^128 - 1; diff --git a/src/test/rmc/CodegenConstValue/main.rs b/src/test/rmc/CodegenConstValue/main.rs index 1762a5f8bc97..c64ec0fc2996 100644 --- a/src/test/rmc/CodegenConstValue/main.rs +++ b/src/test/rmc/CodegenConstValue/main.rs @@ -8,7 +8,7 @@ // [main.pointer_dereference.5] line 16 dereference failure: pointer outside object bounds in *lut_ptr: FAILURE // Tracking issue: https://github.com/model-checking/rmc/issues/307 const DEC_DIGITS_LUT: &'static [u8] = b"ab"; -pub fn main() { +fn main() { // The next two assertions don't go through to CBMC // 'cos they're constant folded away assert!(DEC_DIGITS_LUT[0] == b'a'); diff --git a/src/test/rmc/CodegenConstValue/u128.rs b/src/test/rmc/CodegenConstValue/u128.rs index ef581c5c73c1..0d83656a2383 100644 --- a/src/test/rmc/CodegenConstValue/u128.rs +++ b/src/test/rmc/CodegenConstValue/u128.rs @@ -6,6 +6,6 @@ fn assert_bigger(a: u128, b: u128) { assert!(a > b); } -pub fn main() { +fn main() { assert_bigger(u128::MAX, 12); } diff --git a/src/test/rmc/CodegenMisc/main.rs b/src/test/rmc/CodegenMisc/main.rs index f99326104b81..532a06bd32c2 100644 --- a/src/test/rmc/CodegenMisc/main.rs +++ b/src/test/rmc/CodegenMisc/main.rs @@ -12,7 +12,7 @@ pub type SignalHandler = extern "C" fn(num: c_int, _unused: *mut c_void) -> (); extern "C" fn handle_signal(_: c_int, _: *mut c_void) {} -pub fn main() { +fn main() { let x = handle_signal as *const () as usize; assert!(x != 0); } diff --git a/src/test/rmc/CodegenStatic/main.rs b/src/test/rmc/CodegenStatic/main.rs index bc88c60f91b7..e7b25f580dc2 100644 --- a/src/test/rmc/CodegenStatic/main.rs +++ b/src/test/rmc/CodegenStatic/main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT static STATIC: [&str; 1] = ["FOO"]; -pub fn main() { +fn main() { let x = STATIC[0]; let bytes = x.as_bytes(); assert!(bytes.len() == 3); diff --git a/src/test/rmc/CodegenStatic/struct.rs b/src/test/rmc/CodegenStatic/struct.rs index 3b89073af3fa..ecfad3095705 100644 --- a/src/test/rmc/CodegenStatic/struct.rs +++ b/src/test/rmc/CodegenStatic/struct.rs @@ -7,6 +7,6 @@ pub struct Foo { const x: Foo<3> = Foo { bytes: [1, 2, 3] }; -pub fn main() { +fn main() { assert!(x.bytes[0] == 1); } diff --git a/src/test/rmc/CopyIntrinsics/main.rs b/src/test/rmc/CopyIntrinsics/main.rs index 26d2133d4ec1..e12348ad2135 100644 --- a/src/test/rmc/CopyIntrinsics/main.rs +++ b/src/test/rmc/CopyIntrinsics/main.rs @@ -87,7 +87,7 @@ fn test_swap() { assert!(y == 12); } -pub fn main() { +fn main() { test_copy(); test_swap(); test_append(); diff --git a/src/test/rmc/Count/Unstable/Ctlz/bounds.rs b/src/test/rmc/Count/Unstable/Ctlz/bounds.rs index 6831d6f7c555..7db52aa63ab6 100644 --- a/src/test/rmc/Count/Unstable/Ctlz/bounds.rs +++ b/src/test/rmc/Count/Unstable/Ctlz/bounds.rs @@ -6,7 +6,7 @@ #![feature(core_intrinsics)] use std::intrinsics::ctlz_nonzero; -pub fn main() { +fn main() { let uv8: u8 = 0; let uv16: u16 = 0; let uv32: u32 = 0; diff --git a/src/test/rmc/Count/Unstable/Ctlz/main.rs b/src/test/rmc/Count/Unstable/Ctlz/main.rs index ad1200608907..2cb1b2c85224 100644 --- a/src/test/rmc/Count/Unstable/Ctlz/main.rs +++ b/src/test/rmc/Count/Unstable/Ctlz/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{ctlz, ctlz_nonzero}; -pub fn main() { +fn main() { let uv8 = 0b0011_1000_u8; let uv16 = uv8 as u16; let uv32 = uv8 as u32; diff --git a/src/test/rmc/Count/Unstable/Cttz/bounds.rs b/src/test/rmc/Count/Unstable/Cttz/bounds.rs index ff926996fc20..0327087efa1a 100644 --- a/src/test/rmc/Count/Unstable/Cttz/bounds.rs +++ b/src/test/rmc/Count/Unstable/Cttz/bounds.rs @@ -6,7 +6,7 @@ #![feature(core_intrinsics)] use std::intrinsics::cttz_nonzero; -pub fn main() { +fn main() { let uv8: u8 = 0; let uv16: u16 = 0; let uv32: u32 = 0; diff --git a/src/test/rmc/Count/Unstable/Cttz/main.rs b/src/test/rmc/Count/Unstable/Cttz/main.rs index 8e25a9542c81..bec85ccdd99c 100644 --- a/src/test/rmc/Count/Unstable/Cttz/main.rs +++ b/src/test/rmc/Count/Unstable/Cttz/main.rs @@ -3,7 +3,7 @@ #![feature(core_intrinsics)] use std::intrinsics::{cttz, cttz_nonzero}; -pub fn main() { +fn main() { let uv8 = 0b0011_1000_u8; let uv16 = uv8 as u16; let uv32 = uv8 as u32; diff --git a/src/test/rmc/DynTrait/any_cast_int.rs b/src/test/rmc/DynTrait/any_cast_int.rs index ad357db685f3..032c55f2b06d 100644 --- a/src/test/rmc/DynTrait/any_cast_int.rs +++ b/src/test/rmc/DynTrait/any_cast_int.rs @@ -25,7 +25,7 @@ fn downcast_to_fewer_traits(s: &(dyn Any + Send)) { downcast_to_concrete(c); } -pub fn main() { +fn main() { let i: i32 = 7; downcast_to_fewer_traits(&i); } diff --git a/src/test/rmc/DynTrait/any_cast_int_fail.rs b/src/test/rmc/DynTrait/any_cast_int_fail.rs index e1852d20bc99..8a3469d7892a 100644 --- a/src/test/rmc/DynTrait/any_cast_int_fail.rs +++ b/src/test/rmc/DynTrait/any_cast_int_fail.rs @@ -26,7 +26,7 @@ fn downcast_to_fewer_traits(s: &(dyn Any + Send)) { downcast_to_concrete(c); } -pub fn main() { +fn main() { let i: i32 = 7; downcast_to_fewer_traits(&i); } diff --git a/src/test/rmc/DynTrait/boxed_closure.rs b/src/test/rmc/DynTrait/boxed_closure.rs index 51dc7a71156b..8ef183cbbe8f 100644 --- a/src/test/rmc/DynTrait/boxed_closure.rs +++ b/src/test/rmc/DynTrait/boxed_closure.rs @@ -3,7 +3,7 @@ // Check that we can codegen a boxed dyn closure -pub fn main() { +fn main() { // Create a boxed once-callable closure let f: Box = Box::new(|x, y| { assert!(x == 1.0); diff --git a/src/test/rmc/DynTrait/boxed_closure_fail.rs b/src/test/rmc/DynTrait/boxed_closure_fail.rs index 7d27d100104a..fb36e96c1b39 100644 --- a/src/test/rmc/DynTrait/boxed_closure_fail.rs +++ b/src/test/rmc/DynTrait/boxed_closure_fail.rs @@ -3,7 +3,7 @@ // rmc-verify-fail // Check that we can codegen a boxed dyn closure and fail an inner assertion -pub fn main() { +fn main() { // Create a boxed once-callable closure let f: Box = Box::new(|x| { rmc::expect_fail(x == 2, "Wrong int"); diff --git a/src/test/rmc/DynTrait/boxed_debug_cast.rs b/src/test/rmc/DynTrait/boxed_debug_cast.rs index 57c3737af201..2cd7dc0b0fa3 100644 --- a/src/test/rmc/DynTrait/boxed_debug_cast.rs +++ b/src/test/rmc/DynTrait/boxed_debug_cast.rs @@ -22,7 +22,7 @@ fn f<'a>(x: &'a &Box) -> Box<&'a dyn Debug> { Box::new(d) } -pub fn main() { +fn main() { let c = Concrete {}; let x = Box::new(c) as Box; let d = f(&&x); diff --git a/src/test/rmc/DynTrait/boxed_trait.rs b/src/test/rmc/DynTrait/boxed_trait.rs index 8e0e06cf53c5..0d03b5bac1a1 100644 --- a/src/test/rmc/DynTrait/boxed_trait.rs +++ b/src/test/rmc/DynTrait/boxed_trait.rs @@ -43,7 +43,7 @@ fn do_area_box(x: Box) -> u32 { x.area() } -pub fn main() { +fn main() { let rec = Box::new(Rectangle { w: 10, h: 5 }); assert!(rec.vol(3) == 150); assert!(do_vol(&*rec, 2) == 100); diff --git a/src/test/rmc/DynTrait/boxed_trait_fail.rs b/src/test/rmc/DynTrait/boxed_trait_fail.rs index 9a40000f8ac8..9e690ef063eb 100644 --- a/src/test/rmc/DynTrait/boxed_trait_fail.rs +++ b/src/test/rmc/DynTrait/boxed_trait_fail.rs @@ -45,7 +45,7 @@ fn do_area_box(x: Box) -> u32 { x.area() } -pub fn main() { +fn main() { let rec = Box::new(Rectangle { w: 10, h: 5 }); assert!(rec.vol(3) != 150); assert!(do_vol(&*rec, 2) != 100); diff --git a/src/test/rmc/DynTrait/different_crates.rs b/src/test/rmc/DynTrait/different_crates.rs index d944a596621c..396659289a89 100644 --- a/src/test/rmc/DynTrait/different_crates.rs +++ b/src/test/rmc/DynTrait/different_crates.rs @@ -42,7 +42,7 @@ fn weird_count(c: &mut dyn Iterator) -> usize { c.next().unwrap() } -pub fn main() { +fn main() { 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); diff --git a/src/test/rmc/DynTrait/different_crates_fail.rs b/src/test/rmc/DynTrait/different_crates_fail.rs index 1a8e1345e7c0..3b7c47fe2338 100644 --- a/src/test/rmc/DynTrait/different_crates_fail.rs +++ b/src/test/rmc/DynTrait/different_crates_fail.rs @@ -43,7 +43,7 @@ fn weird_count(c: &mut dyn Iterator) -> usize { c.next().unwrap() } -pub fn main() { +fn main() { 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 diff --git a/src/test/rmc/DynTrait/drop_boxed_dyn.rs b/src/test/rmc/DynTrait/drop_boxed_dyn.rs index 63e3e04cd051..7046ef5f9914 100644 --- a/src/test/rmc/DynTrait/drop_boxed_dyn.rs +++ b/src/test/rmc/DynTrait/drop_boxed_dyn.rs @@ -33,7 +33,7 @@ impl Drop for Concrete2 { } } -pub fn main() { +fn main() { { let x: Box; if rmc::nondet() { diff --git a/src/test/rmc/DynTrait/drop_concrete.rs b/src/test/rmc/DynTrait/drop_concrete.rs index 3ae71a97726f..78634b0d08b7 100644 --- a/src/test/rmc/DynTrait/drop_concrete.rs +++ b/src/test/rmc/DynTrait/drop_concrete.rs @@ -15,7 +15,7 @@ impl Drop for Concrete1 { } } -pub fn main() { +fn main() { { let _x1 = Concrete1 {}; } diff --git a/src/test/rmc/DynTrait/drop_dyn_pointer.rs b/src/test/rmc/DynTrait/drop_dyn_pointer.rs index 96afb19907fa..b015c3078c2a 100644 --- a/src/test/rmc/DynTrait/drop_dyn_pointer.rs +++ b/src/test/rmc/DynTrait/drop_dyn_pointer.rs @@ -33,7 +33,7 @@ impl Drop for Concrete2 { } } -pub fn main() { +fn main() { { let _x1: &dyn T = &Concrete1 {}; } diff --git a/src/test/rmc/DynTrait/drop_nested_boxed_dyn.rs b/src/test/rmc/DynTrait/drop_nested_boxed_dyn.rs index 2e97317716ad..b6d1bca1bbd5 100644 --- a/src/test/rmc/DynTrait/drop_nested_boxed_dyn.rs +++ b/src/test/rmc/DynTrait/drop_nested_boxed_dyn.rs @@ -19,7 +19,7 @@ impl Drop for Concrete { } } -pub fn main() { +fn main() { // Check normal box { let _x: Box = Box::new(Concrete {}); diff --git a/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs b/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs index 6d6ee07ff861..2107118e312f 100644 --- a/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs +++ b/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs @@ -16,7 +16,7 @@ impl Drop for Concrete { } } -pub fn main() { +fn main() { // Check normal box { let _x: Box = Box::new(Concrete {}); diff --git a/src/test/rmc/DynTrait/dyn_fn_mut.rs b/src/test/rmc/DynTrait/dyn_fn_mut.rs index 8249e800c95f..113a0445ea00 100644 --- a/src/test/rmc/DynTrait/dyn_fn_mut.rs +++ b/src/test/rmc/DynTrait/dyn_fn_mut.rs @@ -12,7 +12,7 @@ pub fn mut_i32_ptr(x: &mut i32) { *x = *x + 1; } -pub fn main() { +fn main() { let mut x = 1; takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x); assert!(x == 2); diff --git a/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs b/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs index 2ba54b860e05..f7721de1638c 100644 --- a/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs @@ -13,7 +13,7 @@ pub fn mut_i32_ptr(x: &mut i32) { *x = *x + 1; } -pub fn main() { +fn main() { let mut x = 1; takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x); rmc::expect_fail(x == 3, "Wrong x") diff --git a/src/test/rmc/DynTrait/dyn_fn_once.rs b/src/test/rmc/DynTrait/dyn_fn_once.rs index 7ef98889c79a..cd77781fc0ba 100644 --- a/src/test/rmc/DynTrait/dyn_fn_once.rs +++ b/src/test/rmc/DynTrait/dyn_fn_once.rs @@ -12,6 +12,6 @@ pub fn unit_to_u32() -> u32 { 5 } -pub fn main() { +fn main() { assert!(takes_dyn_fun(Box::new(&unit_to_u32)) == 5) } diff --git a/src/test/rmc/DynTrait/dyn_fn_once_fail.rs b/src/test/rmc/DynTrait/dyn_fn_once_fail.rs index c5252a555eda..8da6593801ed 100644 --- a/src/test/rmc/DynTrait/dyn_fn_once_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_once_fail.rs @@ -13,6 +13,6 @@ pub fn unit_to_u32() -> u32 { 5 } -pub fn main() { +fn main() { rmc::expect_fail(takes_dyn_fun(Box::new(&unit_to_u32)) == 3, "Wrong u32") } diff --git a/src/test/rmc/DynTrait/dyn_fn_param.rs b/src/test/rmc/DynTrait/dyn_fn_param.rs index b08123ddb962..6dfc62c6bfa9 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param.rs @@ -20,6 +20,6 @@ pub fn unit_to_u32() -> u32 { 5 as u32 } -pub fn main() { +fn main() { takes_dyn_fun(&unit_to_u32) } diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure.rs index 57a8df4451f3..5d1313dfdabf 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure.rs @@ -12,7 +12,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) { /* The closure does not capture anything and thus has zero size */ assert!(size_from_vtable(vtable!(fun)) == 0); } -pub fn main() { +fn main() { let closure = || 5; takes_dyn_fun(&closure) } diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture.rs index f1b8877497df..404ab4b03a9c 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture.rs @@ -14,7 +14,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) { assert!(size_from_vtable(vtable!(fun)) == 8); } -pub fn main() { +fn main() { let a = vec![3]; let closure = || a[0] + 2; takes_dyn_fun(&closure) diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs index 1f7776b7e823..3190dcff4c74 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs @@ -13,7 +13,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) { rmc::expect_fail(size_from_vtable(vtable!(fun)) != 8, "Wrong size"); } -pub fn main() { +fn main() { let a = vec![3]; let closure = || a[0] + 2; takes_dyn_fun(&closure) diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs index 833caef3aeba..ac5d4de5636a 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs @@ -11,7 +11,7 @@ fn takes_dyn_fun(fun: &dyn Fn() -> i32) { /* The closure does not capture anything and thus has zero size */ rmc::expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); } -pub fn main() { +fn main() { let closure = || 5; takes_dyn_fun(&closure) } diff --git a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs index b0cb1cb32946..88fb28c8e513 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs @@ -21,6 +21,6 @@ pub fn unit_to_u32() -> u32 { 5 as u32 } -pub fn main() { +fn main() { takes_dyn_fun(&unit_to_u32) } diff --git a/src/test/rmc/DynTrait/generic_duplicate_names.rs b/src/test/rmc/DynTrait/generic_duplicate_names.rs index 830d472a2a40..7826f6ab16b0 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names.rs @@ -18,7 +18,7 @@ impl Foo for () { impl Bar for () {} -pub fn main() { +fn main() { let b: &dyn Bar = &(); // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. diff --git a/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs b/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs index c6dc3bfc62ae..c2472110b021 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs @@ -19,7 +19,7 @@ impl Foo for () { impl Bar for () {} -pub fn main() { +fn main() { let b: &dyn Bar = &(); // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. diff --git a/src/test/rmc/DynTrait/generic_duplicate_names_impl.rs b/src/test/rmc/DynTrait/generic_duplicate_names_impl.rs index fa9c0e571e34..5d542842c0f9 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names_impl.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names_impl.rs @@ -25,7 +25,7 @@ impl Foo for () { impl Bar for () {} -pub fn main() { +fn main() { let b: &dyn Bar = &(); // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. diff --git a/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs b/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs index 7ac194065a55..8a551c491a3d 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs @@ -26,7 +26,7 @@ impl Foo for () { impl Bar for () {} -pub fn main() { +fn main() { let b: &dyn Bar = &(); // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. diff --git a/src/test/rmc/DynTrait/main.rs b/src/test/rmc/DynTrait/main.rs index a61e7a94e679..48b0c914739c 100644 --- a/src/test/rmc/DynTrait/main.rs +++ b/src/test/rmc/DynTrait/main.rs @@ -28,7 +28,7 @@ fn random_animal(random_number: i64) -> Box { if random_number < 5 { Box::new(Sheep {}) } else { Box::new(Cow {}) } } -pub fn main() { +fn main() { let random_number = rmc::nondet(); let animal = random_animal(random_number); let s = animal.noise(); diff --git a/src/test/rmc/DynTrait/main_fail.rs b/src/test/rmc/DynTrait/main_fail.rs index 88d909a59397..1e918c50d81a 100644 --- a/src/test/rmc/DynTrait/main_fail.rs +++ b/src/test/rmc/DynTrait/main_fail.rs @@ -28,7 +28,7 @@ fn random_animal(random_number: i64) -> Box { if random_number < 5 { Box::new(Sheep {}) } else { Box::new(Cow {}) } } -pub fn main() { +fn main() { let random_number = rmc::nondet(); let animal = random_animal(random_number); let s = animal.noise(); diff --git a/src/test/rmc/DynTrait/nested_boxes.rs b/src/test/rmc/DynTrait/nested_boxes.rs index a35a42a289f9..3abfe68816b9 100644 --- a/src/test/rmc/DynTrait/nested_boxes.rs +++ b/src/test/rmc/DynTrait/nested_boxes.rs @@ -20,7 +20,7 @@ struct Foo { pub _b: i8, } -pub fn main() { +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); diff --git a/src/test/rmc/DynTrait/nested_boxes_fail.rs b/src/test/rmc/DynTrait/nested_boxes_fail.rs index 0f67a0304456..3ceefff3988a 100644 --- a/src/test/rmc/DynTrait/nested_boxes_fail.rs +++ b/src/test/rmc/DynTrait/nested_boxes_fail.rs @@ -22,7 +22,7 @@ struct Foo { pub _b: i8, } -pub fn main() { +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); diff --git a/src/test/rmc/DynTrait/nested_closures.rs b/src/test/rmc/DynTrait/nested_closures.rs index f749091ab066..70375214f783 100644 --- a/src/test/rmc/DynTrait/nested_closures.rs +++ b/src/test/rmc/DynTrait/nested_closures.rs @@ -4,7 +4,7 @@ // Check that we can codegen various nesting structures of boxes and // pointer to closures. -pub fn main() { +fn main() { // Create a nested boxed once-callable closure let f: Box> = Box::new(Box::new(|x| assert!(x == 1))); f(1); diff --git a/src/test/rmc/DynTrait/nested_closures_fail.rs b/src/test/rmc/DynTrait/nested_closures_fail.rs index 1e5ca1b3c86c..dfd9474d63d6 100644 --- a/src/test/rmc/DynTrait/nested_closures_fail.rs +++ b/src/test/rmc/DynTrait/nested_closures_fail.rs @@ -6,7 +6,7 @@ // rmc-verify-fail -pub fn main() { +fn main() { // Create a nested boxed once-callable closure let f: Box> = Box::new(Box::new(|x| rmc::expect_fail(x != 1, "wrong int"))); diff --git a/src/test/rmc/DynTrait/object_safe_generics.rs b/src/test/rmc/DynTrait/object_safe_generics.rs index 6be4b51dc3be..1427151344ad 100644 --- a/src/test/rmc/DynTrait/object_safe_generics.rs +++ b/src/test/rmc/DynTrait/object_safe_generics.rs @@ -30,7 +30,7 @@ impl Foo for () { impl Bar for () {} -pub fn main() { +fn main() { let b: &dyn Bar = &(); // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. Both follow the diff --git a/src/test/rmc/DynTrait/object_safe_trait.rs b/src/test/rmc/DynTrait/object_safe_trait.rs index d67bb0621495..c4cba2cc49e5 100644 --- a/src/test/rmc/DynTrait/object_safe_trait.rs +++ b/src/test/rmc/DynTrait/object_safe_trait.rs @@ -40,7 +40,7 @@ impl NonDispatchable for S { } } -pub fn main() { +fn main() { let s = S {}; S::foo(); let t = s.returns(); diff --git a/src/test/rmc/DynTrait/std_lib_add_duplicate.rs b/src/test/rmc/DynTrait/std_lib_add_duplicate.rs index 481420d06aa6..4a378506eb35 100644 --- a/src/test/rmc/DynTrait/std_lib_add_duplicate.rs +++ b/src/test/rmc/DynTrait/std_lib_add_duplicate.rs @@ -18,7 +18,7 @@ fn weird_add(x: &dyn WeirdAdd, y: i32) -> i32 { x.add(y) } -pub fn main() { +fn main() { let x = 2; let y = 4; diff --git a/src/test/rmc/DynTrait/vtable_duplicate_field_override.rs b/src/test/rmc/DynTrait/vtable_duplicate_field_override.rs index 85c1d1ed9ddd..982f943f7a7c 100644 --- a/src/test/rmc/DynTrait/vtable_duplicate_field_override.rs +++ b/src/test/rmc/DynTrait/vtable_duplicate_field_override.rs @@ -45,7 +45,7 @@ impl T for S { } } -pub fn main() { +fn main() { let t = S::new_box(1, 2, 3); let a = ::foo(&*t); assert!(a == 1); diff --git a/src/test/rmc/DynTrait/vtable_duplicate_fields.rs b/src/test/rmc/DynTrait/vtable_duplicate_fields.rs index 7c754717b3d4..a46a6254fe3f 100644 --- a/src/test/rmc/DynTrait/vtable_duplicate_fields.rs +++ b/src/test/rmc/DynTrait/vtable_duplicate_fields.rs @@ -38,7 +38,7 @@ impl B for S { impl T for S {} -pub fn main() { +fn main() { let t = S::new_box(1, 2); let a = ::foo(&*t); assert!(a == 1); diff --git a/src/test/rmc/DynTrait/vtable_size_align_drop.rs b/src/test/rmc/DynTrait/vtable_size_align_drop.rs index 1a5e2b64d28c..786e35fe85dc 100644 --- a/src/test/rmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/rmc/DynTrait/vtable_size_align_drop.rs @@ -45,7 +45,7 @@ fn random_animal(random_number: i64) -> Box { if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) } } -pub fn main() { +fn main() { // The vtable is laid out as the right hand side here: // // +-------+------------------+ diff --git a/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs index 6a8634b5b49b..f4e287282c00 100644 --- a/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs +++ b/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs @@ -47,7 +47,7 @@ fn random_animal(random_number: i64) -> Box { if random_number < 5 { Box::new(Sheep { sheep_num: 7 }) } else { Box::new(Cow { cow_num: 9 }) } } -pub fn main() { +fn main() { let ptr_size = size_of::<&usize>() as isize; // The vtable is laid out as the right hand side here: diff --git a/src/test/rmc/EQ-NE/main.rs b/src/test/rmc/EQ-NE/main.rs index 03f41e713589..5849086dff9c 100644 --- a/src/test/rmc/EQ-NE/main.rs +++ b/src/test/rmc/EQ-NE/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x: u32 = rmc::nondet(); if x < u32::MAX >> 1 { let y = x * 2; diff --git a/src/test/rmc/Enum/main.rs b/src/test/rmc/Enum/main.rs index 5924cde9cf11..b1d87f8ca262 100644 --- a/src/test/rmc/Enum/main.rs +++ b/src/test/rmc/Enum/main.rs @@ -7,7 +7,7 @@ fn foo() -> Result { Ok(1) } -pub fn main() { +fn main() { let v = foo().unwrap(); assert!(v == 1); } diff --git a/src/test/rmc/Enum/min_offset.rs b/src/test/rmc/Enum/min_offset.rs index d96ac5964c81..4b28179e5f33 100644 --- a/src/test/rmc/Enum/min_offset.rs +++ b/src/test/rmc/Enum/min_offset.rs @@ -12,7 +12,7 @@ enum E { Bar, } -pub fn main() { +fn main() { let e = E::Foo { a: 32, b: 100 }; match e { E::Foo { a, b } => { diff --git a/src/test/rmc/Enum/result1.rs b/src/test/rmc/Enum/result1.rs index 209fee003096..10b11d8a395a 100644 --- a/src/test/rmc/Enum/result1.rs +++ b/src/test/rmc/Enum/result1.rs @@ -3,7 +3,7 @@ #[derive(Debug, PartialEq)] pub enum Empty {} -pub fn main() { +fn main() { let res: Result = Ok(0); if let Ok(num) = res { num + 1; diff --git a/src/test/rmc/Enum/result2.rs b/src/test/rmc/Enum/result2.rs index 8df26b95ee24..eae1477bcdd5 100644 --- a/src/test/rmc/Enum/result2.rs +++ b/src/test/rmc/Enum/result2.rs @@ -3,7 +3,7 @@ #[derive(Debug, PartialEq)] pub enum Empty {} -pub fn main() { +fn main() { let res: Result = Err(0); if let Err(num) = res { num + 1; diff --git a/src/test/rmc/Enum/result3.rs b/src/test/rmc/Enum/result3.rs index 3ebd6149c6bd..5531362420b7 100644 --- a/src/test/rmc/Enum/result3.rs +++ b/src/test/rmc/Enum/result3.rs @@ -10,7 +10,7 @@ fn foo(input: &Result) -> u32 { if let Ok(num) = input { *num } else { 3 } } -pub fn main() { +fn main() { let input: Result = rmc::nondet(); let x = foo(&input); assert!(x == 3 || input != Err(Unit::Unit)); diff --git a/src/test/rmc/Enum/variants_multiple_len_2.rs b/src/test/rmc/Enum/variants_multiple_len_2.rs index 3fce781435ce..9dc7662392ac 100644 --- a/src/test/rmc/Enum/variants_multiple_len_2.rs +++ b/src/test/rmc/Enum/variants_multiple_len_2.rs @@ -6,6 +6,6 @@ pub enum EnumMultiple { Multiple2, } -pub fn main() { +fn main() { let e = EnumMultiple::Multiple1; } diff --git a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_0.rs b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_0.rs index 34bc6aa6c1cf..d38f28bfb367 100644 --- a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_0.rs +++ b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_0.rs @@ -5,7 +5,7 @@ pub enum EnumSingle { MySingle, } -pub fn main() { +fn main() { let e = EnumSingle::MySingle; assert!(e == EnumSingle::MySingle); } diff --git a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_1.rs b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_1.rs index a6fd83bb2bb7..4d5ebadca5b5 100644 --- a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_1.rs +++ b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_1.rs @@ -5,7 +5,7 @@ pub enum EnumSingle { MySingle(u32), } -pub fn main() { +fn main() { let e = EnumSingle::MySingle(1); assert!(e == EnumSingle::MySingle(1)); } diff --git a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_2.rs b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_2.rs index 2fcc3a1d259b..ea8f48809fa2 100644 --- a/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_2.rs +++ b/src/test/rmc/Enum/variants_single_len_1_fields_arbitrary_2.rs @@ -5,7 +5,7 @@ pub enum EnumSingle { MySingle(u32, u32), } -pub fn main() { +fn main() { let e = EnumSingle::MySingle(1, 1); assert!(e == EnumSingle::MySingle(1, 1)); } diff --git a/src/test/rmc/Enum/variants_single_len_2_fields_arbitrary_1.rs b/src/test/rmc/Enum/variants_single_len_2_fields_arbitrary_1.rs index 872c84dd6445..54a96f071a54 100644 --- a/src/test/rmc/Enum/variants_single_len_2_fields_arbitrary_1.rs +++ b/src/test/rmc/Enum/variants_single_len_2_fields_arbitrary_1.rs @@ -8,7 +8,7 @@ pub enum MyInfallible {} fn foo() -> Result { Ok(1) } -pub fn main() { +fn main() { let v = foo().unwrap(); assert!(v == 1); } diff --git a/src/test/rmc/ExactDiv/main.rs b/src/test/rmc/ExactDiv/main.rs index 99b9d258be81..81611738350e 100644 --- a/src/test/rmc/ExactDiv/main.rs +++ b/src/test/rmc/ExactDiv/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(core_intrinsics)] -pub fn main() { +fn main() { let a: u8 = 8; let b: u8 = 4; let i = unsafe { std::intrinsics::exact_div(a, b) }; diff --git a/src/test/rmc/FatPointers/boxmuttrait.rs b/src/test/rmc/FatPointers/boxmuttrait.rs index b9081888fadb..0d7779d5fe8a 100644 --- a/src/test/rmc/FatPointers/boxmuttrait.rs +++ b/src/test/rmc/FatPointers/boxmuttrait.rs @@ -13,7 +13,7 @@ use std::ptr::DynMetadata; include!("../Helpers/vtable_utils_ignore.rs"); -pub fn main() { +fn main() { let mut log: Box = Box::new(sink()); let dest: Box = Box::new(log.as_mut()); diff --git a/src/test/rmc/FatPointers/boxmuttrait_fail.rs b/src/test/rmc/FatPointers/boxmuttrait_fail.rs index c1786b6d8687..63233d093455 100644 --- a/src/test/rmc/FatPointers/boxmuttrait_fail.rs +++ b/src/test/rmc/FatPointers/boxmuttrait_fail.rs @@ -4,7 +4,7 @@ use std::io::{sink, Write}; -pub fn main() { +fn main() { let mut log: Box = Box::new(sink()); let dest: Box = Box::new(log.as_mut()); diff --git a/src/test/rmc/FatPointers/boxslice1.rs b/src/test/rmc/FatPointers/boxslice1.rs index 676cd9b9ef42..3ad0ef84030b 100644 --- a/src/test/rmc/FatPointers/boxslice1.rs +++ b/src/test/rmc/FatPointers/boxslice1.rs @@ -7,7 +7,7 @@ // Casts boxed array to boxed slice (example taken from rust documentation) use std::str; -pub fn main() { +fn main() { // This vector of bytes is used to initialize a Box<[u8; 4]> let sparkle_heart_vec = vec![240, 159, 146, 150]; diff --git a/src/test/rmc/FatPointers/boxslice2.rs b/src/test/rmc/FatPointers/boxslice2.rs index fbbdd548b414..c5c103e36213 100644 --- a/src/test/rmc/FatPointers/boxslice2.rs +++ b/src/test/rmc/FatPointers/boxslice2.rs @@ -5,7 +5,7 @@ // Casts boxed array to boxed slice (example taken from rust documentation) use std::str; -pub fn main() { +fn main() { // This vector of bytes is used to initialize a Box<[u8; 4]> let sparkle_heart_vec = vec![240, 159, 146, 150]; diff --git a/src/test/rmc/FatPointers/boxtrait.rs b/src/test/rmc/FatPointers/boxtrait.rs index e76d2a7121ab..13bc7f45be2f 100644 --- a/src/test/rmc/FatPointers/boxtrait.rs +++ b/src/test/rmc/FatPointers/boxtrait.rs @@ -27,7 +27,7 @@ impl Trait for Concrete { } } -pub fn main() { +fn main() { let mut x: Box = Box::new(Concrete::new()); x.increment(); assert!(x.get() == 1); diff --git a/src/test/rmc/FatPointers/boxtrait_fail.rs b/src/test/rmc/FatPointers/boxtrait_fail.rs index 1136d6847c99..05d650bb8bc3 100644 --- a/src/test/rmc/FatPointers/boxtrait_fail.rs +++ b/src/test/rmc/FatPointers/boxtrait_fail.rs @@ -28,7 +28,7 @@ impl Trait for Concrete { } } -pub fn main() { +fn main() { let mut x: Box = Box::new(Concrete::new()); x.increment(); assert!(x.get() == 3); // Should be x.get() == 1 diff --git a/src/test/rmc/FatPointers/fixme_slice2.rs b/src/test/rmc/FatPointers/fixme_slice2.rs index ea70be8fdd0b..569e8ecf4739 100644 --- a/src/test/rmc/FatPointers/fixme_slice2.rs +++ b/src/test/rmc/FatPointers/fixme_slice2.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let array = [1, 2, 3, 4, 5, 6]; let slice = &array[2..5]; assert!(slice[0] == 3); diff --git a/src/test/rmc/FatPointers/slice1.rs b/src/test/rmc/FatPointers/slice1.rs index 21eeb533a2ba..c43a48a76bc1 100644 --- a/src/test/rmc/FatPointers/slice1.rs +++ b/src/test/rmc/FatPointers/slice1.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let array = [1, 2, 3, 4, 5, 6]; let slice: &[u32] = &array; assert!(slice[0] == 1); diff --git a/src/test/rmc/FatPointers/slice3.rs b/src/test/rmc/FatPointers/slice3.rs index 488df1290d5d..5f08278cf019 100644 --- a/src/test/rmc/FatPointers/slice3.rs +++ b/src/test/rmc/FatPointers/slice3.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let array = [1, 2, 3, 4, 5, 6]; let slice1 = &array[2..5]; let slice2 = &slice1[1..2]; diff --git a/src/test/rmc/FatPointers/structslice.rs b/src/test/rmc/FatPointers/structslice.rs index ead0dd1e41d5..d424bd742df2 100644 --- a/src/test/rmc/FatPointers/structslice.rs +++ b/src/test/rmc/FatPointers/structslice.rs @@ -9,7 +9,7 @@ struct Abstract<'a> { uints: &'a [u32], } -pub fn main() { +fn main() { let x = Concrete { array: [1, 2, 3, 4] }; assert!(x.array[0] == 1); let y = Abstract { uints: &[10, 11, 12, 13] }; diff --git a/src/test/rmc/FatPointers/trait1.rs b/src/test/rmc/FatPointers/trait1.rs index dfca9b544661..2eec16094a26 100644 --- a/src/test/rmc/FatPointers/trait1.rs +++ b/src/test/rmc/FatPointers/trait1.rs @@ -24,7 +24,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let _d = DummySubscriber::new(); let _s = &_d as &dyn Subscriber; assert!(_s.process() == 1); diff --git a/src/test/rmc/FatPointers/trait1_fail.rs b/src/test/rmc/FatPointers/trait1_fail.rs index 8e5f9481f84f..1cb23c38f0c4 100644 --- a/src/test/rmc/FatPointers/trait1_fail.rs +++ b/src/test/rmc/FatPointers/trait1_fail.rs @@ -25,7 +25,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let _d = DummySubscriber::new(); let _s = &_d as &dyn Subscriber; assert!(_s.process() == 3); // Should be _s.process() == 1 diff --git a/src/test/rmc/FatPointers/trait2.rs b/src/test/rmc/FatPointers/trait2.rs index 3af07a2bc60b..2ca1638adb0b 100644 --- a/src/test/rmc/FatPointers/trait2.rs +++ b/src/test/rmc/FatPointers/trait2.rs @@ -24,7 +24,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let _d = DummySubscriber::new(); let _s = &_d as *const dyn Subscriber; assert!(unsafe { _s.as_ref().unwrap().process() } == 1); diff --git a/src/test/rmc/FatPointers/trait2_fail.rs b/src/test/rmc/FatPointers/trait2_fail.rs index 971c41b69877..50de1a127e0a 100644 --- a/src/test/rmc/FatPointers/trait2_fail.rs +++ b/src/test/rmc/FatPointers/trait2_fail.rs @@ -25,7 +25,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let _d = DummySubscriber::new(); let _s = &_d as *const dyn Subscriber; assert!(unsafe { _s.as_ref().unwrap().process() } == 3); // Should be == 1 diff --git a/src/test/rmc/FatPointers/trait3.rs b/src/test/rmc/FatPointers/trait3.rs index 04eba8176ae8..4d9feeb2e443 100644 --- a/src/test/rmc/FatPointers/trait3.rs +++ b/src/test/rmc/FatPointers/trait3.rs @@ -28,7 +28,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let d = DummySubscriber::new(); let d1 = &d as *const DummySubscriber; diff --git a/src/test/rmc/FatPointers/trait3_fail.rs b/src/test/rmc/FatPointers/trait3_fail.rs index a495c8ce9ec6..5a1fca792443 100644 --- a/src/test/rmc/FatPointers/trait3_fail.rs +++ b/src/test/rmc/FatPointers/trait3_fail.rs @@ -29,7 +29,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let d = DummySubscriber::new(); let d1 = &d as *const DummySubscriber; diff --git a/src/test/rmc/FloatingPoint/main.rs b/src/test/rmc/FloatingPoint/main.rs index 4067d31b603f..589a2642f1b3 100644 --- a/src/test/rmc/FloatingPoint/main.rs +++ b/src/test/rmc/FloatingPoint/main.rs @@ -21,7 +21,7 @@ macro_rules! test_floats { }; } -pub fn main() { +fn main() { assert!(1.1 == 1.1 * 1.0); assert!(1.1 != 1.11 / 1.0); diff --git a/src/test/rmc/ForeignItems/fixme_main.rs b/src/test/rmc/ForeignItems/fixme_main.rs index 97528227c50a..3cfd8f3b2153 100644 --- a/src/test/rmc/ForeignItems/fixme_main.rs +++ b/src/test/rmc/ForeignItems/fixme_main.rs @@ -48,7 +48,7 @@ extern "C" { fn takes_struct_ptr2(f: &Foo2) -> u32; } -pub fn main() { +fn main() { unsafe { assert!(S == 12); update_static(); diff --git a/src/test/rmc/ForeignItems/fixme_varadic.rs b/src/test/rmc/ForeignItems/fixme_varadic.rs index 2c38630f12dd..e3a1306e6c80 100644 --- a/src/test/rmc/ForeignItems/fixme_varadic.rs +++ b/src/test/rmc/ForeignItems/fixme_varadic.rs @@ -13,7 +13,7 @@ extern "C" { } -pub fn main() { +fn main() { unsafe { assert!(my_add(2 as usize, 3 as usize, 4 as usize) == 7); //works assert!(my_add(3, 3 as usize, 4 as usize, 5 as usize) == 12); //works diff --git a/src/test/rmc/ForeignItems/main.rs b/src/test/rmc/ForeignItems/main.rs index 93cdd0490284..a99e45078682 100644 --- a/src/test/rmc/ForeignItems/main.rs +++ b/src/test/rmc/ForeignItems/main.rs @@ -36,7 +36,7 @@ extern "C" { fn takes_struct_ptr2(f: &Foo2) -> u32; } -pub fn main() { +fn main() { unsafe { assert!(S == 12); update_static(); diff --git a/src/test/rmc/ForeignItems/missing_fn_fail.rs b/src/test/rmc/ForeignItems/missing_fn_fail.rs index 5034b7d3ac2f..257657778c6b 100644 --- a/src/test/rmc/ForeignItems/missing_fn_fail.rs +++ b/src/test/rmc/ForeignItems/missing_fn_fail.rs @@ -10,7 +10,7 @@ extern "C" { fn missing_int_converter(i: u32) -> u32; } -pub fn main() { +fn main() { unsafe { let x = missing_int_converter(3); assert!(x < 2 || x > 1); diff --git a/src/test/rmc/FunctionAbstractions/mem_replace.rs b/src/test/rmc/FunctionAbstractions/mem_replace.rs index 41256f536aaa..32ba619da356 100644 --- a/src/test/rmc/FunctionAbstractions/mem_replace.rs +++ b/src/test/rmc/FunctionAbstractions/mem_replace.rs @@ -3,7 +3,7 @@ use std::mem; -pub fn main() { +fn main() { let mut var1 = rmc::nondet::(); let mut var2 = rmc::nondet::(); let old_var1 = var1; diff --git a/src/test/rmc/FunctionAbstractions/mem_swap.rs b/src/test/rmc/FunctionAbstractions/mem_swap.rs index 9b8b24ed11a1..7517cbcfb28d 100644 --- a/src/test/rmc/FunctionAbstractions/mem_swap.rs +++ b/src/test/rmc/FunctionAbstractions/mem_swap.rs @@ -3,7 +3,7 @@ use std::mem; -pub fn main() { +fn main() { let mut var1 = rmc::nondet::(); let mut var2 = rmc::nondet::(); let old_var1 = var1; diff --git a/src/test/rmc/FunctionAbstractions/ptr_read.rs b/src/test/rmc/FunctionAbstractions/ptr_read.rs index 02f39d852cca..e4bc1684caff 100644 --- a/src/test/rmc/FunctionAbstractions/ptr_read.rs +++ b/src/test/rmc/FunctionAbstractions/ptr_read.rs @@ -3,7 +3,7 @@ use std::ptr::read; -pub fn main() { +fn main() { let var = 1; unsafe { assert_eq!(read(&var), var); diff --git a/src/test/rmc/FunctionAbstractions/ptr_write.rs b/src/test/rmc/FunctionAbstractions/ptr_write.rs index 328044290715..c04468fd10f5 100644 --- a/src/test/rmc/FunctionAbstractions/ptr_write.rs +++ b/src/test/rmc/FunctionAbstractions/ptr_write.rs @@ -3,7 +3,7 @@ use std::ptr::write; -pub fn main() { +fn main() { let mut var = 1; unsafe { write(&mut var, 10); diff --git a/src/test/rmc/FunctionCall/FnPtr/main.rs b/src/test/rmc/FunctionCall/FnPtr/main.rs index 09db0c15ec52..312677786014 100644 --- a/src/test/rmc/FunctionCall/FnPtr/main.rs +++ b/src/test/rmc/FunctionCall/FnPtr/main.rs @@ -10,7 +10,7 @@ pub struct LocalKey { unsafe fn foo(x: i32) -> i32 { x + 1 } -pub fn main() { +fn main() { let l = LocalKey { inner: foo }; unsafe { assert!((l.inner)(3) == 4) } } diff --git a/src/test/rmc/FunctionCall/Variadic/fixme_main.rs b/src/test/rmc/FunctionCall/Variadic/fixme_main.rs index 17c89b3bca55..c0cd99aebae8 100644 --- a/src/test/rmc/FunctionCall/Variadic/fixme_main.rs +++ b/src/test/rmc/FunctionCall/Variadic/fixme_main.rs @@ -14,7 +14,7 @@ pub unsafe extern "C" fn my_add(num: c_long, mut args: ...) -> c_long { accum } -pub fn main() { +fn main() { let arg0: c_long = 2; let arg1: c_long = 3; let arg1: c_long = 4; diff --git a/src/test/rmc/FunctionCall/Variadic/main.rs b/src/test/rmc/FunctionCall/Variadic/main.rs index 8ad70e44f001..1e0e7a517afc 100644 --- a/src/test/rmc/FunctionCall/Variadic/main.rs +++ b/src/test/rmc/FunctionCall/Variadic/main.rs @@ -12,7 +12,7 @@ type c_long = i64; pub unsafe extern "C" fn syscall(_num: c_long, _: ...) {} -pub fn main() { +fn main() { let arg0: c_long = 0; let arg1: c_long = 1; let _x = unsafe { syscall(0, arg0, arg1) }; diff --git a/src/test/rmc/FunctionCall_ImplicitReturn/main.rs b/src/test/rmc/FunctionCall_ImplicitReturn/main.rs index 45086d2c8f66..894527bcc8c6 100644 --- a/src/test/rmc/FunctionCall_ImplicitReturn/main.rs +++ b/src/test/rmc/FunctionCall_ImplicitReturn/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { assert!(x_plus_two_1(0) == 2); assert!(x_plus_two_2(1) == 3); assert!(x_plus_two_1(x_plus_two_2(0) + 1) == 5); diff --git a/src/test/rmc/FunctionCall_NoRet-NoParam/main.rs b/src/test/rmc/FunctionCall_NoRet-NoParam/main.rs index cdabc5c7c456..9d3c9558ce2c 100644 --- a/src/test/rmc/FunctionCall_NoRet-NoParam/main.rs +++ b/src/test/rmc/FunctionCall_NoRet-NoParam/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { assert!(true); trivial_function(); assert!(1.0 == 1.0); diff --git a/src/test/rmc/FunctionCall_NoRet-Param/main.rs b/src/test/rmc/FunctionCall_NoRet-Param/main.rs index 6f39c20b68f7..871486d7c649 100644 --- a/src/test/rmc/FunctionCall_NoRet-Param/main.rs +++ b/src/test/rmc/FunctionCall_NoRet-Param/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { check_u32(4); check_u32(123); check_u32(119); diff --git a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs index ac9430959664..fb2df43cb4a0 100644 --- a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs +++ b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a = return_u32(); assert!(a < 10); assert!(return_u32() < 10); diff --git a/src/test/rmc/FunctionCall_Ret-Param/main.rs b/src/test/rmc/FunctionCall_Ret-Param/main.rs index 687f55b280d6..57c0e14b8515 100644 --- a/src/test/rmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/rmc/FunctionCall_Ret-Param/main.rs @@ -8,7 +8,7 @@ // a verification failure (the loop being unwound depends on // a nondet. variable) -pub fn main() { +fn main() { let x: u32 = rmc::nondet(); let pi = 3.14159265359; diff --git a/src/test/rmc/Generator/main.rs b/src/test/rmc/Generator/main.rs index fc230d6ac7ca..7bfc80113ab7 100644 --- a/src/test/rmc/Generator/main.rs +++ b/src/test/rmc/Generator/main.rs @@ -21,6 +21,6 @@ fn maybe_call(call: bool) { } } -pub fn main() { +fn main() { maybe_call(false); } diff --git a/src/test/rmc/IfElseifElse_NonReturning/main.rs b/src/test/rmc/IfElseifElse_NonReturning/main.rs index 20876dfe471a..0b90b631978e 100644 --- a/src/test/rmc/IfElseifElse_NonReturning/main.rs +++ b/src/test/rmc/IfElseifElse_NonReturning/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: u32 = rmc::nondet(); if a % 3 == 0 { diff --git a/src/test/rmc/IfElseifElse_Returning/main.rs b/src/test/rmc/IfElseifElse_Returning/main.rs index 067f5384cdf7..c3cb9e62fc44 100644 --- a/src/test/rmc/IfElseifElse_Returning/main.rs +++ b/src/test/rmc/IfElseifElse_Returning/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: u32 = rmc::nondet(); let b = if a % 3 == 0 { diff --git a/src/test/rmc/Intrinsics/abort.rs b/src/test/rmc/Intrinsics/abort.rs index ce77852e62d0..fc445524774d 100644 --- a/src/test/rmc/Intrinsics/abort.rs +++ b/src/test/rmc/Intrinsics/abort.rs @@ -4,6 +4,6 @@ #![feature(core_intrinsics)] use std::intrinsics; -pub fn main() { +fn main() { intrinsics::abort(); } diff --git a/src/test/rmc/Intrinsics/black_box.rs b/src/test/rmc/Intrinsics/black_box.rs index 575e962da1fe..a295747e6754 100644 --- a/src/test/rmc/Intrinsics/black_box.rs +++ b/src/test/rmc/Intrinsics/black_box.rs @@ -4,7 +4,7 @@ #![feature(bench_black_box)] use std::hint::black_box; -pub fn main() { +fn main() { // black_box is an identity function that limits compiler optimizations let a = 10; let b = black_box(a); diff --git a/src/test/rmc/Intrinsics/fixme_catch_unwind.rs b/src/test/rmc/Intrinsics/fixme_catch_unwind.rs index 49cf307da74a..aa7e9e980db6 100644 --- a/src/test/rmc/Intrinsics/fixme_catch_unwind.rs +++ b/src/test/rmc/Intrinsics/fixme_catch_unwind.rs @@ -5,7 +5,7 @@ // Stable way of calling the `try` intrinsic. use std::panic; -pub fn main() { +fn main() { let result = panic::catch_unwind(|| { println!("hello!"); }); diff --git a/src/test/rmc/Intrinsics/fixme_try.rs b/src/test/rmc/Intrinsics/fixme_try.rs index c509f2a83367..e465d38c1543 100644 --- a/src/test/rmc/Intrinsics/fixme_try.rs +++ b/src/test/rmc/Intrinsics/fixme_try.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] use std::intrinsics::r#try; -pub fn main() { +fn main() { unsafe { // Rust will make a best-effort to swallow the panic, and then execute the cleanup function. // However, my understanding is that failure is still possible, since its just a best-effort diff --git a/src/test/rmc/Intrinsics/needs_drop.rs b/src/test/rmc/Intrinsics/needs_drop.rs index 1a06c859d66d..808051eadeaf 100644 --- a/src/test/rmc/Intrinsics/needs_drop.rs +++ b/src/test/rmc/Intrinsics/needs_drop.rs @@ -15,7 +15,7 @@ impl Foo { } } -pub fn main() { +fn main() { // Integers don't need to be dropped let int_foo = Foo:: { _foo: 0 }; assert!(!int_foo.call_needs_drop()); diff --git a/src/test/rmc/Intrinsics/raw_eq.rs b/src/test/rmc/Intrinsics/raw_eq.rs index bff99565568c..a05112d27142 100644 --- a/src/test/rmc/Intrinsics/raw_eq.rs +++ b/src/test/rmc/Intrinsics/raw_eq.rs @@ -4,7 +4,7 @@ #![feature(const_intrinsic_raw_eq)] #![deny(const_err)] -pub fn main() { +fn main() { // Check that we get the expected results for the `raw_eq` intrinsic use std::intrinsics::raw_eq; diff --git a/src/test/rmc/Iterator/try_fold.rs b/src/test/rmc/Iterator/try_fold.rs index 783d7f16f42b..beadd52d4737 100644 --- a/src/test/rmc/Iterator/try_fold.rs +++ b/src/test/rmc/Iterator/try_fold.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // cbmc-flags: --unwind 3 -pub fn main() { +fn main() { let arr = [(1, 2), (2, 2)]; let result = arr.iter().try_fold((), |acc, &i| Some(())); assert_ne!(result, None, "This should succeed"); diff --git a/src/test/rmc/LT-GT-LE-GE/main.rs b/src/test/rmc/LT-GT-LE-GE/main.rs index f2e992289cf9..b29d66d9520a 100644 --- a/src/test/rmc/LT-GT-LE-GE/main.rs +++ b/src/test/rmc/LT-GT-LE-GE/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: u32 = rmc::nondet(); let b = a / 2; assert!(b <= a); diff --git a/src/test/rmc/LoopLoop_NonReturning/main.rs b/src/test/rmc/LoopLoop_NonReturning/main.rs index 0f6c092c73a2..76591cfa43b1 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main.rs @@ -3,7 +3,7 @@ // cbmc-flags: --unwind 10 -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); if a < 1024 { diff --git a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs index a2b110f3216f..9b1a725767ab 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -21,7 +21,7 @@ // // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); if a < 1024 { diff --git a/src/test/rmc/LoopWhile_NonReturning/main.rs b/src/test/rmc/LoopWhile_NonReturning/main.rs index 3e83f719ffbf..85dc4bc2772d 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main.rs @@ -3,7 +3,7 @@ // cbmc-flags: --unwind 11 -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); if a < 1024 { diff --git a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs index 1813b40d7115..37a6be42b67c 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -22,7 +22,7 @@ // // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL -pub fn main() { +fn main() { let mut a: u32 = rmc::nondet(); if a < 1024 { diff --git a/src/test/rmc/MemReplace/main.rs b/src/test/rmc/MemReplace/main.rs index 4275f7607c6b..c75b6f98da79 100644 --- a/src/test/rmc/MemReplace/main.rs +++ b/src/test/rmc/MemReplace/main.rs @@ -4,7 +4,7 @@ enum Dummy { Dumb, } -pub fn main() { +fn main() { // invoke replace on a zero-sized type let mut value: Dummy = Dummy::Dumb; let dst: &mut Dummy = &mut value; diff --git a/src/test/rmc/Never/main.rs b/src/test/rmc/Never/main.rs index 87f1c67c2768..0c9c3f506866 100644 --- a/src/test/rmc/Never/main.rs +++ b/src/test/rmc/Never/main.rs @@ -13,4 +13,4 @@ pub fn bar(infalliable: Infallible) -> i32 { } // Give an empty main to make rustc happy. -pub fn main() {} +fn main() {} diff --git a/src/test/rmc/Never/never_return.rs b/src/test/rmc/Never/never_return.rs index d37c099cf268..5bd1be309eb7 100644 --- a/src/test/rmc/Never/never_return.rs +++ b/src/test/rmc/Never/never_return.rs @@ -11,7 +11,7 @@ pub fn err() -> ! { // Give an empty main to make rustc happy. #[no_mangle] -pub fn main() { +fn main() { let var = rmc::nondet::(); if var > 0 { err(); diff --git a/src/test/rmc/NondetVectors/bytes.rs b/src/test/rmc/NondetVectors/bytes.rs index 20fdb0765d72..ac819897ccd5 100644 --- a/src/test/rmc/NondetVectors/bytes.rs +++ b/src/test/rmc/NondetVectors/bytes.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::convert::TryInto; -pub fn main() { +fn main() { let input: &[u8] = &vec![ rmc::nondet(), rmc::nondet(), diff --git a/src/test/rmc/NondetVectors/fixme_main.rs b/src/test/rmc/NondetVectors/fixme_main.rs index eaad4cf85806..889d1131098b 100644 --- a/src/test/rmc/NondetVectors/fixme_main.rs +++ b/src/test/rmc/NondetVectors/fixme_main.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT const FIFO_SIZE: usize = 2; -pub fn main() { +fn main() { let len: usize = rmc::nondet(); if !(len <= FIFO_SIZE) { return; diff --git a/src/test/rmc/Parenths/main.rs b/src/test/rmc/Parenths/main.rs index 7ecc767377f7..a4638549ce63 100644 --- a/src/test/rmc/Parenths/main.rs +++ b/src/test/rmc/Parenths/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a = 10; let b = (a + 6) / 2; assert!(b == 8); diff --git a/src/test/rmc/PointerOffset/Stable/main.rs b/src/test/rmc/PointerOffset/Stable/main.rs index 8cf2b2f7df77..9d6ecad8d5a4 100644 --- a/src/test/rmc/PointerOffset/Stable/main.rs +++ b/src/test/rmc/PointerOffset/Stable/main.rs @@ -9,7 +9,7 @@ // [overflow.2] arithmetic overflow on signed - in var_11 - var_12: FAILURE // Tracking issue: https://github.com/model-checking/rmc/issues/307 -pub fn main() { +fn main() { // pub unsafe fn offset_from(self, origin: *const T) -> isize // Calculates the distance between two pointers. The returned value // is in units of T: the distance in bytes is divided by mem::size_of::(). diff --git a/src/test/rmc/PointerOffset/Unstable/main.rs b/src/test/rmc/PointerOffset/Unstable/main.rs index 7d9fdda61f26..0ada27120326 100644 --- a/src/test/rmc/PointerOffset/Unstable/main.rs +++ b/src/test/rmc/PointerOffset/Unstable/main.rs @@ -12,7 +12,7 @@ #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; -pub fn main() { +fn main() { let a = [0; 5]; let b = [0; 5]; let ptr1: *const i32 = &a[1]; diff --git a/src/test/rmc/PointerOffset/Unstable/main_fail.rs b/src/test/rmc/PointerOffset/Unstable/main_fail.rs index 116d6c74f395..a7ced6f3510b 100644 --- a/src/test/rmc/PointerOffset/Unstable/main_fail.rs +++ b/src/test/rmc/PointerOffset/Unstable/main_fail.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; -pub fn main() { +fn main() { let a = [0; 5]; let b = [0; 5]; let ptr1: *const i32 = &a[1]; diff --git a/src/test/rmc/Pointers_Basic/fixme_from_raw.rs b/src/test/rmc/Pointers_Basic/fixme_from_raw.rs index 79879e608167..ea8d8c3271ca 100644 --- a/src/test/rmc/Pointers_Basic/fixme_from_raw.rs +++ b/src/test/rmc/Pointers_Basic/fixme_from_raw.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-verify-fail -pub fn main() { +fn main() { let address = 0x01234usize; let ptr = address as *mut i32; // pointers can only be dereferenced inside unsafe blocks diff --git a/src/test/rmc/Pointers_Basic/main.rs b/src/test/rmc/Pointers_Basic/main.rs index 27fd7aaa8d83..748451772072 100644 --- a/src/test/rmc/Pointers_Basic/main.rs +++ b/src/test/rmc/Pointers_Basic/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x = 3; let y = &x; let mut z = *y; diff --git a/src/test/rmc/Pointers_Functions/main.rs b/src/test/rmc/Pointers_Functions/main.rs index 146a116cacfa..7b371933f048 100644 --- a/src/test/rmc/Pointers_Functions/main.rs +++ b/src/test/rmc/Pointers_Functions/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut x = 1; add_two(&mut x); assert!(x == 3); diff --git a/src/test/rmc/Pointers_InAssert/main.rs b/src/test/rmc/Pointers_InAssert/main.rs index 1376d3c1290e..827508bc16cb 100644 --- a/src/test/rmc/Pointers_InAssert/main.rs +++ b/src/test/rmc/Pointers_InAssert/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut a = 5; let mut c = &mut a; add_two(c); diff --git a/src/test/rmc/Pointers_OtherTypes/main.rs b/src/test/rmc/Pointers_OtherTypes/main.rs index d4151c2ce197..be5c183d0e25 100644 --- a/src/test/rmc/Pointers_OtherTypes/main.rs +++ b/src/test/rmc/Pointers_OtherTypes/main.rs @@ -8,7 +8,7 @@ // [main.NaN.1] line 25 NaN on * in var_30 * 0.0f: FAILURE // Tracking issue: https://github.com/model-checking/rmc/issues/307 -pub fn main() { +fn main() { let mut x = 1; add_two(&mut x); assert!(x == 3); diff --git a/src/test/rmc/Pointers_OutOfScopeFail/fixme_main.rs b/src/test/rmc/Pointers_OutOfScopeFail/fixme_main.rs index 991ed922cb55..744213ee8767 100644 --- a/src/test/rmc/Pointers_OutOfScopeFail/fixme_main.rs +++ b/src/test/rmc/Pointers_OutOfScopeFail/fixme_main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-verify-fail -pub fn main() { +fn main() { // declare pointer to integer let p_subscoped: *const u32; diff --git a/src/test/rmc/ProjectionElem/ConstantIndex/main.rs b/src/test/rmc/ProjectionElem/ConstantIndex/main.rs index 0c5704d5f493..12ac121b1574 100644 --- a/src/test/rmc/ProjectionElem/ConstantIndex/main.rs +++ b/src/test/rmc/ProjectionElem/ConstantIndex/main.rs @@ -96,7 +96,7 @@ fn test4() { assert!(encode_utf8_raw(code, dst) == 0); } -pub fn main() { +fn main() { test1(); test2(); test3(&[1, 2, 3, 4]); diff --git a/src/test/rmc/Refs/fixme_main.rs b/src/test/rmc/Refs/fixme_main.rs index 503d8e813535..faf14c00766e 100644 --- a/src/test/rmc/Refs/fixme_main.rs +++ b/src/test/rmc/Refs/fixme_main.rs @@ -79,7 +79,7 @@ impl<'a> ArgParser<'a> { } } -pub fn main() { +fn main() { let a: ArgParser = ArgParser { arguments: BTreeMap::new() }; a.format_arguments(); } diff --git a/src/test/rmc/Repr/main.rs b/src/test/rmc/Repr/main.rs index e485e992abf3..3aa5301a7ce9 100644 --- a/src/test/rmc/Repr/main.rs +++ b/src/test/rmc/Repr/main.rs @@ -13,7 +13,7 @@ fn mmap() -> *mut MyCVoid { 0 as *mut MyCVoid } -pub fn main() { +fn main() { let v = mmap(); assert!(v != MAP_FAILED); assert!(v.is_null()); diff --git a/src/test/rmc/SIMD/Compare/main.rs b/src/test/rmc/SIMD/Compare/main.rs index fc42d32acda0..adfd84cc1376 100644 --- a/src/test/rmc/SIMD/Compare/main.rs +++ b/src/test/rmc/SIMD/Compare/main.rs @@ -31,7 +31,7 @@ macro_rules! assert_cmp { // Vectors are compared element-wise producing: // * 0 when comparison is false // * -1 (all bits set) otherwise -pub fn main() { +fn main() { let x = i64x2(0, 0); let y = i64x2(0, 1); diff --git a/src/test/rmc/SIMD/Construction/main.rs b/src/test/rmc/SIMD/Construction/main.rs index 64a60d3c7d60..48d7aa444035 100644 --- a/src/test/rmc/SIMD/Construction/main.rs +++ b/src/test/rmc/SIMD/Construction/main.rs @@ -12,7 +12,7 @@ extern "platform-intrinsic" { fn simd_insert(x: T, idx: u32, b: U) -> T; } -pub fn main() { +fn main() { let y = i64x2(0, 1); let z = i64x2(1, 2); diff --git a/src/test/rmc/SIMD/Operators/main.rs b/src/test/rmc/SIMD/Operators/main.rs index 9a73ffa23903..c184f2bb32ec 100644 --- a/src/test/rmc/SIMD/Operators/main.rs +++ b/src/test/rmc/SIMD/Operators/main.rs @@ -29,7 +29,7 @@ macro_rules! assert_op { // Tests inspired by Rust's examples in // https://github.com/rust-lang/rust/blob/0d97f7a96877a96015d70ece41ad08bb7af12377/src/test/ui/simd-intrinsic/simd-intrinsic-generic-arithmetic.rs -pub fn main() { +fn main() { let x = i64x2(0, 0); let y = i64x2(0, 1); let z = i64x2(1, 2); diff --git a/src/test/rmc/SIMD/Shuffle/main.rs b/src/test/rmc/SIMD/Shuffle/main.rs index 098c11e5e362..4fe19d77e422 100644 --- a/src/test/rmc/SIMD/Shuffle/main.rs +++ b/src/test/rmc/SIMD/Shuffle/main.rs @@ -17,7 +17,7 @@ extern "platform-intrinsic" { fn simd_shuffle4(x: T, y: T, idx: [u32; 4]) -> U; } -pub fn main() { +fn main() { { let y = i64x2(0, 1); let z = i64x2(1, 2); diff --git a/src/test/rmc/SaturatingIntrinsics/fixme_128.rs b/src/test/rmc/SaturatingIntrinsics/fixme_128.rs index 004943ce1c11..66e9f2848a5d 100644 --- a/src/test/rmc/SaturatingIntrinsics/fixme_128.rs +++ b/src/test/rmc/SaturatingIntrinsics/fixme_128.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] use std::intrinsics; -pub fn main() { +fn main() { let v: u128 = rmc::nondet(); let w: u128 = rmc::nondet(); intrinsics::saturating_add(v, w); diff --git a/src/test/rmc/SaturatingIntrinsics/main.rs b/src/test/rmc/SaturatingIntrinsics/main.rs index 9fa58dbc22a3..31fa51b78d45 100644 --- a/src/test/rmc/SaturatingIntrinsics/main.rs +++ b/src/test/rmc/SaturatingIntrinsics/main.rs @@ -49,7 +49,7 @@ macro_rules! test_saturating_intrinsics { }; } -pub fn main() { +fn main() { test_saturating_intrinsics!(u8); test_saturating_intrinsics!(u16); test_saturating_intrinsics!(u32); diff --git a/src/test/rmc/Scopes_NonReturning/main.rs b/src/test/rmc/Scopes_NonReturning/main.rs index 46ca5f282365..b2dbb0cb0d57 100644 --- a/src/test/rmc/Scopes_NonReturning/main.rs +++ b/src/test/rmc/Scopes_NonReturning/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: u32 = rmc::nondet(); let b = a / 2; let c = a / 2; diff --git a/src/test/rmc/Scopes_Returning/main.rs b/src/test/rmc/Scopes_Returning/main.rs index 6400f73f35bc..d0de28d81371 100644 --- a/src/test/rmc/Scopes_Returning/main.rs +++ b/src/test/rmc/Scopes_Returning/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x = { 5 }; assert!(x == 5); diff --git a/src/test/rmc/Serde/main.rs b/src/test/rmc/Serde/main.rs index 2c34e6979e1d..acd38b53b2e7 100644 --- a/src/test/rmc/Serde/main.rs +++ b/src/test/rmc/Serde/main.rs @@ -17,7 +17,7 @@ impl fmt::Display for OneOf { } } -pub fn main() { +fn main() { let v = OneOf { names: &["one"] }; println!("{}", v); } diff --git a/src/test/rmc/SizeAndAlignOfDst/main_assert_fixme.rs b/src/test/rmc/SizeAndAlignOfDst/main_assert_fixme.rs index 7c038ff06100..ca25e765b5a1 100644 --- a/src/test/rmc/SizeAndAlignOfDst/main_assert_fixme.rs +++ b/src/test/rmc/SizeAndAlignOfDst/main_assert_fixme.rs @@ -60,7 +60,7 @@ impl Subscriber for DummySubscriber { } } -pub fn main() { +fn main() { let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); let mut data = s.lock().unwrap(); data.increment(); diff --git a/src/test/rmc/SizeAndAlignOfDst/main_fixme.rs b/src/test/rmc/SizeAndAlignOfDst/main_fixme.rs index 6f8e644f2ffd..477bea37fe7d 100644 --- a/src/test/rmc/SizeAndAlignOfDst/main_fixme.rs +++ b/src/test/rmc/SizeAndAlignOfDst/main_fixme.rs @@ -53,6 +53,6 @@ impl Subscriber for DummySubscriber { fn interest_list(&self) {} } -pub fn main() { +fn main() { let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); } diff --git a/src/test/rmc/Slice/codegen.rs b/src/test/rmc/Slice/codegen.rs index 3f57e79d703f..c499cf1fbccc 100644 --- a/src/test/rmc/Slice/codegen.rs +++ b/src/test/rmc/Slice/codegen.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let name = String::from("Mark"); let name_str = name.as_str(); assert!(name_str.len() > 0); diff --git a/src/test/rmc/Slice/drop_in_place.rs b/src/test/rmc/Slice/drop_in_place.rs index d02a9c473b0f..b0dfdf1bb593 100644 --- a/src/test/rmc/Slice/drop_in_place.rs +++ b/src/test/rmc/Slice/drop_in_place.rs @@ -11,7 +11,7 @@ pub unsafe fn drop_in_place(to_drop: *mut T) { unsafe { drop_in_place(to_drop) } } -pub fn main() { +fn main() { let mut x = 3; drop_in_place(x); } diff --git a/src/test/rmc/Slice/main.rs b/src/test/rmc/Slice/main.rs index d90ebd29de76..eaf911150ec1 100644 --- a/src/test/rmc/Slice/main.rs +++ b/src/test/rmc/Slice/main.rs @@ -3,7 +3,7 @@ // cbmc-flags: --unwind 6 -pub fn main() { +fn main() { let name: &str = "hello"; assert!(name == "hello"); } diff --git a/src/test/rmc/Slice/pathbuf.rs b/src/test/rmc/Slice/pathbuf.rs index d7c886914369..1e70d972ec0b 100644 --- a/src/test/rmc/Slice/pathbuf.rs +++ b/src/test/rmc/Slice/pathbuf.rs @@ -4,7 +4,7 @@ use std::fs; use std::path::PathBuf; -pub fn main() { +fn main() { let buf = PathBuf::new(); let _x = fs::remove_dir_all(buf); } diff --git a/src/test/rmc/Slice/slice.rs b/src/test/rmc/Slice/slice.rs index e60f55b1caec..788bfa4416d1 100644 --- a/src/test/rmc/Slice/slice.rs +++ b/src/test/rmc/Slice/slice.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let list = [1, 2, 3]; let slice = &list[1..2]; assert!(slice.len() > 0); diff --git a/src/test/rmc/Slice/slice_from_raw.rs b/src/test/rmc/Slice/slice_from_raw.rs index b1036fde7aba..12ff8b97c24f 100644 --- a/src/test/rmc/Slice/slice_from_raw.rs +++ b/src/test/rmc/Slice/slice_from_raw.rs @@ -5,7 +5,7 @@ use std::slice; // From Listing 19-7: Creating a slice from an arbitrary memory location. https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html -pub fn main() { +fn main() { let address = 0x01234usize; let r = address as *mut i32; let slice: &mut [i32] = unsafe { slice::from_raw_parts_mut(r, 10000) }; diff --git a/src/test/rmc/Static/main.rs b/src/test/rmc/Static/main.rs index 5b83365dae4d..70a80f2a8730 100644 --- a/src/test/rmc/Static/main.rs +++ b/src/test/rmc/Static/main.rs @@ -11,7 +11,7 @@ pub enum MyEnum { ChoiceC, } -pub fn main() { +fn main() { assert!(!X); unsafe { Y = true; diff --git a/src/test/rmc/Static/table_of_pairs.rs b/src/test/rmc/Static/table_of_pairs.rs index 5f53c45e5af9..b045309a19ac 100644 --- a/src/test/rmc/Static/table_of_pairs.rs +++ b/src/test/rmc/Static/table_of_pairs.rs @@ -7,7 +7,7 @@ fn test_equal(a: u64, b: u64) -> bool { a == b } -pub fn main() { +fn main() { let x = TABLE[0]; assert!(test_equal(x.1, 2)); } diff --git a/src/test/rmc/Static/table_of_pairs2.rs b/src/test/rmc/Static/table_of_pairs2.rs index 0c63a24d1944..3766a30ef497 100644 --- a/src/test/rmc/Static/table_of_pairs2.rs +++ b/src/test/rmc/Static/table_of_pairs2.rs @@ -12,7 +12,7 @@ fn test_equal(a: u64, b: u64) -> bool { a == b } -pub fn main() { +fn main() { let x = TABLE1[0]; assert!(test_equal(x.1, 1)); let y = TABLE2[0]; diff --git a/src/test/rmc/Strings/copy_empty_string_by_intrinsic.rs b/src/test/rmc/Strings/copy_empty_string_by_intrinsic.rs index 030e4d205d81..0258d412ba9c 100644 --- a/src/test/rmc/Strings/copy_empty_string_by_intrinsic.rs +++ b/src/test/rmc/Strings/copy_empty_string_by_intrinsic.rs @@ -24,7 +24,7 @@ fn copy_string(s: &str, l: usize) { } } -pub fn main() { +fn main() { copy_string("x", 1); copy_string("", 0); } diff --git a/src/test/rmc/Strings/copy_empty_string_by_intrinsic_fixme.rs b/src/test/rmc/Strings/copy_empty_string_by_intrinsic_fixme.rs index f905e74c368b..cc56426c6c05 100644 --- a/src/test/rmc/Strings/copy_empty_string_by_intrinsic_fixme.rs +++ b/src/test/rmc/Strings/copy_empty_string_by_intrinsic_fixme.rs @@ -37,7 +37,7 @@ fn copy_string(s: &str, l: usize) { } } -pub fn main() { +fn main() { // Verification fails for both of these cases. copy_string("x", 1); copy_string("", 0); diff --git a/src/test/rmc/Strings/copy_empty_string_by_ref.rs b/src/test/rmc/Strings/copy_empty_string_by_ref.rs index 6e5089e78325..6df0193e54aa 100644 --- a/src/test/rmc/Strings/copy_empty_string_by_ref.rs +++ b/src/test/rmc/Strings/copy_empty_string_by_ref.rs @@ -7,7 +7,7 @@ fn take_string_ref(s: &str, l: usize) { assert!(s.len() == l) } -pub fn main() { +fn main() { take_string_ref(&"x".to_string(), 1); take_string_ref(&"".to_string(), 0); } diff --git a/src/test/rmc/Strings/fixme_boxed_str.rs b/src/test/rmc/Strings/fixme_boxed_str.rs index a471becb9e2d..e00e96daa35a 100644 --- a/src/test/rmc/Strings/fixme_boxed_str.rs +++ b/src/test/rmc/Strings/fixme_boxed_str.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // Fails with a type safety error - see TODO in rvalue.rs::codegen_misc_cast() -pub fn main() { +fn main() { let s = String::from("hello"); let _b = s.into_boxed_str(); } diff --git a/src/test/rmc/Strings/fixme_main.rs b/src/test/rmc/Strings/fixme_main.rs index 90a6ecd3e0d0..2e7e190b8a49 100644 --- a/src/test/rmc/Strings/fixme_main.rs +++ b/src/test/rmc/Strings/fixme_main.rs @@ -23,7 +23,7 @@ fn test4() { //assert!(*ptr.offset(1) as char == '2'); // u8 to char not handled yet } } -pub fn main() { +fn main() { // test2(); // test3(); test4(); diff --git a/src/test/rmc/Strings/fixme_os_str.rs b/src/test/rmc/Strings/fixme_os_str.rs index 718f75877087..33ab5e13fabc 100644 --- a/src/test/rmc/Strings/fixme_os_str.rs +++ b/src/test/rmc/Strings/fixme_os_str.rs @@ -44,7 +44,7 @@ impl OsStr { } } -pub fn main() { +fn main() { let x = OsStr::new("hi"); x.as_bytes(); } diff --git a/src/test/rmc/Strings/main.rs b/src/test/rmc/Strings/main.rs index d3c371dece07..c7cc4fc3193e 100644 --- a/src/test/rmc/Strings/main.rs +++ b/src/test/rmc/Strings/main.rs @@ -20,6 +20,6 @@ fn test1() { assert!(string.len() == 3); } -pub fn main() { +fn main() { test1(); } diff --git a/src/test/rmc/Strings/os_str_reduced.rs b/src/test/rmc/Strings/os_str_reduced.rs index 99e64106eb35..8aa00a90f882 100644 --- a/src/test/rmc/Strings/os_str_reduced.rs +++ b/src/test/rmc/Strings/os_str_reduced.rs @@ -28,7 +28,7 @@ fn test2() { assert!(inner.inner[1] == 'i' as u8); } -pub fn main() { +fn main() { test1(); test2(); } diff --git a/src/test/rmc/SubSlice/subslice1.rs b/src/test/rmc/SubSlice/subslice1.rs index da349d3aaa38..7c79c734e8e1 100644 --- a/src/test/rmc/SubSlice/subslice1.rs +++ b/src/test/rmc/SubSlice/subslice1.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let arr = [1, 2, 3]; // s is a slice (&[i32]) let [s @ ..] = &arr[..]; diff --git a/src/test/rmc/SubSlice/subslice2_fixme.rs b/src/test/rmc/SubSlice/subslice2_fixme.rs index bb4bdb8d9351..06cf15c3550a 100644 --- a/src/test/rmc/SubSlice/subslice2_fixme.rs +++ b/src/test/rmc/SubSlice/subslice2_fixme.rs @@ -30,7 +30,7 @@ // Full support for subslice projection to be added in // https://github.com/model-checking/rmc/issues/357 -pub fn main() { +fn main() { let arr = [1, 2, 3]; // s is a slice (&[i32]) let [s @ ..] = &arr[1..]; diff --git a/src/test/rmc/SwitchInt/main.rs b/src/test/rmc/SwitchInt/main.rs index 1e0ccc3adc2d..9c341457e204 100644 --- a/src/test/rmc/SwitchInt/main.rs +++ b/src/test/rmc/SwitchInt/main.rs @@ -36,7 +36,7 @@ fn doswitch_bytes() -> i32 { return 2; } -pub fn main() { +fn main() { let v = doswitch_int(); assert!(v == 1); let v = doswitch_chars(); diff --git a/src/test/rmc/Transparent/transparent1.rs b/src/test/rmc/Transparent/transparent1.rs index 54c478b6a2cd..96386187c4ad 100644 --- a/src/test/rmc/Transparent/transparent1.rs +++ b/src/test/rmc/Transparent/transparent1.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let mut x: u32 = 4; let pointer0: std::ptr::NonNull = std::ptr::NonNull::new(&mut x).unwrap(); let y = unsafe { *pointer0.as_ptr() }; diff --git a/src/test/rmc/Transparent/transparent2.rs b/src/test/rmc/Transparent/transparent2.rs index 1138dc73151e..d872cad4ccdf 100644 --- a/src/test/rmc/Transparent/transparent2.rs +++ b/src/test/rmc/Transparent/transparent2.rs @@ -23,7 +23,7 @@ where } } -pub fn main() { +fn main() { let mut x: u32 = 4; let container = Container::new(&mut x); let _y = container.get(); diff --git a/src/test/rmc/Transparent/transparent3.rs b/src/test/rmc/Transparent/transparent3.rs index bd857994bcf7..7d342118bdeb 100644 --- a/src/test/rmc/Transparent/transparent3.rs +++ b/src/test/rmc/Transparent/transparent3.rs @@ -10,7 +10,7 @@ pub struct Container { container: Pointer, } -pub fn main() { +fn main() { let x: u32 = 4; let my_pointer = Pointer { pointer: &x }; let my_container = Container { container: my_pointer }; diff --git a/src/test/rmc/Transparent/transparent4.rs b/src/test/rmc/Transparent/transparent4.rs index 145e8fdd988a..96c1916858c5 100644 --- a/src/test/rmc/Transparent/transparent4.rs +++ b/src/test/rmc/Transparent/transparent4.rs @@ -13,7 +13,7 @@ pub struct Container { container: Pointer, } -pub fn main() { +fn main() { let x: u32 = 4; let my_container = Container { container: Pointer { pointer: &x } }; diff --git a/src/test/rmc/Unit/main.rs b/src/test/rmc/Unit/main.rs index 1d842b2de2f3..8829690c4658 100644 --- a/src/test/rmc/Unit/main.rs +++ b/src/test/rmc/Unit/main.rs @@ -18,7 +18,7 @@ fn ret_unit() { () } -pub fn main() { +fn main() { assert!(() == ()); let u = ret_unit(); assert!(u == ()); diff --git a/src/test/rmc/UnsafeBlocks_Useless/main.rs b/src/test/rmc/UnsafeBlocks_Useless/main.rs index aa3ebcab012f..f093a5879b2c 100644 --- a/src/test/rmc/UnsafeBlocks_Useless/main.rs +++ b/src/test/rmc/UnsafeBlocks_Useless/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let x = unsafe { assert!(true); 5 diff --git a/src/test/rmc/Vectors/fixme_main.rs b/src/test/rmc/Vectors/fixme_main.rs index 263fc9b67bf0..e5f896339572 100644 --- a/src/test/rmc/Vectors/fixme_main.rs +++ b/src/test/rmc/Vectors/fixme_main.rs @@ -9,7 +9,7 @@ pub struct GuestRegionMmap { } // TODO: running this with --unwrap 2 causes CBMC to hang in propositional reduction. -pub fn main() { +fn main() { let r = GuestRegionMmap { guest_base: GuestAddress(0) }; let mut regions: Vec = vec![]; regions.push(r); diff --git a/src/test/rmc/Vectors/vector_extend.rs b/src/test/rmc/Vectors/vector_extend.rs index aae0270adbd7..9b69be65ea95 100644 --- a/src/test/rmc/Vectors/vector_extend.rs +++ b/src/test/rmc/Vectors/vector_extend.rs @@ -4,7 +4,7 @@ // Check that we can handle set len on drop. If drop_in_place is not // called correctly, this will fail to actually extend the vector. -pub fn main() { +fn main() { let mut v: Vec = Vec::new(); v.extend(42..=42); assert!(v[0] == 42); diff --git a/src/test/rmc/Vectors/vector_extend_fail.rs b/src/test/rmc/Vectors/vector_extend_fail.rs index 59c70e0cde26..dcc8de177b16 100644 --- a/src/test/rmc/Vectors/vector_extend_fail.rs +++ b/src/test/rmc/Vectors/vector_extend_fail.rs @@ -5,7 +5,7 @@ // rmc-verify-fail -pub fn main() { +fn main() { let mut v: Vec = Vec::new(); v.extend(42..=42); assert!(v[0] == 41); // Incorrect value diff --git a/src/test/rmc/Vectors/vector_extend_in_new.rs b/src/test/rmc/Vectors/vector_extend_in_new.rs index f4cfc99c1d20..cba398134c87 100644 --- a/src/test/rmc/Vectors/vector_extend_in_new.rs +++ b/src/test/rmc/Vectors/vector_extend_in_new.rs @@ -7,7 +7,7 @@ // There is an implicit loop, so we need an explicit unwind // cbmc-flags: --unwind 3 --unwinding-assertions -pub fn main() { +fn main() { let a: Vec> = vec![vec![0; 2]; 1]; assert!(a.len() == 1); } diff --git a/src/test/rmc/VolatileIntrinsics/core_intrinsics.rs b/src/test/rmc/VolatileIntrinsics/core_intrinsics.rs index e27956c1e7a5..183eeda75ea5 100644 --- a/src/test/rmc/VolatileIntrinsics/core_intrinsics.rs +++ b/src/test/rmc/VolatileIntrinsics/core_intrinsics.rs @@ -6,7 +6,7 @@ use std::intrinsics::*; -pub fn main() { +fn main() { let mut a: Box = Box::new(0); unsafe { let x = volatile_load(&*a); diff --git a/src/test/rmc/VolatileIntrinsics/main.rs b/src/test/rmc/VolatileIntrinsics/main.rs index 21dfa5be9cd5..ae9f71ba2101 100644 --- a/src/test/rmc/VolatileIntrinsics/main.rs +++ b/src/test/rmc/VolatileIntrinsics/main.rs @@ -114,7 +114,7 @@ fn test_copy_volatile_nonoverlapping() { } } -pub fn main() { +fn main() { test_volatile_store(); test_copy_volatile(); test_copy_volatile_nonoverlapping(); diff --git a/src/test/rmc/Whitespace/main.rs b/src/test/rmc/Whitespace/main.rs index fafb04f4e8d6..3e321e7a83b2 100644 --- a/src/test/rmc/Whitespace/main.rs +++ b/src/test/rmc/Whitespace/main.rs @@ -10,7 +10,7 @@ // [_RNvXs5_NtNtCs9Odk7Lrvgnw_4core3str7patternINtB5_19MultiCharEqSearcherNtB7_12IsWhitespaceENtB5_8Searcher4nextCs21hi0yVfW1J_4main.overflow.1] line 641 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_5 + 8)) - 1114112: FAILURE // Tracking issue: https://github.com/model-checking/rmc/issues/307 -pub fn main() { +fn main() { let mut iter = "A few words".split_whitespace(); match iter.next() { None => assert!(false), diff --git a/src/test/rmc/i32-Unary-/main.rs b/src/test/rmc/i32-Unary-/main.rs index 066ac239eb20..0fb94edd4261 100644 --- a/src/test/rmc/i32-Unary-/main.rs +++ b/src/test/rmc/i32-Unary-/main.rs @@ -1,6 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -pub fn main() { +fn main() { let a: i32 = rmc::nondet(); if -100000 < a && a < 100000 { let b = -a;