diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 5660f5616e42f642d962af21324bd1963a59b467..75d11316c614844c36c6193fd864d1a6175b8938 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -73,6 +73,5 @@ top/
 doc/doxygen/doxygen.cfg
 doc/doxygen/html
 doc/doxygen/warn.log
-benchmarking/tools/fc-time
 lib/libgmp-e-acsl.a
 lib/libjemalloc-e-acsl.a
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 146cc5b6b145e8a7310cd8b41ab79048c2a26883..b9f74b3d5b7b2ec3f2315a6b4d015fb3925c4c0d 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -118,25 +118,6 @@ clean::
 
 endif
 
-######################
-# Benchmarking tools #
-######################
-
-EACSL_BM_SOURCES = $(wildcard $(PLUGIN_DIR)/benchmarking/tools/*.c)
-EACSL_BM_BINARIES = $(patsubst %.c,%, $(EACSL_BM_SOURCES))
-
-CFLAGS = -g3 -O2 -std=c11 -pedantic -Wall -Wno-unused-result
-
-$(EACSL_BM_BINARIES): % : %.c
-	$(PRINT_CC) $@
-	$(CC) $(CFLAGS) -o $@ $^
-
-all:: $(EACSL_BM_BINARIES)
-
-clean::
-	$(PRINT_RM) benchmarking tools
-	$(RM) $(EACSL_BM_BINARIES)
-
 ################################################
 # E-ACSL C Libs: libjemalloc, libgmp           #
 ################################################
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
deleted file mode 100644
index 725d4337c6b42ce4b561875ef24fc4ba47802600..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
+++ /dev/null
@@ -1,4 +0,0 @@
-Benchmark   No-model  Segment-model Bittree-model
-grep        2           4.4        18
-sed         3           9          16
-diff        4           9.3        7.3
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat
deleted file mode 100644
index c8851c9a5beff4d6885904e4ed60fc73ef1e1865..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat
+++ /dev/null
@@ -1,11 +0,0 @@
-RUNS    No-model  Segment-model Bittree-model
-1       1.1       4.6           8.6
-2       2.3       9.2           13.8
-3       1.0       9.9           11.2
-4       1.9       4.3           6.9
-5       3.4       6.9           12.5
-6       5.4       20.4          33.4
-7       8.1       21.8          36.7
-8       11.6      23.7          16.2
-9       16.6      40.8          22.7
-10      1.15      7.4           8.1
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh b/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh
deleted file mode 100755
index 56f3dd52eb0e386769462deda79ce8b25a849cce..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh
+++ /dev/null
@@ -1,32 +0,0 @@
-#!/bin/sh
-
-# Sample script showing usage of `bm.gnuplot` script
-
-# Path to gnuplot script
-BM_GNUPLOT="../../tools/bm.gnuplot"
-
-# Build a line plot using lineplot.dat data file
-gnuplot \
-    -e "BaseFile='dat/lineplot'" \
-    -e "Style='lines'" \
-    -e "WithOverheads=1" \
-    -e "PlotTitle='Sample line plot title'" \
-    -e "XLabel='Sample line plot label of X axis'" \
-    -e "YLabel='Sample line plot label of Y axis'" \
-    -e "OutputDir='.'" \
-    -e "WithOverheads='1'" \
-    $BM_GNUPLOT
-
-# Build a histogram using barplot.dat data file
-gnuplot \
-    -e "BaseFile='dat/barplot'" \
-    -e "Style='histogram'" \
-    -e "WithOverheads=1" \
-    -e "PlotTitle='Sample histogram title'" \
-    -e "XLabel='Sample histogram label of X axis'" \
-    -e "YLabel='Sample histogram label of Y axis'" \
-    -e "OutputDir='.'" \
-    -e "WithOverheads='1'" \
-    $BM_GNUPLOT
-
-exit 0
diff --git a/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot b/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot
deleted file mode 100755
index 59fce6cb7f7bbf8a87018cd4358c994ca07d2080..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot
+++ /dev/null
@@ -1,180 +0,0 @@
-#!/usr/bin/env gnuplot
-
-##########################################################################
-#                                                                        #
-#  This file is part of the Frama-C's E-ACSL plug-in.                    #
-#                                                                        #
-#  Copyright (C) 2012-2016                                               #
-#    CEA (Commissariat à l'énergie atomique et aux énergies              #
-#         alternatives)                                                  #
-#                                                                        #
-#  you can redistribute it and/or modify it under the terms of the GNU   #
-#  Lesser General Public License as published by the Free Software       #
-#  Foundation, version 2.1.                                              #
-#                                                                        #
-#  It is distributed in the hope that it will be useful,                 #
-#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
-#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
-#  GNU Lesser General Public License for more details.                   #
-#                                                                        #
-#  See the GNU Lesser General Public License version 2.1                 #
-#  for more details (enclosed in the file license/LGPLv2.1).             #
-#                                                                        #
-##########################################################################
-
-# Usage information of a script
-#
-# Gnuplot script for building line graphs and histograps
-#
-# The script should be invoked as follows:
-#  gnuplot \
-#    -e "BaseFile='<Base name of .dat file>' \
-#    -e "Style='<lines|histogram>' \
-#    -e "PlotTitle='<Optional: Plot title: [BaseFile]>'"
-#    -e "XLabel='<Optional: X-axis label: [""]>'"
-#    -e "YLabel='<Optional: Y-axis label: ["1st column title"]>'"
-#    -e "OutputDir='<Optional: directory where to place output files>'"
-#    -e "WithOverheads='<ANY>'"
-#   data.plot
-#
-# Arguments:
-# - BaseName - base name of a data file with data to plot. This script expects
-#     BaseName.dat to exist and contain data. E.g., if the provided value is
-#     'foo/bar', then foo/bar.dat file should exist
-# - Style - a compulsory argument indicating the type of a plot to be constructed.
-# Allowed values are 'histogram' or 'lines'. If 'lines' value is given then
-# this script builds a line plot expecting the data file be of the form:
-#  YLabel XLabel1 XLabel2 ...
-#  YValue XValue1 XValue2 ...
-#  ...
-# If 'histogram' argument is specified a data file is expected to be of the form:
-#  GroupLabel   Label2 Label3 Label4
-#  Group1       Value1 Value2 Value3 ...
-#  Group2       Value1 Value2 Value3 ...
-#  ...
-# - XLabel - optional string used a X-axis label
-# - YLabel - optional string used a Y-axis label
-# - PlotTitle - optional string used a plot title
-# - OutputDir - optional directory for placement of resulting pdf files
-# - WithOverheads - if any value is given to this argument then the script
-#    computes overheads relative to the values in the second column
-
-# Check if a given file exists
-file_exists(file) = system("test -f '".file."' && echo '1' || echo '0'") + 0
-
-if (exists("Style") && (Style eq "histogram" && Style eq "lines")) {
-  print "ERROR: Unknown histogram style [histogram|lines]"
-  print "See inline comments for details"
-  exit 1
-}
-
-# Check if the base name of the datafile (name - extension .dat)
-# is given via commandline
-if (!exists("BaseFile")) {
-  print "ERROR: Variable 'BaseFile' should be set via commandline"
-  print "See inline comments for details"
-  exit
-}
-
-# Set datafile name
-DataFile = BaseFile.'.dat'
-
-# Check if it exists
-if (!file_exists(DataFile)) {
-  print "ERROR: ".DataFile." not found."
-  print "See inline comments for details"
-  exit
-}
-
-# Unless specified the plot title is named after the base name of the file
-if (!exists("PlotTitle"))
-  PlotTitle = BaseFile
-# Unless specified the Y axis label is the leftmost column header
-if (!exists("YLabel"))
-  YLabel = word(system(sprintf("head -n 1 %s", DataFile)),1)
-# Unless specified Y label is empty
-if (!exists("XLabel"))
-  XLabel = ""
-
-# Fonts and background
-Background      = '#F7F7F7'
-BaseFont        = 'Arial,14'
-TicsFont        = "Arial,10"
-LegendFont      = "Arial,12"
-SideLabelFont   = "Arial-Bold,16"
-
-# Line colours
-set linetype 6 linewidth 2 linecolor rgb "#666633" pointtype 6  pointsize 0.7 # Dark yellow
-set linetype 5 linewidth 2 linecolor rgb "#006633" pointtype 5  pointsize 0.7 # Green
-set linetype 4 linewidth 2 linecolor rgb "#000000" pointtype 4  pointsize 0.7 # Black
-set linetype 3 linewidth 2 linecolor rgb "#990099" pointtype 3  pointsize 0.7 # Magenta
-set linetype 2 linewidth 2 linecolor rgb "#000066" pointtype 8  pointsize 0.7 # Dark blue
-set linetype 1 linewidth 2 linecolor rgb "#990000" pointtype 7  pointsize 0.7 # Maroon
-
-# Use the postscript terminal, as a PDF one is not fully featured
-set terminal postscript landscape size 10,7 enhanced color font BaseFont
-
-# Set background colour for the plot area
-set object 1 rectangle from graph 0, graph 0 to graph 1, graph 1 behind fc rgbcolor Background fs noborder
-
-# Set font for ticks and make them appear outside
-# nomirror removes x2ticks and y2ticks (top and right)
-set ytics font TicsFont out nomirror
-set xtics font TicsFont out nomirror
-
-set autoscale
-
-# Legend font
-set key on horizontal font LegendFont
-
-# PlotTitle variable should come from environment via -e
-set title PlotTitle
-
-# Enable fonts for side labels
-set xlabel XLabel font SideLabelFont
-set ylabel YLabel font SideLabelFont
-
-# Enable macros
-set macros
-
-PsFile = BaseFile.'.ps'
-PdfFile = BaseFile.'.pdf'
-
-if (exists("OutputDir")) {
-  PsFile = OutputDir."/".system("basename ".DataFile)
-  PdfFile = OutputDir."/".system("basename ".PdfFile)
-}
-
-Columns=`tail -n 1 @DataFile | wc -w`
-
-# Set output file command
-set output PsFile
-
-# Overhead plotting function
-#   nat - time of an original executable
-#   mod -= time of the modified executable
-# If WithOverheads var is defined then compute overheads, otherwise plot as is
-ovh(nat, mod) = exists("WithOverheads") ? mod/nat : mod
-
-###################
-# Plotting
-###################
-# Build a line plot
-if (Style eq "lines") {
-  plot for [COL = 2:Columns] DataFile \
-    using 1:(ovh(column(2), column(COL))) title columnheader(COL) with linespoints
-}
-
-# Build a histogram
-if (Style eq "histogram") {
-  set yrange [0:]
-  set style data histogram
-  set style fill solid border -1
-  plot for [COL=2:Columns] DataFile using (ovh(column(2), column(COL))):xticlabels(1) title columnheader
-}
-
-# At this point postscript is generated, create PDF
-!ps2pdf @PsFile @PdfFile
-!rm @PsFile
-
-
diff --git a/src/plugins/e-acsl/benchmarking/tools/fc-time.c b/src/plugins/e-acsl/benchmarking/tools/fc-time.c
deleted file mode 100644
index 4aa78abe3ff66ffcddf642722e97584ca795e766..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/benchmarking/tools/fc-time.c
+++ /dev/null
@@ -1,467 +0,0 @@
-/* Copyright (C) 1990, 91, 92, 93, 96 Free Software Foundation, Inc.
- *
- * This program is free software; you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation; either version 2, or (at your option)
- * any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
- * 02111-1307, USA. */
-
-/* fc-time -- mesaure real time of an executed command */
-
-#include <stdlib.h>
-#include <string.h>
-#include <stdio.h>
-#include <unistd.h>
-#include <stdarg.h>
-#include <errno.h>
-#include <getopt.h>
-#include <signal.h>
-#include <sys/wait.h>
-#include <sys/time.h>
-#include <sys/types.h>
-#include <sys/resource.h>
-
-/* Extra declarations to suppress warnings in -std=c99 or -std=c11 modes */
-int kill(pid_t pid, int sig);
-
-const char *strdup(const char *s);
-
-pid_t wait4(pid_t pid, int *status, int options, struct rusage *rusage);
-
-typedef void (*sighandler_t) (int);
-
-#ifdef __linux__
-#include <linux/limits.h>
-#endif
-
-/* Minimal reported runtime */
-#define MINTIME  0.001
-
-/* Minimal time limit after which a program is forcibly terminated  */
-#define MINLIMIT 0.1
-
-/* Name of the output file. Only used if -o option is given.  */
-static const char *outfile;
-
-/* Output stream, defaults to stderr */
-static FILE *outfp;
-
-/* If true, append to `outfile' rather than truncating it  */
-static int append;
-
-/* Program name */
-static const char * program_name = NULL;
-
-/* Time limit in seconds */
-long double time_limit = 0;
-
-/* Verbosity level */
-int verbose;
-
-/* Gather memory stats via /proc/[pid]/statm */
-int memory;
-
-/* Struct for holding the results of memory statistics */
-struct statistics {
-  unsigned long vsize;      /* (1) total program size (page size) */
-  unsigned long rss;        /* (2) resident set size (page size) */
-  unsigned long share;      /* (3) shared pages (page size) */
-  unsigned long text;       /* (4) text (page size) */
-  unsigned long lib;        /* (5) library (page size) */
-  unsigned long data;       /* (6) data + stack (page size) */
-
-  /* The number of times a procfile has been read */
-  unsigned long count;
-  int status; /* exit status */
-
-  struct timeval start; /* timestamp of program start */
-  struct timeval finish; /* timestamp of program end */
-  struct rusage resusage; /* struct for use with getrusage */
-};
-
-/* Name of the used memory stat file */
-char procfile [PATH_MAX];
-
-/* Memory stat file stream */
-FILE *procfp = NULL;
-
-/* Default report format string */
-char *report_format = "%e\n";
-
-/* Memory size units */
-#define B_SZ  1
-#define KB_SZ 1024
-#define MB_SZ (1024*KB_SZ)
-#define GB_SZ (1024*MB_SZ)
-
-/* Reported block unit */
-static int block_size;
-
-/* Short options */
-static const char *shortopts = "+ao:l:vmB:f:";
-
-/* Long options */
-static struct option longopts[] = {
-  {"limit", required_argument, NULL, 'l'},
-  {"verbose", no_argument, NULL, 'v'},
-  {"append", no_argument, NULL, 'a'},
-  {"help", no_argument, NULL, 'h'},
-  {"output-file", required_argument, NULL, 'o'},
-  {"memory", required_argument, NULL, 'm'},
-  {"block-bize", required_argument, NULL, 'B'},
-  {"format", required_argument, NULL, 'f'},
-  {NULL, no_argument, NULL, 0}
-};
-
-/* Print help page and exit */
-static void usage (FILE *stream, int status) {
-  fprintf(stream,
-"NAME:\n"
-"  fc-time -- measure execution time and/or memory consumption of a command\n"
-"SYNOPSIS:\n"
-"  fc-time [options] command [arg...]\n"
-"OPTIONS:\n"
-"  -h, --help     print this help page and exit.\n"
-"  -o FILE        send output to a named file [stderr].\n"
-"  -a, --append   append an output file without truncating it (with -o).\n"
-"  -l SECONDS     limit in seconds arter which a program is terminated\n"
-" even if it is not finshed. The limit needs to be specified with seconds\n"
-" precision.\n"
-"  -m, --memory - collect memory statistics [disabled].\n"
-"  -v             warn if a program has been terminated via -l option.\n"
-"  -f             printf-like report format string.\n"
-"     %%e - elapsed real time [seconds:milliseconds].\n"
-"     %%E - same as %%e\n"
-"     %%U - total time spent in user mode [seconds:milliseconds].\n"
-"     %%S - total time spent in kernel mode [seconds:milliseconds].\n"
-"     %%v - virtual memory consumption peak [bytes].\n"
-"     %%t - text segment size [bytes].\n"
-"     %%d - data + stack segments sizes [bytes].\n"
-"     %%r - maximum resident set size [bytes].\n"
-" Memory-related measurements (e.g., virtual memory consumption or rss)\n"
-" are disabled by default. Unless -m option is used they are reported as\n"
-" zeroes. Computing memory peaks may result in the increase of runtime.\n"
-"  -B, --byte-size=<B|KB|MB|GB> - change reported memory unit [B].\n");
-  exit(status);
-}
-
-/* Error reporting function. Replica of the GNU error (3).
- * Added for portability purposes. */
-static void error(int status, int errnum, const char *format, ...) {
-  fflush(stderr); /* Flush streams */
-  fflush(stdout);
-
-  if (program_name) /* Report program name */
-    fprintf(stderr, "%s: ", program_name);
-
-  va_list va; /* Pass the error message given by the user */
-  va_start(va, format);
-  vfprintf(stderr, format, va);
-  va_end(va);
-
-  if (errnum) /* Report error given via errno */
-    fprintf(stderr, ": %s", strerror(errnum));
-
-  /* Add the newline at the end */
-  fprintf(stderr, "\n");
-
-  /* Exit if status is a non-zero */
-  if (status)
-    exit(status);
-}
-
-#define warning(_fmt, ...) \
-  if (verbose) {  \
-    error(0, 0, _fmt, __VA_ARGS__); \
-  }
-
-/* Initialize the options and parse the command line arguments.
-   Also note the position in ARGV where the command to time starts. */
-static const char ** getargs (int argc, char **argv) {
-  int optc;
-  outfile = NULL;
-  outfp   = stderr; /* Output to  stderr by default */
-  append  = 0;
-  verbose = 0;
-  memory  = 0;
-  block_size = KB_SZ;
-
-  while ((optc = getopt_long(argc, argv, shortopts, longopts, NULL)) != EOF) {
-    switch (optc) {
-      case 'a':
-        append = 1;
-        break;
-      case 'h':
-        usage (stdout, 0);
-      case 'o':
-        outfile = optarg;
-        break;
-      case 'v':
-        verbose = 1;
-        break;
-      case 'm':
-        memory = 1;
-        break;
-      case 'f':
-        report_format = (char*)strdup(optarg);
-        break;
-      case 'l':
-        /* Convert time limit to seconds */
-        time_limit = strtold(optarg, NULL);
-
-        /* Abort if the time limit provided at input is invalid or less than
-           the threshold given by MINLIMIT */
-        if (time_limit < MINLIMIT)
-          error(1, errno, "Bad time limit specification: '%s'."
-            " Expected positive number greater than %0.3f", optarg, MINLIMIT);
-        /* Detect over- or underflow */
-        if (errno == ERANGE)
-          error(1, errno, "%s", optarg);
-        break;
-	    case 'B': { /* reported unit size */
-        switch(optarg[0]) {
-          case 'B': /* report memory in bytes */
-            block_size = B_SZ;
-            break;
-          case 'K': /* ... kilobytes */
-            block_size = KB_SZ;
-            break;
-          case 'M': /* ... megabytes */
-            block_size = MB_SZ;
-            break;
-          case 'G': /* ... gigabytes */
-            block_size = GB_SZ;
-            break;
-          default:
-            error(1, 0, "Bad block size specification (%s), expected B,K,M or G", optarg);
-        }
-        break;
-      }
-      default:
-        usage (stderr, 1);
-    }
-  }
-
-  if (optind == argc)
-    usage (stderr, 1);
-
-  if (outfile) {
-    if (append)
-      outfp = fopen (outfile, "a");
-    else
-      outfp = fopen (outfile, "w");
-    if (outfp == NULL)
-      error(1, errno, "%s", outfile);
-  }
-  return (const char **) &argv[optind];
-}
-
-/* Convert timeval into a double with millisecond precision */
-#define TIMEWMS(_tval) (_tval.tv_sec + (_tval.tv_usec/1000000.0))
-#define TIMEDIFF(_finish,_start) (TIMEWMS(_finish) - TIMEWMS(_start))
-
-/* Assign the max of _old and _new to _old */
-#define assignmax(_old, _new) _old = (_old > _new) ? _old : _new
-
-/* Observe the child's execution, collect memory stats and terminate the
- * execution if the time limit is exceeded
- *
- * - This function is invoked only if either `time_limit' or `memory'
- *   are specified, i.e., a user requests either to collect memory stats
- *   or terminate the execution upon exceeding some time limit.
- *
- * - For the case when a time limit is given but memory statistics do not
- *   need to be collected the parent process checks if the time limit is
- *   exceeded each second. This is to limit the interference
- *
- * - If memory stats are collected, then checking time limit and reading
- *   procfile is done in a cycle without sleeping periods. This may slightly
- *   extend the execution of the program
-*/
-int observe(pid_t chpid, struct statistics * stats) {
-  int status;
-  pid_t rpid;
-
-  while (!(rpid = wait4(chpid, &status, WNOHANG, &stats->resusage))) {
-    gettimeofday(&stats->finish, NULL);
-    if (time_limit && TIMEDIFF(stats->finish, stats->start) > time_limit) {
-      warning("Warning: Attempting graceful termination due exceeded time "
-          "limit of %0.2Lf seconds", "", time_limit);
-      kill(chpid, SIGTERM);
-      break;
-    } else {
-      /* No mem stats need to be collected, sleep for one second */
-      if (!memory) {
-        sleep(1);
-      /* Mem stats need to be collected */
-      } else {
-        unsigned long vsize, rss, share, text, lib, data;
-        /* Open and read process file */
-        procfp = fopen(procfile, "r");
-        if (!procfp)
-          error(1, errno, "cannot open process memory stat file %s", procfile);
-        fscanf(procfp, "%lu %lu %lu %lu %lu %lu",
-          &vsize, &rss, &share, &text, &lib, &data);
-        assignmax(stats->vsize, vsize);
-        assignmax(stats->rss, rss);
-        assignmax(stats->share, share);
-        assignmax(stats->text, text);
-        assignmax(stats->lib, lib);
-        assignmax(stats->data, data);
-        fclose(procfp);
-        stats->count++;
-      }
-    }
-  }
-
-  if (rpid == -1)
-    return 0;
-  return 1;
-}
-
-/* Run command and return statistics on it. */
-static int run_command (const char ** cmd) {
-  pid_t pid = 0;			/* Pid of child  */
-  int status = 0;     /* Status of a child */
-  sighandler_t interrupt_signal, quit_signal;
-
-  struct statistics stats;
-  memset(&stats, 0, sizeof(struct statistics));
-
-  /* Fork the child process */
-  pid = fork();
-
-  /* Copy the name of the stat file to the `procfile` global */
-  sprintf(procfile, "/proc/%d/statm", pid);
-
-  /* Start measuring real time */
-  gettimeofday(&stats.start, NULL);
-
-  if (pid < 0) {
-    error(1, errno, "cannot fork");
-  } else if (pid == 0) { /* If child. */
-    execvp(cmd[0], (char *const*) cmd);
-    error(0, errno, "cannot run %s", cmd[0]);
-    exit(errno == ENOENT ? 127 : 126);
-  }
-
-  /* Have signals kill the child but not self */
-  interrupt_signal = signal(SIGINT, SIG_IGN);
-  quit_signal = signal(SIGQUIT, SIG_IGN);
-
-  /* Time limit has been specified. Observe execution of the child process
-   * and terminate the program after the time limit has been exceeded. */
-  if (time_limit || memory) {
-    if (observe(pid, &stats) == 0)
-      error(1, errno, "error waiting for child process");
-  /* No time limit given. Run the program as is and compute the runtime after
-   * the process terminates. */
-  } else {
-    pid_t rpid = wait4(pid, &status, 0, &stats.resusage);
-    gettimeofday(&stats.finish, NULL);
-    if (rpid == -1)
-      error (1, errno, "error waiting for child process");
-  }
-
-  /* Re-enable signals.  */
-  signal(SIGINT, interrupt_signal);
-  signal(SIGQUIT, quit_signal);
-
-  /* Format string for report */
-  char *fmt = report_format;
-
-  /* Page size (/proc/[pid]/statm) reports sizes in pages */
-  long pagesz = sysconf(_SC_PAGESIZE);
-
-  while(*fmt != '\0') {
-    switch(*fmt) {
-      case '%': {
-        fmt++;
-	      switch (*fmt) {
-          /* Elapsed time with millisecond precition */
-          case 'E':
-          case 'e': {
-            double elapsed = TIMEWMS(stats.finish) - TIMEWMS(stats.start);
-            fprintf(outfp, "%0.3f", (elapsed > MINTIME) ? elapsed : MINTIME);
-            break;
-          }
-          /* Time spent in kernel mode */
-          case 'S':
-            fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_stime));
-            break;
-          /* Time spent in user mode */
-          case 'U':
-            fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_utime));
-            break;
-          case 'v':
-            fprintf(outfp, "%lu", (stats.vsize*pagesz)/block_size);
-            break;
-          case 'd':
-            fprintf(outfp, "%lu", (stats.data*pagesz)/block_size);
-            break;
-          case 't':
-            fprintf(outfp, "%lu", (stats.text*pagesz)/block_size);
-            break;
-          case 'r':
-            fprintf(outfp, "%lu", (stats.rss*pagesz)/block_size);
-            break;
-          default:
-            fprintf(outfp, "???");
-            break;
-        }
-        break;
-      }
-      case '\\': {
-        fmt++;
-	      switch (*fmt) {
-	        case 't':
-	          putc ('\t', outfp);
-	          break;
-	        case 'n':
-	          putc ('\n', outfp);
-	          break;
-	        case '\\':
-	          putc ('\\', outfp);
-	          break;
-	        default:
-	          putc ('?', outfp);
-	          putc ('\\', outfp);
-	          putc (*fmt, outfp);
-	      }
-	      break;
-      }
-      default: {
-        putc (*fmt, outfp);
-      }
-    }
-    fmt++;
-  }
-
-  fflush(outfp);
-  /* ... and return the status of the child */
-  return status;
-}
-
-int main (int argc, char **argv) {
-  program_name = *argv;
-  const char **command_line = getargs(argc, argv);
-  int status = run_command(command_line);
-
-  /* Examining exit status of wait */
-  if (WIFSTOPPED(status))
-    exit(WSTOPSIG(status));
-  else if (WIFSIGNALED(status))
-    exit(WTERMSIG(status));
-  else if (WIFEXITED(status))
-    exit(WEXITSTATUS(status));
-  return 0;
-}