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>

0 files changed, 0 insertions, 0 deletions