diff options
| author | Paul E. McKenney <paulmck@kernel.org> | 2023-05-11 19:12:16 -0700 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-07-14 15:10:56 -0700 |
| commit | 1304affd35739d83b4089a297d39ab08f1624158 (patch) | |
| tree | 3c39a66766165a5983eeac72a6fc017ee7ac8aec /tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h | |
| parent | 965167e8e6c9877390bb9574f88da21dc42f03eb (diff) | |
rcu: Remove formal-verification tests
The CBMC-based formal-verification testing for SRCU was quite the thing
back in 2016, but the problem is that SRCU changes too quickly for the
scripting to keep up. In addition, more recently, SRCU's grace-period
ordering has been formally modeled by a group of Linux-kernel memory-model
litmus tests.
This commit therefore removes the pioneering formal-verification tests.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h')
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h deleted file mode 100644 index 5e7912c6a521..000000000000 --- a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/bug_on.h +++ /dev/null @@ -1,14 +0,0 @@ -/* SPDX-License-Identifier: GPL-2.0 */ -#ifndef BUG_ON_H -#define BUG_ON_H - -#include <assert.h> - -#define BUG() assert(0) -#define BUG_ON(x) assert(!(x)) - -/* Does it make sense to treat warnings as errors? */ -#define WARN() BUG() -#define WARN_ON(x) (BUG_ON(x), false) - -#endif |