[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PATCH 09/22] cex: add support for $TIME_LIMIT
From: |
Akim Demaille |
Subject: |
[PATCH 09/22] cex: add support for $TIME_LIMIT |
Date: |
Sat, 23 Jan 2021 15:55:48 +0100 |
* src/counterexample.c (TIME_LIMIT): Replace with...
(time_limit): this.
(counterexample_init): Check $TIME_LIMIT.
* src/scan-gram.l: Reorder includes.
---
src/counterexample.c | 18 ++++++++++++++++--
src/scan-gram.l | 3 +--
2 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/counterexample.c b/src/counterexample.c
index 8a19aa51b..b4caef7d7 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 e10d68e2a..6d33cdf23 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>
--
2.30.0
- [PATCH 00/22] maint: prepare 3.7.5, Akim Demaille, 2021/01/23
- [PATCH 01/22] c: adjust _Noreturn to pedantic clang, Akim Demaille, 2021/01/23
- [PATCH 02/22] autoconf: update, Akim Demaille, 2021/01/23
- [PATCH 03/22] examples: avoid "unbound variable" errors, Akim Demaille, 2021/01/23
- [PATCH 04/22] c++: use noexcept where appropriate, Akim Demaille, 2021/01/23
- [PATCH 05/22] tables: avoid warnings and save bits, Akim Demaille, 2021/01/23
- [PATCH 06/22] glr.cc: don't "leak" yyparse, Akim Demaille, 2021/01/23
- [PATCH 07/22] c++: I'm tired of Flex's warnings, Akim Demaille, 2021/01/23
- [PATCH 08/22] cex: send traces to stderr, not stdout, Akim Demaille, 2021/01/23
- [PATCH 09/22] cex: add support for $TIME_LIMIT,
Akim Demaille <=
- [PATCH 10/22] cex: fix traces: add missing end-of-lines, Akim Demaille, 2021/01/23
- [PATCH 11/22] cex: fix traces: fix display of disabled items, Akim Demaille, 2021/01/23
- [PATCH 12/22] package: codespell, Akim Demaille, 2021/01/23
- [PATCH 13/22] style: YYUSE is private, make it YY_USE, Akim Demaille, 2021/01/23
- [PATCH 14/22] skeletons: introduce "slot"s for symbols, Akim Demaille, 2021/01/23
- [PATCH 15/22] %merge: clearer tests on diagnostics, Akim Demaille, 2021/01/23
- [PATCH 16/22] %merge: let mergers record a typing-symbol, rather than a type, Akim Demaille, 2021/01/23
- [PATCH 17/22] %merge: delegate the generation of calls to mergers to m4, Akim Demaille, 2021/01/23
- [PATCH 18/22] %merge: fix compatibility with api.value.type=union, Akim Demaille, 2021/01/23
- [PATCH 19/22] %merge: associate it to its first definition, not the latest, Akim Demaille, 2021/01/23