diff options
author | Paul E. McKenney <paulmck@kernel.org> | 2019-03-18 13:40:57 -0700 |
---|---|---|
committer | Paul E. McKenney <paulmck@kernel.org> | 2023-03-24 10:24:13 -0700 |
commit | 02484d826fda923f829fc47350ee99fd3cbd3414 (patch) | |
tree | 7f8aaa865aa0c218aa66f6eff81e184ec379eb70 /tools/memory-model/scripts/judgelitmus.sh | |
parent | b1da11c936e28d60a02f13c9ea27fdc3d1759b38 (diff) |
tools/memory-model: Make judgelitmus.sh identify bad macros
Currently, judgelitmus.sh treats use of unknown primitives (such as
srcu_read_lock() prior to SRCU support) as "!!! Verification error".
This can be misleading because it fails to call out typos and running
a version LKMM on a litmus test requiring a feature not provided by
that version. This commit therefore changes judgelitmus.sh to check
for unknown primitives and to report them, for example, with:
'!!! Current LKMM version does not know "rcu_write_lock"'.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model/scripts/judgelitmus.sh')
-rwxr-xr-x | tools/memory-model/scripts/judgelitmus.sh | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index d3c313b9a458..d40439c7b71e 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -42,6 +42,18 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out then : +elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out +then + badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus" + echo $badmsg + if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + then + echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1 + fi + exit 254 elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out then echo ' !!! Timeout' $litmus |