diff options
| author | Akim Demaille <akim.demaille@gmail.com> | 2021-01-14 06:32:39 +0100 |
|---|---|---|
| committer | Akim Demaille <akim.demaille@gmail.com> | 2021-01-23 09:40:32 +0100 |
| commit | 7a31b6bb7f24d925851be1849dbf1dbbd3b69826 (patch) | |
| tree | 3bcca0387eed815033372b16cece9d3aa3aa46bb /src | |
| parent | 8320691a63ca3bccb21360f780db0e727b6e6567 (diff) | |
| download | bison-7a31b6bb7f24d925851be1849dbf1dbbd3b69826.tar.gz | |
cex: add support for $TIME_LIMIT
* src/counterexample.c (TIME_LIMIT): Replace with...
(time_limit): this.
(counterexample_init): Check $TIME_LIMIT.
* src/scan-gram.l: Reorder includes.
Diffstat (limited to 'src')
| -rw-r--r-- | src/counterexample.c | 18 | ||||
| -rw-r--r-- | src/scan-gram.l | 3 |
2 files changed, 17 insertions, 4 deletions
diff --git a/src/counterexample.c b/src/counterexample.c index 8a19aa51..b4caef7d 100644 --- a/src/counterexample.c +++ b/src/counterexample.c @@ -23,6 +23,7 @@ #include "system.h" +#include <errno.h> #include <gl_linked_list.h> #include <gl_rbtreehash_list.h> #include <hash.h> @@ -59,7 +60,7 @@ #define ASSURANCE_LIMIT 2.0f /* The time limit before giving up looking for unifying counterexample. */ -#define TIME_LIMIT 5.0f +static float time_limit = 5.0f; #define CUMULATIVE_TIME_LIMIT 120.0f @@ -1171,7 +1172,7 @@ unifying_example (state_item_number itm1, stderr); assurance_printed = true; } - if (time_passed > TIME_LIMIT) + if (time_passed > time_limit) { fprintf (stderr, "time limit exceeded: %f\n", time_passed); goto cex_search_end; @@ -1208,6 +1209,19 @@ static time_t cumulative_time; void counterexample_init (void) { + /* Recognize $TIME_LIMIT. Not a public feature, just to help + debugging. If we need something public, a %define/-D/-F variable + would be more appropriate. */ + { + const char *cp = getenv ("TIME_LIMIT"); + if (cp) + { + char *end = NULL; + float v = strtof (cp, &end); + if (*end == '\0' && errno == 0) + time_limit = v; + } + } time (&cumulative_time); scp_set = bitset_create (nstates, BITSET_FIXED); rpp_set = bitset_create (nstates, BITSET_FIXED); diff --git a/src/scan-gram.l b/src/scan-gram.l index e10d68e2..6d33cdf2 100644 --- a/src/scan-gram.l +++ b/src/scan-gram.l @@ -21,9 +21,8 @@ %option prefix="gram_" outfile="lex.yy.c" %{ -#include <errno.h> - #include <c-ctype.h> +#include <errno.h> #include <mbswidth.h> #include <quote.h> #include <quotearg.h> |