aboutsummaryrefslogtreecommitdiffstatshomepage
path: root/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail
diff options
context:
space:
mode:
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail')
-rw-r--r--tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail1
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail
deleted file mode 100644
index 8fe00c8db466..000000000000
--- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/store_buffering/force2.fail
+++ /dev/null
@@ -1 +0,0 @@
-test_cbmc_options="-DFORCE_FAILURE_2"