diff options
| author | Paul E. McKenney <paulmck@kernel.org> | 2019-03-18 11:53:50 -0700 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-03-24 10:24:13 -0700 |
| commit | 2c644d3f6536dd31f2378529c44a04ad77ea6b77 (patch) | |
| tree | 3236216d75181a6b26228f7dc8390a81bf8dc60a /tools/memory-model | |
| parent | 7e7eb5ae4e4cd482a1ebc6a82ea8a04c5ead62ee (diff) | |
tools/memory-model: Make judgelitmus.sh note timeouts
Currently, judgelitmus.sh treats timeouts (as in the "--timeout" argument)
as "!!! Verification error". This can be misleading because it is quite
possible that running the test longer would have produced a verification.
This commit therefore changes judgelitmus.sh to check for timeouts and
to report them with "!!! Timeout".
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model')
| -rwxr-xr-x | tools/memory-model/scripts/judgelitmus.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 0cc63875e395..d3c313b9a458 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -42,6 +42,14 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out then : +elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out +then + echo ' !!! Timeout' $litmus + if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + then + echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1 + fi + exit 124 else echo ' !!! Verification error' $litmus if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out |