diff --git a/rust-tests/.gitignore b/rust-tests/.gitignore deleted file mode 100644 index 74c56fa256d2..000000000000 --- a/rust-tests/.gitignore +++ /dev/null @@ -1 +0,0 @@ -.sandbox/ diff --git a/rust-tests/run.sh b/rust-tests/run.sh deleted file mode 100755 index f2e0611b17e4..000000000000 --- a/rust-tests/run.sh +++ /dev/null @@ -1,51 +0,0 @@ -#!/bin/bash -# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 OR MIT - -rm -rf .sandbox || true -mkdir .sandbox - -TEST_DIR=${1:-.} -UNWIND=${2:-10} - -EXIT_CODE=0 -for f in `find $TEST_DIR -name '*.rs'`; do - BASE=`basename "$f"` - NAME=${BASE%.rs} - - printf "Verifying %-64s" $f - if [[ "$f" == *fixme* ]]; then - echo "SKIP (known FAIL)" - continue - fi - if [[ "$f" == *ignore* ]]; then - echo "SKIP (not supported)" - continue - fi - - EXTRA_ARGS="" - if [[ "$f" == *bounds* ]]; then - EXTRA_ARGS+="--bounds-check" - fi - - rmc $f -- --object-bits 11 --unwind $UNWIND $EXTRA_ARGS > .sandbox/"$NAME".output - - CODE=$? - if [[ $CODE == 0 ]]; then - if [[ $NAME == *_fail* ]]; then - echo "FAIL (expected verify failure)" - EXIT_CODE=1 - else - echo "PASS" - fi - else - if [[ $NAME != *_fail* ]]; then - echo "FAIL (expected verify okay)" - EXIT_CODE=1 - else - echo "PASS" - fi - fi -done - -exit $EXIT_CODE diff --git a/scripts/rmc-regression.sh b/scripts/rmc-regression.sh index 553adbb4b8d0..96bbe50cafeb 100755 --- a/scripts/rmc-regression.sh +++ b/scripts/rmc-regression.sh @@ -23,14 +23,10 @@ check-cbmc-version.py --major 5 --minor 30 # Standalone rmc tests pushd $RUST_DIR ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS} -cd rust-tests -for TEST_DIR in cbmc-reg smack-regressions prusti-regressions; do - ./run.sh $TEST_DIR -done -./run.sh firecracker-like 2 +./x.py test -i --stage 1 cbmc firecracker prusti smack # Standalone cargo-rmc tests -cd ../cargo-rmc-tests +cd cargo-rmc-tests for DIR in */; do ./run.py $DIR done @@ -38,4 +34,3 @@ popd # run-make tests ./x.py test -i --stage 1 src/test/run-make --test-args gotoc -./x.py test -i --stage 1 src/test/cbmc diff --git a/src/bootstrap/builder.rs b/src/bootstrap/builder.rs index 40b93b0ab61a..5e293b0ed6fe 100644 --- a/src/bootstrap/builder.rs +++ b/src/bootstrap/builder.rs @@ -434,9 +434,14 @@ impl<'a> Builder<'a> { test::RustdocJson, // Run bootstrap close to the end as it's unlikely to fail test::Bootstrap, + // RMC regression tests + test::CBMC, + test::Firecracker, + test::Prusti, + test::Serial, + test::SMACK, // Run run-make last, since these won't pass without make on Windows test::RunMake, - test::CBMC, ), Kind::Bench => describe!(test::Crate, test::CrateLibrustc), Kind::Doc => describe!( diff --git a/src/bootstrap/test.rs b/src/bootstrap/test.rs index 1a53141ecb2b..a9ea48fad310 100644 --- a/src/bootstrap/test.rs +++ b/src/bootstrap/test.rs @@ -1123,6 +1123,14 @@ default_test!(Assembly { path: "src/test/assembly", mode: "assembly", suite: "as default_test!(CBMC { path: "src/test/cbmc", mode: "rmc", suite: "cbmc" }); +default_test!(Firecracker { path: "src/test/firecracker", mode: "rmc", suite: "firecracker" }); + +default_test!(Prusti { path: "src/test/prusti", mode: "rmc", suite: "prusti" }); + +default_test!(Serial { path: "src/test/serial", mode: "rmc", suite: "serial" }); + +default_test!(SMACK { path: "src/test/smack", mode: "rmc", suite: "smack" }); + #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] struct Compiletest { compiler: Compiler, diff --git a/rust-tests/cbmc-reg/ArithEqualOperators/main.rs b/src/test/cbmc/ArithEqualOperators/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/ArithEqualOperators/main.rs rename to src/test/cbmc/ArithEqualOperators/main.rs diff --git a/rust-tests/cbmc-reg/ArithOperators/main.rs b/src/test/cbmc/ArithOperators/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/ArithOperators/main.rs rename to src/test/cbmc/ArithOperators/main.rs diff --git a/rust-tests/cbmc-reg/Asm/main_fixme.rs b/src/test/cbmc/Asm/main_fixme.rs similarity index 100% rename from rust-tests/cbmc-reg/Asm/main_fixme.rs rename to src/test/cbmc/Asm/main_fixme.rs diff --git a/rust-tests/cbmc-reg/Assert/UninitValid/fixme_main_fail.rs b/src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Assert/UninitValid/fixme_main_fail.rs rename to src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs diff --git a/rust-tests/cbmc-reg/Assert/ZeroValid/fixme_main_fail.rs b/src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Assert/ZeroValid/fixme_main_fail.rs rename to src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs diff --git a/rust-tests/cbmc-reg/Assert/ZeroValid/main.rs b/src/test/cbmc/Assert/ZeroValid/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Assert/ZeroValid/main.rs rename to src/test/cbmc/Assert/ZeroValid/main.rs diff --git a/rust-tests/cbmc-reg/Assume/main.rs b/src/test/cbmc/Assume/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Assume/main.rs rename to src/test/cbmc/Assume/main.rs diff --git a/rust-tests/cbmc-reg/Assume/main_fail.rs b/src/test/cbmc/Assume/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Assume/main_fail.rs rename to src/test/cbmc/Assume/main_fail.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/CompareExchange/main.rs b/src/test/cbmc/Atomics/Stable/CompareExchange/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/CompareExchange/main.rs rename to src/test/cbmc/Atomics/Stable/CompareExchange/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/Fence/main.rs b/src/test/cbmc/Atomics/Stable/Fence/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/Fence/main.rs rename to src/test/cbmc/Atomics/Stable/Fence/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/FetchAdd/main.rs b/src/test/cbmc/Atomics/Stable/FetchAdd/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/FetchAdd/main.rs rename to src/test/cbmc/Atomics/Stable/FetchAdd/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/FetchAnd/main.rs b/src/test/cbmc/Atomics/Stable/FetchAnd/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/FetchAnd/main.rs rename to src/test/cbmc/Atomics/Stable/FetchAnd/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/FetchOr/main.rs b/src/test/cbmc/Atomics/Stable/FetchOr/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/FetchOr/main.rs rename to src/test/cbmc/Atomics/Stable/FetchOr/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/FetchSub/main.rs b/src/test/cbmc/Atomics/Stable/FetchSub/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/FetchSub/main.rs rename to src/test/cbmc/Atomics/Stable/FetchSub/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/FetchXor/main.rs b/src/test/cbmc/Atomics/Stable/FetchXor/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/FetchXor/main.rs rename to src/test/cbmc/Atomics/Stable/FetchXor/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/Load/main.rs b/src/test/cbmc/Atomics/Stable/Load/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/Load/main.rs rename to src/test/cbmc/Atomics/Stable/Load/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Stable/Store/main.rs b/src/test/cbmc/Atomics/Stable/Store/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Stable/Store/main.rs rename to src/test/cbmc/Atomics/Stable/Store/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicAdd/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicAdd/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicAdd/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicAdd/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicAnd/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicAnd/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicAnd/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicAnd/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicCxchg/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicCxchg/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicCxchg/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicCxchg/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicFence/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicFence/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicFence/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicFence/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicLoad/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicLoad/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicLoad/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicLoad/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicOr/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicOr/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicOr/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicOr/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicStore/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicStore/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicStore/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicStore/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicSub/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicSub/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicSub/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicSub/main.rs diff --git a/rust-tests/cbmc-reg/Atomics/Unstable/AtomicXor/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicXor/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Atomics/Unstable/AtomicXor/main.rs rename to src/test/cbmc/Atomics/Unstable/AtomicXor/main.rs diff --git a/rust-tests/cbmc-reg/BinOp_Offset/main.rs b/src/test/cbmc/BinOp_Offset/main.rs similarity index 100% rename from rust-tests/cbmc-reg/BinOp_Offset/main.rs rename to src/test/cbmc/BinOp_Offset/main.rs diff --git a/rust-tests/cbmc-reg/BinOp_Offset/main_fail.rs b/src/test/cbmc/BinOp_Offset/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/BinOp_Offset/main_fail.rs rename to src/test/cbmc/BinOp_Offset/main_fail.rs diff --git a/rust-tests/cbmc-reg/BitManipulation/Stable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/BitManipulation/Stable/fixme_main_fail.rs rename to src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs diff --git a/rust-tests/cbmc-reg/BitManipulation/Unstable/Rotate/main.rs b/src/test/cbmc/BitManipulation/Unstable/Rotate/main.rs similarity index 100% rename from rust-tests/cbmc-reg/BitManipulation/Unstable/Rotate/main.rs rename to src/test/cbmc/BitManipulation/Unstable/Rotate/main.rs diff --git a/rust-tests/cbmc-reg/BitManipulation/Unstable/fixme_main_fail.rs b/src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/BitManipulation/Unstable/fixme_main_fail.rs rename to src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs diff --git a/rust-tests/cbmc-reg/BitwiseArithOperators/main.rs b/src/test/cbmc/BitwiseArithOperators/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/BitwiseArithOperators/main.rs rename to src/test/cbmc/BitwiseArithOperators/main.rs diff --git a/rust-tests/cbmc-reg/BitwiseEqualOperators/main.rs b/src/test/cbmc/BitwiseEqualOperators/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/BitwiseEqualOperators/main.rs rename to src/test/cbmc/BitwiseEqualOperators/main.rs diff --git a/rust-tests/cbmc-reg/BitwiseShiftOperators/Usize/main.rs b/src/test/cbmc/BitwiseShiftOperators/Usize/main.rs similarity index 100% rename from rust-tests/cbmc-reg/BitwiseShiftOperators/Usize/main.rs rename to src/test/cbmc/BitwiseShiftOperators/Usize/main.rs diff --git a/rust-tests/cbmc-reg/BitwiseShiftOperators/main.rs b/src/test/cbmc/BitwiseShiftOperators/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/BitwiseShiftOperators/main.rs rename to src/test/cbmc/BitwiseShiftOperators/main.rs diff --git a/src/test/cbmc/Bool-BoolOperators/main.rs b/src/test/cbmc/Bool-BoolOperators/main.rs old mode 100755 new mode 100644 diff --git a/rust-tests/cbmc-reg/Cast/cast_abstract_args_to_concrete.rs b/src/test/cbmc/Cast/cast_abstract_args_to_concrete.rs similarity index 100% rename from rust-tests/cbmc-reg/Cast/cast_abstract_args_to_concrete.rs rename to src/test/cbmc/Cast/cast_abstract_args_to_concrete.rs diff --git a/rust-tests/cbmc-reg/Cast/from_be_bytes.rs b/src/test/cbmc/Cast/from_be_bytes.rs similarity index 100% rename from rust-tests/cbmc-reg/Cast/from_be_bytes.rs rename to src/test/cbmc/Cast/from_be_bytes.rs diff --git a/rust-tests/cbmc-reg/Cast/main.rs b/src/test/cbmc/Cast/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Cast/main.rs rename to src/test/cbmc/Cast/main.rs diff --git a/rust-tests/cbmc-reg/Cast/path.rs b/src/test/cbmc/Cast/path.rs similarity index 100% rename from rust-tests/cbmc-reg/Cast/path.rs rename to src/test/cbmc/Cast/path.rs diff --git a/rust-tests/cbmc-reg/Closure/main.rs b/src/test/cbmc/Closure/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Closure/main.rs rename to src/test/cbmc/Closure/main.rs diff --git a/rust-tests/cbmc-reg/CodegenConstValue/main.rs b/src/test/cbmc/CodegenConstValue/main.rs similarity index 100% rename from rust-tests/cbmc-reg/CodegenConstValue/main.rs rename to src/test/cbmc/CodegenConstValue/main.rs diff --git a/rust-tests/cbmc-reg/CodegenConstValue/u128.rs b/src/test/cbmc/CodegenConstValue/u128.rs similarity index 100% rename from rust-tests/cbmc-reg/CodegenConstValue/u128.rs rename to src/test/cbmc/CodegenConstValue/u128.rs diff --git a/rust-tests/cbmc-reg/CodegenMisc/main.rs b/src/test/cbmc/CodegenMisc/main.rs similarity index 100% rename from rust-tests/cbmc-reg/CodegenMisc/main.rs rename to src/test/cbmc/CodegenMisc/main.rs diff --git a/rust-tests/cbmc-reg/CodegenStatic/main.rs b/src/test/cbmc/CodegenStatic/main.rs similarity index 100% rename from rust-tests/cbmc-reg/CodegenStatic/main.rs rename to src/test/cbmc/CodegenStatic/main.rs diff --git a/rust-tests/cbmc-reg/CodegenStatic/struct.rs b/src/test/cbmc/CodegenStatic/struct.rs similarity index 100% rename from rust-tests/cbmc-reg/CodegenStatic/struct.rs rename to src/test/cbmc/CodegenStatic/struct.rs diff --git a/rust-tests/cbmc-reg/CopyIntrinsics/main.rs b/src/test/cbmc/CopyIntrinsics/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/CopyIntrinsics/main.rs rename to src/test/cbmc/CopyIntrinsics/main.rs diff --git a/rust-tests/cbmc-reg/Count/Unstable/Ctlz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs similarity index 95% rename from rust-tests/cbmc-reg/Count/Unstable/Ctlz/bounds_fail.rs rename to src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs index f28794464441..deb91a6646e7 100644 --- a/rust-tests/cbmc-reg/Count/Unstable/Ctlz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs @@ -1,9 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --bounds-check + #![feature(core_intrinsics)] use std::intrinsics::ctlz_nonzero; -/// rmc bounds_fail.rs -- --bounds-check fn main() { let uv8: u8 = 0; let uv16: u16 = 0; diff --git a/rust-tests/cbmc-reg/Count/Unstable/Ctlz/main.rs b/src/test/cbmc/Count/Unstable/Ctlz/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Count/Unstable/Ctlz/main.rs rename to src/test/cbmc/Count/Unstable/Ctlz/main.rs diff --git a/rust-tests/cbmc-reg/Count/Unstable/Cttz/bounds_fail.rs b/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs similarity index 95% rename from rust-tests/cbmc-reg/Count/Unstable/Cttz/bounds_fail.rs rename to src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs index f30a2e09b036..5fa791853c05 100644 --- a/rust-tests/cbmc-reg/Count/Unstable/Cttz/bounds_fail.rs +++ b/src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs @@ -1,9 +1,11 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --bounds-check + #![feature(core_intrinsics)] use std::intrinsics::cttz_nonzero; -/// rmc bounds_fail.rs -- --bounds-check fn main() { let uv8: u8 = 0; let uv16: u16 = 0; diff --git a/rust-tests/cbmc-reg/Count/Unstable/Cttz/main.rs b/src/test/cbmc/Count/Unstable/Cttz/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Count/Unstable/Cttz/main.rs rename to src/test/cbmc/Count/Unstable/Cttz/main.rs diff --git a/rust-tests/cbmc-reg/DynTrait/main.rs b/src/test/cbmc/DynTrait/main.rs similarity index 100% rename from rust-tests/cbmc-reg/DynTrait/main.rs rename to src/test/cbmc/DynTrait/main.rs diff --git a/rust-tests/cbmc-reg/DynTrait/main_fail.rs b/src/test/cbmc/DynTrait/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/DynTrait/main_fail.rs rename to src/test/cbmc/DynTrait/main_fail.rs diff --git a/rust-tests/cbmc-reg/DynTrait/object_safe_trait.rs b/src/test/cbmc/DynTrait/object_safe_trait.rs similarity index 100% rename from rust-tests/cbmc-reg/DynTrait/object_safe_trait.rs rename to src/test/cbmc/DynTrait/object_safe_trait.rs diff --git a/rust-tests/cbmc-reg/DynTrait/vtable_duplicate_fields_fixme.rs b/src/test/cbmc/DynTrait/vtable_duplicate_fields_fixme.rs similarity index 100% rename from rust-tests/cbmc-reg/DynTrait/vtable_duplicate_fields_fixme.rs rename to src/test/cbmc/DynTrait/vtable_duplicate_fields_fixme.rs diff --git a/rust-tests/cbmc-reg/EQ-NE/main.rs b/src/test/cbmc/EQ-NE/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/EQ-NE/main.rs rename to src/test/cbmc/EQ-NE/main.rs diff --git a/rust-tests/cbmc-reg/Enum/main.rs b/src/test/cbmc/Enum/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/main.rs rename to src/test/cbmc/Enum/main.rs diff --git a/rust-tests/cbmc-reg/Enum/result1.rs b/src/test/cbmc/Enum/result1.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/result1.rs rename to src/test/cbmc/Enum/result1.rs diff --git a/rust-tests/cbmc-reg/Enum/result2.rs b/src/test/cbmc/Enum/result2.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/result2.rs rename to src/test/cbmc/Enum/result2.rs diff --git a/rust-tests/cbmc-reg/Enum/result3.rs b/src/test/cbmc/Enum/result3.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/result3.rs rename to src/test/cbmc/Enum/result3.rs diff --git a/rust-tests/cbmc-reg/Enum/variants_multiple_len_2.rs b/src/test/cbmc/Enum/variants_multiple_len_2.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/variants_multiple_len_2.rs rename to src/test/cbmc/Enum/variants_multiple_len_2.rs diff --git a/rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_0.rs b/src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_0.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_0.rs rename to src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_0.rs diff --git a/rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_1.rs b/src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_1.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_1.rs rename to src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_1.rs diff --git a/rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_2.rs b/src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_2.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/variants_single_len_1_fields_arbitrary_2.rs rename to src/test/cbmc/Enum/variants_single_len_1_fields_arbitrary_2.rs diff --git a/rust-tests/cbmc-reg/Enum/variants_single_len_2_fields_arbitrary_1.rs b/src/test/cbmc/Enum/variants_single_len_2_fields_arbitrary_1.rs similarity index 100% rename from rust-tests/cbmc-reg/Enum/variants_single_len_2_fields_arbitrary_1.rs rename to src/test/cbmc/Enum/variants_single_len_2_fields_arbitrary_1.rs diff --git a/rust-tests/cbmc-reg/ExactDiv/main.rs b/src/test/cbmc/ExactDiv/main.rs similarity index 100% rename from rust-tests/cbmc-reg/ExactDiv/main.rs rename to src/test/cbmc/ExactDiv/main.rs diff --git a/rust-tests/cbmc-reg/FatPointers/boxmuttrait.rs b/src/test/cbmc/FatPointers/boxmuttrait.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/boxmuttrait.rs rename to src/test/cbmc/FatPointers/boxmuttrait.rs diff --git a/rust-tests/cbmc-reg/FatPointers/boxslice1.rs b/src/test/cbmc/FatPointers/boxslice1.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/boxslice1.rs rename to src/test/cbmc/FatPointers/boxslice1.rs diff --git a/rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs b/src/test/cbmc/FatPointers/boxslice2_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/boxslice2_fail.rs rename to src/test/cbmc/FatPointers/boxslice2_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/boxtrait.rs b/src/test/cbmc/FatPointers/boxtrait.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/boxtrait.rs rename to src/test/cbmc/FatPointers/boxtrait.rs diff --git a/rust-tests/cbmc-reg/FatPointers/boxtrait_fail.rs b/src/test/cbmc/FatPointers/boxtrait_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/boxtrait_fail.rs rename to src/test/cbmc/FatPointers/boxtrait_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_boxmuttrait_fail.rs b/src/test/cbmc/FatPointers/fixme_boxmuttrait_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_boxmuttrait_fail.rs rename to src/test/cbmc/FatPointers/fixme_boxmuttrait_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_slice2.rs b/src/test/cbmc/FatPointers/fixme_slice2.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_slice2.rs rename to src/test/cbmc/FatPointers/fixme_slice2.rs diff --git a/rust-tests/cbmc-reg/FatPointers/slice1.rs b/src/test/cbmc/FatPointers/slice1.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/slice1.rs rename to src/test/cbmc/FatPointers/slice1.rs diff --git a/rust-tests/cbmc-reg/FatPointers/slice3.rs b/src/test/cbmc/FatPointers/slice3.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/slice3.rs rename to src/test/cbmc/FatPointers/slice3.rs diff --git a/rust-tests/cbmc-reg/FatPointers/structslice.rs b/src/test/cbmc/FatPointers/structslice.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/structslice.rs rename to src/test/cbmc/FatPointers/structslice.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait1.rs b/src/test/cbmc/FatPointers/trait1.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait1.rs rename to src/test/cbmc/FatPointers/trait1.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait1_fail.rs b/src/test/cbmc/FatPointers/trait1_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait1_fail.rs rename to src/test/cbmc/FatPointers/trait1_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait2.rs b/src/test/cbmc/FatPointers/trait2.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait2.rs rename to src/test/cbmc/FatPointers/trait2.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait2_fail.rs b/src/test/cbmc/FatPointers/trait2_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait2_fail.rs rename to src/test/cbmc/FatPointers/trait2_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait3.rs b/src/test/cbmc/FatPointers/trait3.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait3.rs rename to src/test/cbmc/FatPointers/trait3.rs diff --git a/rust-tests/cbmc-reg/FatPointers/trait3_fail.rs b/src/test/cbmc/FatPointers/trait3_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/trait3_fail.rs rename to src/test/cbmc/FatPointers/trait3_fail.rs diff --git a/rust-tests/cbmc-reg/FloatingPoint/main.rs b/src/test/cbmc/FloatingPoint/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/FloatingPoint/main.rs rename to src/test/cbmc/FloatingPoint/main.rs diff --git a/rust-tests/cbmc-reg/ForeignItems/fixme_main.rs b/src/test/cbmc/ForeignItems/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/ForeignItems/fixme_main.rs rename to src/test/cbmc/ForeignItems/fixme_main.rs diff --git a/rust-tests/cbmc-reg/ForeignItems/fixme_varadic.rs b/src/test/cbmc/ForeignItems/fixme_varadic.rs similarity index 100% rename from rust-tests/cbmc-reg/ForeignItems/fixme_varadic.rs rename to src/test/cbmc/ForeignItems/fixme_varadic.rs diff --git a/rust-tests/cbmc-reg/ForeignItems/lib.c b/src/test/cbmc/ForeignItems/lib.c similarity index 100% rename from rust-tests/cbmc-reg/ForeignItems/lib.c rename to src/test/cbmc/ForeignItems/lib.c diff --git a/rust-tests/cbmc-reg/FunctionCall/FnPtr/main.rs b/src/test/cbmc/FunctionCall/FnPtr/main.rs similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall/FnPtr/main.rs rename to src/test/cbmc/FunctionCall/FnPtr/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall/Variadic/fixme_main.rs b/src/test/cbmc/FunctionCall/Variadic/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall/Variadic/fixme_main.rs rename to src/test/cbmc/FunctionCall/Variadic/fixme_main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall/Variadic/main.rs b/src/test/cbmc/FunctionCall/Variadic/main.rs similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall/Variadic/main.rs rename to src/test/cbmc/FunctionCall/Variadic/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall_ImplicitReturn/main.rs b/src/test/cbmc/FunctionCall_ImplicitReturn/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall_ImplicitReturn/main.rs rename to src/test/cbmc/FunctionCall_ImplicitReturn/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall_NoRet-NoParam/main.rs b/src/test/cbmc/FunctionCall_NoRet-NoParam/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall_NoRet-NoParam/main.rs rename to src/test/cbmc/FunctionCall_NoRet-NoParam/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall_NoRet-Param/main.rs b/src/test/cbmc/FunctionCall_NoRet-Param/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall_NoRet-Param/main.rs rename to src/test/cbmc/FunctionCall_NoRet-Param/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall_Ret-NoParam/main.rs b/src/test/cbmc/FunctionCall_Ret-NoParam/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/FunctionCall_Ret-NoParam/main.rs rename to src/test/cbmc/FunctionCall_Ret-NoParam/main.rs diff --git a/rust-tests/cbmc-reg/FunctionCall_Ret-Param/main.rs b/src/test/cbmc/FunctionCall_Ret-Param/main.rs old mode 100755 new mode 100644 similarity index 97% rename from rust-tests/cbmc-reg/FunctionCall_Ret-Param/main.rs rename to src/test/cbmc/FunctionCall_Ret-Param/main.rs index 383a5bc5c6a3..955e5c45aa13 --- a/rust-tests/cbmc-reg/FunctionCall_Ret-Param/main.rs +++ b/src/test/cbmc/FunctionCall_Ret-Param/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 10 + fn __nondet() -> T { unimplemented!() } diff --git a/rust-tests/cbmc-reg/IfElseifElse_NonReturning/main.rs b/src/test/cbmc/IfElseifElse_NonReturning/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/IfElseifElse_NonReturning/main.rs rename to src/test/cbmc/IfElseifElse_NonReturning/main.rs diff --git a/rust-tests/cbmc-reg/IfElseifElse_Returning/main.rs b/src/test/cbmc/IfElseifElse_Returning/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/IfElseifElse_Returning/main.rs rename to src/test/cbmc/IfElseifElse_Returning/main.rs diff --git a/rust-tests/cbmc-reg/Intrinsics/abort_fail.rs b/src/test/cbmc/Intrinsics/abort_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Intrinsics/abort_fail.rs rename to src/test/cbmc/Intrinsics/abort_fail.rs diff --git a/rust-tests/cbmc-reg/LT-GT-LE-GE/main.rs b/src/test/cbmc/LT-GT-LE-GE/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/LT-GT-LE-GE/main.rs rename to src/test/cbmc/LT-GT-LE-GE/main.rs diff --git a/rust-tests/cbmc-reg/LoopLoop_NonReturning/main.rs b/src/test/cbmc/LoopLoop_NonReturning/main.rs old mode 100755 new mode 100644 similarity index 87% rename from rust-tests/cbmc-reg/LoopLoop_NonReturning/main.rs rename to src/test/cbmc/LoopLoop_NonReturning/main.rs index e43c9c01d8bc..2d58260c728f --- a/rust-tests/cbmc-reg/LoopLoop_NonReturning/main.rs +++ b/src/test/cbmc/LoopLoop_NonReturning/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 10 --unwinding-assertions + fn __nondet() -> T { unimplemented!() } diff --git a/rust-tests/cbmc-reg/LoopWhile_NonReturning/main.rs b/src/test/cbmc/LoopWhile_NonReturning/main.rs old mode 100755 new mode 100644 similarity index 85% rename from rust-tests/cbmc-reg/LoopWhile_NonReturning/main.rs rename to src/test/cbmc/LoopWhile_NonReturning/main.rs index fa9247a0fde8..7c9805c727fa --- a/rust-tests/cbmc-reg/LoopWhile_NonReturning/main.rs +++ b/src/test/cbmc/LoopWhile_NonReturning/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 11 --unwinding-assertions + fn __nondet() -> T { unimplemented!() } diff --git a/rust-tests/cbmc-reg/MemReplace/main.rs b/src/test/cbmc/MemReplace/main.rs similarity index 100% rename from rust-tests/cbmc-reg/MemReplace/main.rs rename to src/test/cbmc/MemReplace/main.rs diff --git a/rust-tests/cbmc-reg/NondetVectors/bytes.rs b/src/test/cbmc/NondetVectors/bytes.rs similarity index 100% rename from rust-tests/cbmc-reg/NondetVectors/bytes.rs rename to src/test/cbmc/NondetVectors/bytes.rs diff --git a/rust-tests/cbmc-reg/NondetVectors/fixme_main.rs b/src/test/cbmc/NondetVectors/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/NondetVectors/fixme_main.rs rename to src/test/cbmc/NondetVectors/fixme_main.rs diff --git a/rust-tests/cbmc-reg/Parenths/main.rs b/src/test/cbmc/Parenths/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Parenths/main.rs rename to src/test/cbmc/Parenths/main.rs diff --git a/rust-tests/cbmc-reg/PointerOffset/Stable/main.rs b/src/test/cbmc/PointerOffset/Stable/main.rs similarity index 100% rename from rust-tests/cbmc-reg/PointerOffset/Stable/main.rs rename to src/test/cbmc/PointerOffset/Stable/main.rs diff --git a/rust-tests/cbmc-reg/PointerOffset/Unstable/main.rs b/src/test/cbmc/PointerOffset/Unstable/main.rs similarity index 100% rename from rust-tests/cbmc-reg/PointerOffset/Unstable/main.rs rename to src/test/cbmc/PointerOffset/Unstable/main.rs diff --git a/rust-tests/cbmc-reg/PointerOffset/Unstable/main_fail.rs b/src/test/cbmc/PointerOffset/Unstable/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/PointerOffset/Unstable/main_fail.rs rename to src/test/cbmc/PointerOffset/Unstable/main_fail.rs diff --git a/rust-tests/cbmc-reg/Pointers_Basic/fixme_from_raw_fail.rs b/src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Pointers_Basic/fixme_from_raw_fail.rs rename to src/test/cbmc/Pointers_Basic/fixme_from_raw_fail.rs diff --git a/rust-tests/cbmc-reg/Pointers_Basic/main.rs b/src/test/cbmc/Pointers_Basic/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Pointers_Basic/main.rs rename to src/test/cbmc/Pointers_Basic/main.rs diff --git a/rust-tests/cbmc-reg/Pointers_Functions/main.rs b/src/test/cbmc/Pointers_Functions/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Pointers_Functions/main.rs rename to src/test/cbmc/Pointers_Functions/main.rs diff --git a/rust-tests/cbmc-reg/Pointers_InAssert/main.rs b/src/test/cbmc/Pointers_InAssert/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Pointers_InAssert/main.rs rename to src/test/cbmc/Pointers_InAssert/main.rs diff --git a/rust-tests/cbmc-reg/Pointers_OtherTypes/main.rs b/src/test/cbmc/Pointers_OtherTypes/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Pointers_OtherTypes/main.rs rename to src/test/cbmc/Pointers_OtherTypes/main.rs diff --git a/rust-tests/cbmc-reg/Pointers_OutOfScopeFail/fixme_main_fail.rs b/src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Pointers_OutOfScopeFail/fixme_main_fail.rs rename to src/test/cbmc/Pointers_OutOfScopeFail/fixme_main_fail.rs diff --git a/rust-tests/cbmc-reg/ProjectionElem/ConstantIndex/main.rs b/src/test/cbmc/ProjectionElem/ConstantIndex/main.rs similarity index 100% rename from rust-tests/cbmc-reg/ProjectionElem/ConstantIndex/main.rs rename to src/test/cbmc/ProjectionElem/ConstantIndex/main.rs diff --git a/rust-tests/cbmc-reg/Refs/fixme_main.rs b/src/test/cbmc/Refs/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/Refs/fixme_main.rs rename to src/test/cbmc/Refs/fixme_main.rs diff --git a/rust-tests/cbmc-reg/Repr/main.rs b/src/test/cbmc/Repr/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Repr/main.rs rename to src/test/cbmc/Repr/main.rs diff --git a/rust-tests/cbmc-reg/SIMD/Compare/main_fail.rs b/src/test/cbmc/SIMD/Compare/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/SIMD/Compare/main_fail.rs rename to src/test/cbmc/SIMD/Compare/main_fail.rs diff --git a/rust-tests/cbmc-reg/SIMD/Operators/main.rs b/src/test/cbmc/SIMD/Operators/main.rs similarity index 100% rename from rust-tests/cbmc-reg/SIMD/Operators/main.rs rename to src/test/cbmc/SIMD/Operators/main.rs diff --git a/rust-tests/cbmc-reg/SaturatingIntrinsics/fixme_128.rs b/src/test/cbmc/SaturatingIntrinsics/fixme_128.rs similarity index 100% rename from rust-tests/cbmc-reg/SaturatingIntrinsics/fixme_128.rs rename to src/test/cbmc/SaturatingIntrinsics/fixme_128.rs diff --git a/rust-tests/cbmc-reg/SaturatingIntrinsics/main.rs b/src/test/cbmc/SaturatingIntrinsics/main.rs similarity index 100% rename from rust-tests/cbmc-reg/SaturatingIntrinsics/main.rs rename to src/test/cbmc/SaturatingIntrinsics/main.rs diff --git a/rust-tests/cbmc-reg/Scopes_NonReturning/main.rs b/src/test/cbmc/Scopes_NonReturning/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Scopes_NonReturning/main.rs rename to src/test/cbmc/Scopes_NonReturning/main.rs diff --git a/rust-tests/cbmc-reg/Scopes_Returning/main.rs b/src/test/cbmc/Scopes_Returning/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/Scopes_Returning/main.rs rename to src/test/cbmc/Scopes_Returning/main.rs diff --git a/rust-tests/cbmc-reg/Serde/main_fail.rs b/src/test/cbmc/Serde/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Serde/main_fail.rs rename to src/test/cbmc/Serde/main_fail.rs diff --git a/rust-tests/cbmc-reg/SizeAndAlignOfDst/main.rs b/src/test/cbmc/SizeAndAlignOfDst/main.rs similarity index 100% rename from rust-tests/cbmc-reg/SizeAndAlignOfDst/main.rs rename to src/test/cbmc/SizeAndAlignOfDst/main.rs diff --git a/rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs b/src/test/cbmc/SizeAndAlignOfDst/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs rename to src/test/cbmc/SizeAndAlignOfDst/main_fail.rs diff --git a/rust-tests/cbmc-reg/Slice/codegen.rs b/src/test/cbmc/Slice/codegen.rs similarity index 100% rename from rust-tests/cbmc-reg/Slice/codegen.rs rename to src/test/cbmc/Slice/codegen.rs diff --git a/rust-tests/cbmc-reg/Slice/drop_in_place_fail.rs b/src/test/cbmc/Slice/drop_in_place_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Slice/drop_in_place_fail.rs rename to src/test/cbmc/Slice/drop_in_place_fail.rs diff --git a/rust-tests/cbmc-reg/Slice/main.rs b/src/test/cbmc/Slice/main.rs similarity index 78% rename from rust-tests/cbmc-reg/Slice/main.rs rename to src/test/cbmc/Slice/main.rs index bd78a56de91a..419493b77b57 100644 --- a/rust-tests/cbmc-reg/Slice/main.rs +++ b/src/test/cbmc/Slice/main.rs @@ -1,6 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -/// rmc main.rs -- --unwind 6 --unwinding-assertions + +// cbmc-flags: --unwind 6 --unwinding-assertions + fn main() { let name: &str = "hello"; assert!(name == "hello"); diff --git a/rust-tests/cbmc-reg/Slice/pathbuf_fail.rs b/src/test/cbmc/Slice/pathbuf_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Slice/pathbuf_fail.rs rename to src/test/cbmc/Slice/pathbuf_fail.rs diff --git a/rust-tests/cbmc-reg/Slice/slice.rs b/src/test/cbmc/Slice/slice.rs similarity index 100% rename from rust-tests/cbmc-reg/Slice/slice.rs rename to src/test/cbmc/Slice/slice.rs diff --git a/rust-tests/cbmc-reg/Slice/slice_from_raw_fail.rs b/src/test/cbmc/Slice/slice_from_raw_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/Slice/slice_from_raw_fail.rs rename to src/test/cbmc/Slice/slice_from_raw_fail.rs diff --git a/rust-tests/cbmc-reg/Static/main.rs b/src/test/cbmc/Static/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Static/main.rs rename to src/test/cbmc/Static/main.rs diff --git a/rust-tests/cbmc-reg/Static/table_of_pairs.rs b/src/test/cbmc/Static/table_of_pairs.rs similarity index 100% rename from rust-tests/cbmc-reg/Static/table_of_pairs.rs rename to src/test/cbmc/Static/table_of_pairs.rs diff --git a/rust-tests/cbmc-reg/Static/table_of_pairs2.rs b/src/test/cbmc/Static/table_of_pairs2.rs similarity index 100% rename from rust-tests/cbmc-reg/Static/table_of_pairs2.rs rename to src/test/cbmc/Static/table_of_pairs2.rs diff --git a/rust-tests/cbmc-reg/Strings/fixme_boxed_str.rs b/src/test/cbmc/Strings/fixme_boxed_str.rs similarity index 100% rename from rust-tests/cbmc-reg/Strings/fixme_boxed_str.rs rename to src/test/cbmc/Strings/fixme_boxed_str.rs diff --git a/rust-tests/cbmc-reg/Strings/fixme_main.rs b/src/test/cbmc/Strings/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/Strings/fixme_main.rs rename to src/test/cbmc/Strings/fixme_main.rs diff --git a/rust-tests/cbmc-reg/Strings/fixme_os_str.rs b/src/test/cbmc/Strings/fixme_os_str.rs similarity index 100% rename from rust-tests/cbmc-reg/Strings/fixme_os_str.rs rename to src/test/cbmc/Strings/fixme_os_str.rs diff --git a/rust-tests/cbmc-reg/Strings/main.rs b/src/test/cbmc/Strings/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Strings/main.rs rename to src/test/cbmc/Strings/main.rs diff --git a/rust-tests/cbmc-reg/Strings/os_str_reduced.rs b/src/test/cbmc/Strings/os_str_reduced.rs similarity index 100% rename from rust-tests/cbmc-reg/Strings/os_str_reduced.rs rename to src/test/cbmc/Strings/os_str_reduced.rs diff --git a/rust-tests/cbmc-reg/SwitchInt/main.rs b/src/test/cbmc/SwitchInt/main.rs similarity index 93% rename from rust-tests/cbmc-reg/SwitchInt/main.rs rename to src/test/cbmc/SwitchInt/main.rs index f3077a46efe7..b16413d70175 100644 --- a/rust-tests/cbmc-reg/SwitchInt/main.rs +++ b/src/test/cbmc/SwitchInt/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 2 --unwinding-assertions + fn doswitch_int() -> i32 { for i in [99].iter() { if *i == 99 { diff --git a/rust-tests/cbmc-reg/Transparent/transparent1.rs b/src/test/cbmc/Transparent/transparent1.rs similarity index 100% rename from rust-tests/cbmc-reg/Transparent/transparent1.rs rename to src/test/cbmc/Transparent/transparent1.rs diff --git a/rust-tests/cbmc-reg/Transparent/transparent2.rs b/src/test/cbmc/Transparent/transparent2.rs similarity index 100% rename from rust-tests/cbmc-reg/Transparent/transparent2.rs rename to src/test/cbmc/Transparent/transparent2.rs diff --git a/rust-tests/cbmc-reg/Transparent/transparent3.rs b/src/test/cbmc/Transparent/transparent3.rs similarity index 100% rename from rust-tests/cbmc-reg/Transparent/transparent3.rs rename to src/test/cbmc/Transparent/transparent3.rs diff --git a/rust-tests/cbmc-reg/Transparent/transparent4.rs b/src/test/cbmc/Transparent/transparent4.rs similarity index 100% rename from rust-tests/cbmc-reg/Transparent/transparent4.rs rename to src/test/cbmc/Transparent/transparent4.rs diff --git a/rust-tests/cbmc-reg/Unit/main.rs b/src/test/cbmc/Unit/main.rs similarity index 100% rename from rust-tests/cbmc-reg/Unit/main.rs rename to src/test/cbmc/Unit/main.rs diff --git a/rust-tests/cbmc-reg/UnsafeBlocks_Useless/main.rs b/src/test/cbmc/UnsafeBlocks_Useless/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/UnsafeBlocks_Useless/main.rs rename to src/test/cbmc/UnsafeBlocks_Useless/main.rs diff --git a/rust-tests/cbmc-reg/Vectors/fixme_main.rs b/src/test/cbmc/Vectors/fixme_main.rs similarity index 100% rename from rust-tests/cbmc-reg/Vectors/fixme_main.rs rename to src/test/cbmc/Vectors/fixme_main.rs diff --git a/rust-tests/cbmc-reg/VolatileIntrinsics/main.rs b/src/test/cbmc/VolatileIntrinsics/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/VolatileIntrinsics/main.rs rename to src/test/cbmc/VolatileIntrinsics/main.rs diff --git a/rust-tests/cbmc-reg/Whitespace/main.rs b/src/test/cbmc/Whitespace/main.rs similarity index 84% rename from rust-tests/cbmc-reg/Whitespace/main.rs rename to src/test/cbmc/Whitespace/main.rs index e24839e9cd4d..b602f93ad621 100644 --- a/rust-tests/cbmc-reg/Whitespace/main.rs +++ b/src/test/cbmc/Whitespace/main.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 2 --unwinding-assertions + fn main() { let mut iter = "A few words".split_whitespace(); match iter.next() { diff --git a/rust-tests/cbmc-reg/i32-Unary-/main.rs b/src/test/cbmc/i32-Unary-/main.rs old mode 100755 new mode 100644 similarity index 100% rename from rust-tests/cbmc-reg/i32-Unary-/main.rs rename to src/test/cbmc/i32-Unary-/main.rs diff --git a/rust-tests/firecracker-like/micro-http-parsed-request/ignore-main.rs b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs similarity index 100% rename from rust-tests/firecracker-like/micro-http-parsed-request/ignore-main.rs rename to src/test/firecracker/micro-http-parsed-request/ignore-main.rs diff --git a/rust-tests/firecracker-like/virtio-balloon-compact/ignore-main.rs b/src/test/firecracker/virtio-balloon-compact/ignore-main.rs similarity index 100% rename from rust-tests/firecracker-like/virtio-balloon-compact/ignore-main.rs rename to src/test/firecracker/virtio-balloon-compact/ignore-main.rs diff --git a/rust-tests/firecracker-like/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs similarity index 100% rename from rust-tests/firecracker-like/virtio-block-parse/main.rs rename to src/test/firecracker/virtio-block-parse/main.rs diff --git a/rust-tests/prusti-regressions/100_doors.rs b/src/test/prusti/100_doors.rs similarity index 100% rename from rust-tests/prusti-regressions/100_doors.rs rename to src/test/prusti/100_doors.rs diff --git a/rust-tests/prusti-regressions/Ackermann_function.rs b/src/test/prusti/Ackermann_function.rs similarity index 100% rename from rust-tests/prusti-regressions/Ackermann_function.rs rename to src/test/prusti/Ackermann_function.rs diff --git a/rust-tests/prusti-regressions/Binary_search_fail.rs b/src/test/prusti/Binary_search_fail.rs similarity index 96% rename from rust-tests/prusti-regressions/Binary_search_fail.rs rename to src/test/prusti/Binary_search_fail.rs index 3dc870a560e0..5f1ac6da17aa 100644 --- a/rust-tests/prusti-regressions/Binary_search_fail.rs +++ b/src/test/prusti/Binary_search_fail.rs @@ -1,5 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// cbmc-flags: --unwind 4 --unwinding-assertions + use std::cmp::Ordering::*; /// this is interestingly a wrong implementation at diff --git a/rust-tests/prusti-regressions/Fibonacci_sequence.rs b/src/test/prusti/Fibonacci_sequence.rs similarity index 100% rename from rust-tests/prusti-regressions/Fibonacci_sequence.rs rename to src/test/prusti/Fibonacci_sequence.rs diff --git a/rust-tests/prusti-regressions/Heapsort.rs b/src/test/prusti/Heapsort.rs similarity index 100% rename from rust-tests/prusti-regressions/Heapsort.rs rename to src/test/prusti/Heapsort.rs diff --git a/rust-tests/prusti-regressions/Selection_sort.rs b/src/test/prusti/Selection_sort.rs similarity index 100% rename from rust-tests/prusti-regressions/Selection_sort.rs rename to src/test/prusti/Selection_sort.rs diff --git a/rust-tests/prusti-regressions/Tower_of_Hanoi.rs b/src/test/prusti/Tower_of_Hanoi.rs similarity index 100% rename from rust-tests/prusti-regressions/Tower_of_Hanoi.rs rename to src/test/prusti/Tower_of_Hanoi.rs diff --git a/rust-tests/prusti-regressions/borrow_first.rs b/src/test/prusti/borrow_first.rs similarity index 100% rename from rust-tests/prusti-regressions/borrow_first.rs rename to src/test/prusti/borrow_first.rs diff --git a/rust-tests/serial/serial.rs b/src/test/serial/serial.rs similarity index 100% rename from rust-tests/serial/serial.rs rename to src/test/serial/serial.rs diff --git a/rust-tests/serial/serial2.rs b/src/test/serial/serial2.rs similarity index 100% rename from rust-tests/serial/serial2.rs rename to src/test/serial/serial2.rs diff --git a/rust-tests/serial/serial3.rs b/src/test/serial/serial3.rs similarity index 100% rename from rust-tests/serial/serial3.rs rename to src/test/serial/serial3.rs diff --git a/rust-tests/serial/serial4.rs b/src/test/serial/serial4.rs similarity index 100% rename from rust-tests/serial/serial4.rs rename to src/test/serial/serial4.rs diff --git a/rust-tests/serial/serial_spec.rs b/src/test/serial/serial_spec.rs similarity index 100% rename from rust-tests/serial/serial_spec.rs rename to src/test/serial/serial_spec.rs diff --git a/rust-tests/smack-regressions/basic/add_fail.rs b/src/test/smack/basic/add_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/add_fail.rs rename to src/test/smack/basic/add_fail.rs diff --git a/rust-tests/smack-regressions/basic/arith.rs b/src/test/smack/basic/arith.rs similarity index 100% rename from rust-tests/smack-regressions/basic/arith.rs rename to src/test/smack/basic/arith.rs diff --git a/rust-tests/smack-regressions/basic/arith_assume.rs b/src/test/smack/basic/arith_assume.rs similarity index 100% rename from rust-tests/smack-regressions/basic/arith_assume.rs rename to src/test/smack/basic/arith_assume.rs diff --git a/rust-tests/smack-regressions/basic/arith_assume2.rs b/src/test/smack/basic/arith_assume2.rs similarity index 100% rename from rust-tests/smack-regressions/basic/arith_assume2.rs rename to src/test/smack/basic/arith_assume2.rs diff --git a/rust-tests/smack-regressions/basic/arith_assume_fail.rs b/src/test/smack/basic/arith_assume_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/arith_assume_fail.rs rename to src/test/smack/basic/arith_assume_fail.rs diff --git a/rust-tests/smack-regressions/basic/div_fail.rs b/src/test/smack/basic/div_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/div_fail.rs rename to src/test/smack/basic/div_fail.rs diff --git a/rust-tests/smack-regressions/basic/mod_fail.rs b/src/test/smack/basic/mod_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/mod_fail.rs rename to src/test/smack/basic/mod_fail.rs diff --git a/rust-tests/smack-regressions/basic/mul_fail.rs b/src/test/smack/basic/mul_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/mul_fail.rs rename to src/test/smack/basic/mul_fail.rs diff --git a/rust-tests/smack-regressions/basic/sub_fail.rs b/src/test/smack/basic/sub_fail.rs similarity index 100% rename from rust-tests/smack-regressions/basic/sub_fail.rs rename to src/test/smack/basic/sub_fail.rs diff --git a/rust-tests/smack-regressions/functions/closure.rs b/src/test/smack/functions/closure.rs similarity index 100% rename from rust-tests/smack-regressions/functions/closure.rs rename to src/test/smack/functions/closure.rs diff --git a/rust-tests/smack-regressions/functions/closure_fail.rs b/src/test/smack/functions/closure_fail.rs similarity index 100% rename from rust-tests/smack-regressions/functions/closure_fail.rs rename to src/test/smack/functions/closure_fail.rs diff --git a/rust-tests/smack-regressions/functions/double.rs b/src/test/smack/functions/double.rs similarity index 100% rename from rust-tests/smack-regressions/functions/double.rs rename to src/test/smack/functions/double.rs diff --git a/rust-tests/smack-regressions/functions/double_fail.rs b/src/test/smack/functions/double_fail.rs similarity index 100% rename from rust-tests/smack-regressions/functions/double_fail.rs rename to src/test/smack/functions/double_fail.rs diff --git a/rust-tests/smack-regressions/generics/generic_function.rs b/src/test/smack/generics/generic_function.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function.rs rename to src/test/smack/generics/generic_function.rs diff --git a/rust-tests/smack-regressions/generics/generic_function_fail1.rs b/src/test/smack/generics/generic_function_fail1.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function_fail1.rs rename to src/test/smack/generics/generic_function_fail1.rs diff --git a/rust-tests/smack-regressions/generics/generic_function_fail2.rs b/src/test/smack/generics/generic_function_fail2.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function_fail2.rs rename to src/test/smack/generics/generic_function_fail2.rs diff --git a/rust-tests/smack-regressions/generics/generic_function_fail3.rs b/src/test/smack/generics/generic_function_fail3.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function_fail3.rs rename to src/test/smack/generics/generic_function_fail3.rs diff --git a/rust-tests/smack-regressions/generics/generic_function_fail4.rs b/src/test/smack/generics/generic_function_fail4.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function_fail4.rs rename to src/test/smack/generics/generic_function_fail4.rs diff --git a/rust-tests/smack-regressions/generics/generic_function_fail5.rs b/src/test/smack/generics/generic_function_fail5.rs similarity index 100% rename from rust-tests/smack-regressions/generics/generic_function_fail5.rs rename to src/test/smack/generics/generic_function_fail5.rs diff --git a/rust-tests/smack-regressions/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs similarity index 89% rename from rust-tests/smack-regressions/loops/gauss_sum_nondet.rs rename to src/test/smack/loops/gauss_sum_nondet.rs index aa0d2446521f..72688943b60d 100644 --- a/rust-tests/smack-regressions/loops/gauss_sum_nondet.rs +++ b/src/test/smack/loops/gauss_sum_nondet.rs @@ -3,6 +3,8 @@ // @flag --no-memory-splitting --unroll=4 // @expect verified +// cbmc-flags: --unwind 5 --unwinding-assertions + fn __nondet() -> T { unimplemented!() } diff --git a/rust-tests/smack-regressions/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs similarity index 89% rename from rust-tests/smack-regressions/loops/gauss_sum_nondet_fail.rs rename to src/test/smack/loops/gauss_sum_nondet_fail.rs index a50c0b7cb613..4bd53d7861ff 100644 --- a/rust-tests/smack-regressions/loops/gauss_sum_nondet_fail.rs +++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs @@ -3,6 +3,8 @@ // @flag --no-memory-splitting --unroll=10 // @expect error +// cbmc-flags: --unwind 5 --unwinding-assertions + fn __nondet() -> T { unimplemented!() } diff --git a/rust-tests/smack-regressions/loops/iterator.rs b/src/test/smack/loops/iterator.rs similarity index 91% rename from rust-tests/smack-regressions/loops/iterator.rs rename to src/test/smack/loops/iterator.rs index 11a3c9a76ed2..08724bbbfa8d 100644 --- a/rust-tests/smack-regressions/loops/iterator.rs +++ b/src/test/smack/loops/iterator.rs @@ -3,6 +3,8 @@ // @flag --no-memory-splitting --unroll=4 // @expect verified +// cbmc-flags: --unwind 5 --unwinding-assertions + fn fac(n: u64) -> u64 { match n { 0 => 1, diff --git a/rust-tests/smack-regressions/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs similarity index 91% rename from rust-tests/smack-regressions/loops/iterator_fail.rs rename to src/test/smack/loops/iterator_fail.rs index fa0ae9c1a111..141fb82a692a 100644 --- a/rust-tests/smack-regressions/loops/iterator_fail.rs +++ b/src/test/smack/loops/iterator_fail.rs @@ -3,6 +3,8 @@ // @flag --no-memory-splitting --unroll=10 // @expect error +// cbmc-flags: --unwind 5 --unwinding-assertions + fn fac(n: u64) -> u64 { match n { 0 => 1, diff --git a/rust-tests/smack-regressions/overflow/add_overflow_fail.rs b/src/test/smack/overflow/add_overflow_fail.rs similarity index 100% rename from rust-tests/smack-regressions/overflow/add_overflow_fail.rs rename to src/test/smack/overflow/add_overflow_fail.rs diff --git a/rust-tests/smack-regressions/overflow/mul_overflow_fail.rs b/src/test/smack/overflow/mul_overflow_fail.rs similarity index 100% rename from rust-tests/smack-regressions/overflow/mul_overflow_fail.rs rename to src/test/smack/overflow/mul_overflow_fail.rs diff --git a/rust-tests/smack-regressions/overflow/sub_overflow_fail.rs b/src/test/smack/overflow/sub_overflow_fail.rs similarity index 100% rename from rust-tests/smack-regressions/overflow/sub_overflow_fail.rs rename to src/test/smack/overflow/sub_overflow_fail.rs diff --git a/rust-tests/smack-regressions/recursion/fac.rs b/src/test/smack/recursion/fac.rs similarity index 100% rename from rust-tests/smack-regressions/recursion/fac.rs rename to src/test/smack/recursion/fac.rs diff --git a/rust-tests/smack-regressions/recursion/fac_fail.rs b/src/test/smack/recursion/fac_fail.rs similarity index 100% rename from rust-tests/smack-regressions/recursion/fac_fail.rs rename to src/test/smack/recursion/fac_fail.rs diff --git a/rust-tests/smack-regressions/recursion/fib.rs b/src/test/smack/recursion/fib.rs similarity index 100% rename from rust-tests/smack-regressions/recursion/fib.rs rename to src/test/smack/recursion/fib.rs diff --git a/rust-tests/smack-regressions/recursion/fib_fail.rs b/src/test/smack/recursion/fib_fail.rs similarity index 100% rename from rust-tests/smack-regressions/recursion/fib_fail.rs rename to src/test/smack/recursion/fib_fail.rs diff --git a/rust-tests/smack-regressions/structures/option.rs b/src/test/smack/structures/option.rs similarity index 100% rename from rust-tests/smack-regressions/structures/option.rs rename to src/test/smack/structures/option.rs diff --git a/rust-tests/smack-regressions/structures/option_fail.rs b/src/test/smack/structures/option_fail.rs similarity index 100% rename from rust-tests/smack-regressions/structures/option_fail.rs rename to src/test/smack/structures/option_fail.rs diff --git a/rust-tests/smack-regressions/structures/point.rs b/src/test/smack/structures/point.rs similarity index 100% rename from rust-tests/smack-regressions/structures/point.rs rename to src/test/smack/structures/point.rs diff --git a/rust-tests/smack-regressions/structures/point_fail.rs b/src/test/smack/structures/point_fail.rs similarity index 100% rename from rust-tests/smack-regressions/structures/point_fail.rs rename to src/test/smack/structures/point_fail.rs diff --git a/rust-tests/smack-regressions/vector/vec1.rs b/src/test/smack/vector/vec1.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec1.rs rename to src/test/smack/vector/vec1.rs diff --git a/rust-tests/smack-regressions/vector/vec1_fail1.rs b/src/test/smack/vector/vec1_fail1.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec1_fail1.rs rename to src/test/smack/vector/vec1_fail1.rs diff --git a/rust-tests/smack-regressions/vector/vec1_fail2.rs b/src/test/smack/vector/vec1_fail2.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec1_fail2.rs rename to src/test/smack/vector/vec1_fail2.rs diff --git a/rust-tests/smack-regressions/vector/vec1_fail3.rs b/src/test/smack/vector/vec1_fail3.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec1_fail3.rs rename to src/test/smack/vector/vec1_fail3.rs diff --git a/rust-tests/smack-regressions/vector/vec_resize.rs b/src/test/smack/vector/vec_resize.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec_resize.rs rename to src/test/smack/vector/vec_resize.rs diff --git a/rust-tests/smack-regressions/vector/vec_resize_fail.rs b/src/test/smack/vector/vec_resize_fail.rs similarity index 100% rename from rust-tests/smack-regressions/vector/vec_resize_fail.rs rename to src/test/smack/vector/vec_resize_fail.rs diff --git a/src/tools/compiletest/src/header.rs b/src/tools/compiletest/src/header.rs index 983934d129a2..3b2764fb88a4 100644 --- a/src/tools/compiletest/src/header.rs +++ b/src/tools/compiletest/src/header.rs @@ -51,6 +51,14 @@ impl EarlyProps { let has_tsan = util::TSAN_SUPPORTED_TARGETS.contains(&&*config.target); let has_hwasan = util::HWASAN_SUPPORTED_TARGETS.contains(&&*config.target); + if config.mode == Mode::RMC { + // If the path to the test contains "fixme" or "ignore", skip it. + let path = testfile.to_str().unwrap(); + if path.contains("fixme") || path.contains("ignore") { + props.ignore = true; + } + } + iter_header(testfile, None, rdr, &mut |ln| { // we should check if any only- exists and if it exists // and does not matches the current platform, skip the test @@ -277,6 +285,10 @@ pub struct TestProps { pub error_patterns: Vec, // Extra flags to pass to the compiler pub compile_flags: Vec, + // Extra flags to pass to RMC + pub rmc_flags: Vec, + // Extra flags to pass to CBMC + pub cbmc_flags: Vec, // Extra flags to pass when the compiled code is run (such as --bench) pub run_flags: Option, // If present, the name of a file that this test should match when @@ -360,6 +372,8 @@ impl TestProps { TestProps { error_patterns: vec![], compile_flags: vec![], + rmc_flags: vec![], + cbmc_flags: vec![], run_flags: None, pp_exact: None, aux_builds: vec![], @@ -436,6 +450,14 @@ impl TestProps { self.compile_flags.extend(flags.split_whitespace().map(|s| s.to_owned())); } + if let Some(flags) = config.parse_rmc_flags(ln) { + self.rmc_flags.extend(flags.split_whitespace().map(|s| s.to_owned())); + } + + if let Some(flags) = config.parse_cbmc_flags(ln) { + self.cbmc_flags.extend(flags.split_whitespace().map(|s| s.to_owned())); + } + if let Some(edition) = config.parse_edition(ln) { self.compile_flags.push(format!("--edition={}", edition)); } @@ -729,6 +751,16 @@ impl Config { self.parse_name_value_directive(line, "compile-flags") } + /// Parses strings of the form `// rmc-flags: ...` and returns the options listed after `rmc-flags:` + fn parse_rmc_flags(&self, line: &str) -> Option { + self.parse_name_value_directive(line, "rmc-flags") + } + + /// Parses strings of the form `// cbmc-flags: ...` and returns the options listed after `cbmc-flags:` + fn parse_cbmc_flags(&self, line: &str) -> Option { + self.parse_name_value_directive(line, "cbmc-flags") + } + fn parse_and_update_revisions(&self, line: &str, existing: &mut Vec) { if let Some(raw) = self.parse_name_value_directive(line, "revisions") { let mut duplicates: HashSet<_> = existing.iter().cloned().collect(); diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index f3bbcd0961d9..99f431b6bdec 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -396,6 +396,7 @@ impl<'test> TestCx<'test> { panic!("revision name must begin with rpass, rfail, or cfail"); } } + RMC => !self.testpaths.file.to_str().unwrap().contains("fail"), mode => panic!("unimplemented for mode {:?}", mode), } } @@ -2382,19 +2383,30 @@ impl<'test> TestCx<'test> { } } - /// Runs RMC on the test file specified by `self.testpaths.file`. - /// An error message is printed to stdout if verfication fails. + /// Runs RMC on the test file specified by `self.testpaths.file`. An error + /// message is printed to stdout if verification result is not expected. fn run_rmc_test(&self) { // Other modes call self.compile_test(...). However, we cannot call it here for two reasons: // 1. It calls rustc instead of RMC // 2. It may pass some options that do not make sense for RMC // So we create our own command to execute RMC and pass it to self.compose_and_run_compiler(...) directly. let mut rmc = Command::new("rmc"); + // Pass the test path along with RMC and CBMC flags parsed from comments at the top of the test file. + rmc.args(&self.props.rmc_flags) + .arg(&self.testpaths.file) + .arg("--") + .args(&self.props.cbmc_flags); self.add_rmc_dir_to_path(&mut rmc); - rmc.arg(&self.testpaths.file); let proc_res = self.compose_and_run_compiler(rmc, None); - if !proc_res.status.success() { - self.fatal_proc_rec("verification failed!", &proc_res); + // Print an error if the verification result is not expected. + if self.should_compile_successfully(self.pass_mode()) { + if !proc_res.status.success() { + self.fatal_proc_rec("test failed: expected success, got failure", &proc_res); + } + } else { + if proc_res.status.success() { + self.fatal_proc_rec("test failed: expected failure, got success", &proc_res); + } } }