cex: check -Dcex.timeout

* src/counterexample.c (counterexample_init): Remove stray debug
trace.
Complain about invalid values.
* tests/input.at (-Dcex.timeout): New.
This commit is contained in:
Akim Demaille
2022-09-20 08:19:02 +02:00
parent de3041b69a
commit 25b3d0e1a3
2 changed files with 48 additions and 3 deletions

View File

@@ -30,6 +30,7 @@
#include <gl_rbtreehash_list.h> #include <gl_rbtreehash_list.h>
#include <hash.h> #include <hash.h>
#include <mbswidth.h> #include <mbswidth.h>
#include <quote.h>
#include <stdlib.h> #include <stdlib.h>
#include <textstyle.h> #include <textstyle.h>
#include <time.h> #include <time.h>
@@ -1209,15 +1210,23 @@ static xtime_t cumulative_time;
void void
counterexample_init (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') if (*cp != '\0')
{ {
char *end = NULL; char *end = NULL;
double v = c_strtod (cp, &end); double v = c_strtod (cp, &end);
if (*end == '\0' && errno == 0) if (*end == '\0' && errno == 0 && v >= 0)
time_limit = v; 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); free (cp);
} }

View File

@@ -3283,3 +3283,39 @@ AT_TEST([-M foo= -M baz], [baz], [<command line>:6])
m4_popdef([AT_TEST]) m4_popdef([AT_TEST])
AT_CLEANUP 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