diff options
Diffstat (limited to 'tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c')
| -rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c new file mode 100644 index 000000000000..29eb5d2697ed --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c @@ -0,0 +1,13 @@ +#include <config.h> + +/* Include all source files. */ + +#include "include_srcu.c" + +#include "preempt.c" +#include "misc.c" + +/* Used by test.c files */ +#include <pthread.h> +#include <stdlib.h> +#include <linux/srcu.h> |