cex: add support for $TIME_LIMIT

commit 82133a610319a512c3ff69753628f039ad68cd8c
Author: Akim Demaille <[email protected]>
Date:   Thu Jan 14 06:32:39 2021 +0100

    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.

diff --git a/src/counterexample.c b/src/counterexample.c
index f38c7fd6..8cf56135 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
 
@@ -1172,7 +1173,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;
@@ -1209,6 +1210,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 aabdc5f5..c84d2b98 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>