summaryrefslogtreecommitdiff
path: root/tools/memory-model
diff options
context:
space:
mode:
authorPaul E. McKenney <paulmck@kernel.org>2019-04-05 12:34:56 -0700
committerPaul E. McKenney <paulmck@kernel.org>2023-03-24 10:24:14 -0700
commitd9313e05f08dea8cf9f7a67662d642ba47f8040a (patch)
tree6d4b45ed34dc22ab892627dfee460e345c69a990 /tools/memory-model
parenta9504aaa9b0d6906741be69c001722a4d1cbbf1e (diff)
tools/memory-model: Add -v flag to jingle7 runs
Adding the -v flag to jingle7 invocations gives much useful information on why jingle7 didn't like a given litmus test. This commit therefore adds this flag and saves off any such information into a .err file. Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model')
-rwxr-xr-xtools/memory-model/scripts/runlitmus.sh5
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 5f2d29b460ff..dfdb1f00fcc0 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -68,10 +68,11 @@ fi
# Generate the assembly code and run herd7 on it.
gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
-jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
+jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
then
- echo ' !!! ' jingle7 failed, no $hwlitmus generated
+ echo ' !!! ' jingle7 failed, errors in $hwlitmus.err
+ cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
exit 253
fi
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1