Isolate: Fix bug in time measurement without --cg

diff --git a/isolate/isolate.c b/isolate/isolate.c
index fff31f4bb4235bb142d0957b2b5a5260a624b7fa..15b06488beb3756a437c21a5dfc087243f5a9117 100644 (file)
--- a/isolate/isolate.c
+++ b/isolate/isolate.c
@@ -70,7 +70,7 @@ static int read_errors_from_fd;
 static void die(char *msg, ...) NONRET;
 static void cg_stats(void);
 static int get_wall_time_ms(void);
 static void die(char *msg, ...) NONRET;
 static void cg_stats(void);
 static int get_wall_time_ms(void);

-static int get_run_time_ms(void);
+static int get_run_time_ms(struct rusage *rus);

 
 /*** Meta-files ***/
 
 
 /*** Meta-files ***/
 


@@ -111,7 +111,7 @@ meta_printf(const char *fmt, ...)
 static void
 final_stats(struct rusage *rus)
 {
 static void
 final_stats(struct rusage *rus)
 {

-  total_ms = get_run_time_ms();
+  total_ms = get_run_time_ms(rus);

   wall_ms = get_wall_time_ms();
 
   meta_printf("time:%d.%03d\n", total_ms/1000, total_ms%1000);
   wall_ms = get_wall_time_ms();
 
   meta_printf("time:%d.%03d\n", total_ms/1000, total_ms%1000);


@@ -613,11 +613,18 @@ get_wall_time_ms(void)
 }
 
 static int
 }
 
 static int

-get_run_time_ms(void)
+get_run_time_ms(struct rusage *rus)

 {
   if (cg_timing)
     return cg_get_run_time_ms();
 
 {
   if (cg_timing)
     return cg_get_run_time_ms();
 

+  if (rus)
+    {
+      struct timeval total;
+      timeradd(&rus->ru_utime, &rus->ru_stime, &total);
+      return total.tv_sec*1000 + total.tv_usec/1000;
+    }
+

   char buf[PROC_BUF_SIZE], *x;
   int utime, stime;
   static int proc_stat_fd;
   char buf[PROC_BUF_SIZE], *x;
   int utime, stime;
   static int proc_stat_fd;


@@ -653,7 +660,7 @@ check_timeout(void)
     }
   if (timeout)
     {
     }
   if (timeout)
     {

-      int ms = get_run_time_ms();
+      int ms = get_run_time_ms(NULL);

       if (verbose > 1)
        fprintf(stderr, "[time check: %d msec]\n", ms);
       if (ms > timeout && ms > extra_timeout)
       if (verbose > 1)
        fprintf(stderr, "[time check: %d msec]\n", ms);
       if (ms > timeout && ms > extra_timeout)