Better error reporting when res is not what is expected

c.f. https://dev.azure.com/coq/coq/_build/results?buildId=6485&view=logs&jobId=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&j=2d2b3007-3c5c-5840-9bb0-2b1ea49925f3&t=77aad734-2057-5694-9ae2-ee1f5f26eae8

1 files changed, 17 insertions, 11 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7e2ef3bc75..1546b7cf62 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -540,19 +540,25 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	    echo "    $<...Error! (couldn't find a time measure)"; \
 	  else \
 	    true "express effective time in centiseconds"; \
+	    resorig="$$res"; \
 	    res=`echo "$$res"00 | sed -n -e "s/\([0-9]*\)\.\([0-9][0-9]\).*/\1\2/p"`; \
-	    true "find expected time * 100"; \
-	    exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \
-	    true "compute corrected effective time, rounded up"; \
-	    rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \
-	    ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \
-	    if [ "$$ok" = 1 ]; then \
-	      echo $(log_success); \
-	      echo "    $<...Ok"; \
-	    else \
+	    if [ "$$res" = "" ]; then \
 	      echo $(log_failure); \
-	      echo "    $<...Error! (should run faster ($$rescorrected >= $$exp))"; \
-	      $(FAIL); \
+	      echo "    $<...Error! (invalid time measure: $$resorig)"; \
+	    else \
+	      true "find expected time * 100"; \
+	      exp=`sed -n -e "s/(\*.*Expected time < \([0-9]\).\([0-9][0-9]\)s.*\*)/\1\2/p" "$<"`; \
+	      true "compute corrected effective time, rounded up"; \
+	      rescorrected=`expr \( $$res \* $(bogomips) + 6120 - 1 \) / 6120`; \
+	      ok=`expr \( $$res \* $(bogomips) \) "<" \( $$exp \* 6120 \)`; \
+	      if [ "$$ok" = 1 ]; then \
+	        echo $(log_success); \
+	        echo "    $<...Ok"; \
+	      else \
+	        echo $(log_failure); \
+	        echo "    $<...Error! (should run faster ($$rescorrected >= $$exp))"; \
+	        $(FAIL); \
+	      fi; \
 	    fi; \
 	  fi; \
 	} > "$@"