Skip to content

Commit a546905

Browse files
zhassan-awstedinski
authored andcommitted
Enabled CBMC unknown language mode test now that rust-lang#533 has been fixed (rust-lang#650)
* Enabled CBMC unknown language mode test now that rust-lang#533 has been fixed and migrated it to a cargo-rmc test
1 parent 33bdc58 commit a546905

File tree

6 files changed

+2
-44
lines changed

6 files changed

+2
-44
lines changed

scripts/rmc-regression.sh

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -55,10 +55,6 @@ time "$RMC_DIR"/src/test/rmc-dependency-test/diamond-dependency/run-dependency-t
5555
# Check that we don't have type mismatches across different crates
5656
time "$RMC_DIR"/src/test/rmc-multicrate/type-mismatch/run-mismatch-test.sh
5757

58-
# Check that CBMC issue #6341 is fixed
59-
# Disabled till https://github.com/model-checking/rmc/issues/533 is fixed
60-
#time "$RMC_DIR"/src/test/rmc-multicrate/cbmc-unknown-lang-mode/run-cbmc-unknown-lang-mode.sh
61-
6258
echo
6359
echo "All RMC regression tests completed successfully."
6460
echo

src/test/rmc-multicrate/cbmc-unknown-lang-mode/unknown-lang-mode/Cargo.toml renamed to src/test/cargo-rmc/cbmc-unknown-lang-mode/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[package]
5-
name = "unknown-lang-mode"
5+
name = "cbmc-unknown-lang-mode"
66
version = "0.1.0"
77
edition = "2018"
88

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
VERIFICATION SUCCESSFUL

src/test/rmc-multicrate/cbmc-unknown-lang-mode/run-cbmc-unknown-lang-mode.sh

Lines changed: 0 additions & 38 deletions
This file was deleted.

src/test/rmc-multicrate/type-mismatch/run-mismatch-test.sh

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ export CARGO_TARGET_DIR=/tmp/type_mismatch_test_build
2121
export RUST_BACKTRACE=1
2222
cargo rmc &> $RESULT
2323

24-
# Run the solver
2524
if ! grep -q "VERIFICATION SUCCESSFUL" $RESULT; then
2625
cat $RESULT
2726
echo

0 commit comments

Comments
 (0)