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 | 14 |
1 files changed, 14 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 000000000..e67ee5b3d --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/combined_source.c @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: GPL-2.0 +#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> |