rcutorture: Add CBMC-based formal verification for SRCU

This commit creates a formal/srcu-cbmc directory containing scripts that
pull SRCU in from the source code, filter it to remove things that CBMC
cannot handle, and run a series of verifications on it.  This has a number
of shortcomings:

1.	It does not yet hook into the upper-level self-test Makefiles.
2.	It tests only a single scenario, store buffering.
3.	There is no gcc-based syntax-error prefiltering.

Nevertheless, it does fully verify a piece of SRCU under a moderately
weak memory model (PSO).

Signed-off-by: Lance Roy <ldr709@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

1 files changed, 11 insertions, 0 deletions

diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
new file mode 100644
index 000000000000..ca892e3b2351
--- /dev/null
+++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.c
@@ -0,0 +1,11 @@
+#include <config.h>
+
+#include "misc.h"
+#include "bug_on.h"
+
+struct rcu_head;
+
+void wakeme_after_rcu(struct rcu_head *head)
+{
+	BUG();
+}