Re: Counterexamples timeout

[Akim Demaille]

I will have to make another tarball, I had left a debugging trace.  Sorry about 
that.


commit 25b3d0e1a3f97a33615099e4b211f3953990c203
Author: Akim Demaille <akim.demaille@gmail.com>
Date:   Tue Sep 20 08:19:02 2022 +0200

    cex: check -Dcex.timeout
    
    * src/counterexample.c (counterexample_init): Remove stray debug
    trace.
    Complain about invalid values.
    * tests/input.at (-Dcex.timeout): New.

diff --git a/src/counterexample.c b/src/counterexample.c
index 8a4f8b2c..82ee43da 100644
--- a/src/counterexample.c
+++ b/src/counterexample.c
@@ -30,6 +30,7 @@
 #include <gl_rbtreehash_list.h>
 #include <hash.h>
 #include <mbswidth.h>
+#include <quote.h>
 #include <stdlib.h>
 #include <textstyle.h>
 #include <time.h>
@@ -1209,15 +1210,23 @@ static xtime_t cumulative_time;
 void
 counterexample_init (void)
 {
+  // Check cex.timeout.
   {
-    char *cp = muscle_percent_define_get ("cex.timeout");
+    const char *variable = "cex.timeout";
+    char *cp = muscle_percent_define_get (variable);
     if (*cp != '\0')
       {
         char *end = NULL;
         double v = c_strtod (cp, &end);
-        if (*end == '\0' && errno == 0)
+        if (*end == '\0' && errno == 0 && v >= 0)
           time_limit = v;
-        fprintf (stderr, "lim: %f from %s\n", time_limit, cp);
+        else
+          {
+            location loc = muscle_percent_define_get_loc (variable);
+            complain (&loc, complaint,
+                      _("invalid value for %%define variable %s: %s"),
+                      quote (variable), quote_n (1, cp));
+          }
       }
     free (cp);
   }
diff --git a/tests/input.at b/tests/input.at
index 5cacb066..04b31f99 100644
--- a/tests/input.at
+++ b/tests/input.at
@@ -3283,3 +3283,39 @@ m4_pushdef([AT_TEST],
 m4_popdef([AT_TEST])
 
 AT_CLEANUP
+
+
+## --------------- ##
+## -Dcex.timeout.  ##
+## --------------- ##
+
+AT_SETUP([[-Dcex.timeout]])
+
+AT_KEYWORDS([cex])
+
+# AT_TEST(OPTIONS)
+# ----------------
+m4_pushdef([AT_TEST],
+[AT_DATA([[input.y]],
+[[
+%%
+exp: %empty;
+]])
+AT_BISON_CHECK([[$1 input.y]], [[$2]], [[]], [m4_ifvaln([$3], [$3])])
+])
+
+# It's ok to define the timeout even if we don't run -Wcex.
+AT_TEST([-Dcex.timeout=1], [0])
+AT_TEST([-Dcex.timeout=1 -Wcex], [0])
+AT_TEST([-Dcex.timeout=1.5 -Wcex], [0])
+# No time at all.  Not really wrong.
+AT_TEST([-Dcex.timeout=0 -Wcex], [0])
+
+AT_TEST([-Dcex.timeout=foo -Wcex], [1],
+        [[<command line>:3: error: invalid value for %define variable 
'cex.timeout': 'foo']])
+AT_TEST([-Dcex.timeout=-1.5 -Wcex], [1],
+        [[<command line>:3: error: invalid value for %define variable 
'cex.timeout': '-1.5']])
+
+m4_popdef([AT_TEST])
+
+AT_CLEANUP