I will have to make another tarball, I had left a debugging trace. Sorry about that.
commit 25b3d0e1a3f97a33615099e4b211f3953990c203 Author: Akim Demaille <akim.demai...@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