From 29809be8d72cdc2c364b5d3ee8bc5272ca0cd5e2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 21 Jul 2020 15:32:58 +0200
Subject: [PATCH] [ptests] use CPU user time for measuring timeout instead of
 wall clock

---
 doc/developer/advance.tex     | 3 ++-
 ptests/ptests.ml              | 4 ++--
 tests/syntax/string_concat.c  | 2 +-
 tests/syntax/wstring_concat.c | 2 +-
 4 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 2489c968a19..54d485f04fa 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -991,7 +991,8 @@ test
 & \textit{None}
 \\
 & \texttt{TIMEOUT}\nscodeidxdef{Test!Directive}{TIMEOUT}
-& kill the test after the given duration and report a failure
+& kill the test after the given duration (in seconds of CPU user time)
+and report a failure
 & \textit{None}
 \\
 & \texttt{NOFRAMAC}\nscodeidxdef{Test!Directive}{NOFRAMAC}
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 36fb036537e..78469525850 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1037,7 +1037,7 @@ let basic_command_string =
       end
     in
     if command.timeout = "" then raw_command
-    else "timeout " ^ command.timeout ^ " " ^ raw_command
+    else "ulimit -t " ^ command.timeout ^ " && " ^ raw_command
 
 (* Searches for executable [s] in the directories contained in the PATH
    environment variable. Returns [None] if not found, or
@@ -1128,7 +1128,7 @@ let command_string command =
     | "" -> command_string
     | s ->
       Printf.sprintf
-        "%s; if test $? -eq 124; then \
+        "%s; if test $? -gt 127; then \
          echo 'TIMEOUT (%s); ABORTING EXECUTION' > %s; \
          fi"
         command_string s (Filename.sanitize stderr)
diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c
index 9669f9687ef..8073c72f04c 100644
--- a/tests/syntax/string_concat.c
+++ b/tests/syntax/string_concat.c
@@ -1,5 +1,5 @@
 /* run.config*
-TIMEOUT: 45s
+TIMEOUT: 45
 OPT: -eva
 */
 
diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c
index 86d7d3ff4ea..4c72ed31cce 100644
--- a/tests/syntax/wstring_concat.c
+++ b/tests/syntax/wstring_concat.c
@@ -1,5 +1,5 @@
 /* run.config*
-TIMEOUT: 45s
+TIMEOUT: 45
 OPT: -eva
 */
 
-- 
GitLab