diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e059f9c1deb996b9abb7da4f0f539851a843060f..0a11d379311ee097e2d4160e99d61e68c01315ea 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -120,6 +120,24 @@ E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config \
endif
+######################
+# Benchmarking tools #
+######################
+BM_TOOLS_SOURCES = benchmarking/tools/fc-time.c
+BM_TOOLS_BINARIES = $(patsubst %.c,%, $(BM_TOOLS_SOURCES))
+
+CFLAGS = -g3 -O2 -std=c11 -pedantic -Wall -Wno-unused-result
+
+$(BM_TOOLS_BINARIES): % : %.c
+ $(PRINT_CC) $@
+ $(CC) $(CFLAGS) -o $@ $^
+
+all:: $(BM_TOOLS_BINARIES)
+
+clean::
+ $(PRINT_RM) benchmarking tools
+ $(RM) $(BM_TOOLS_BINARIES)
+
############
# Cleaning #
############
diff --git a/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
new file mode 100644
index 0000000000000000000000000000000000000000..725d4337c6b42ce4b561875ef24fc4ba47802600
--- /dev/null
+++ b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000000000000000000000000000000000000..c8851c9a5beff4d6885904e4ed60fc73ef1e1865
--- /dev/null
+++ b/src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat
@@ -0,0 +1,11 @@
+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
new file mode 100755
index 0000000000000000000000000000000000000000..56f3dd52eb0e386769462deda79ce8b25a849cce
--- /dev/null
+++ b/src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh
@@ -0,0 +1,32 @@
+#!/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
new file mode 100755
index 0000000000000000000000000000000000000000..59fce6cb7f7bbf8a87018cd4358c994ca07d2080
--- /dev/null
+++ b/src/plugins/e-acsl/benchmarking/tools/bm.gnuplot
@@ -0,0 +1,180 @@
+#!/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
new file mode 100644
index 0000000000000000000000000000000000000000..4aa78abe3ff66ffcddf642722e97584ca795e766
--- /dev/null
+++ b/src/plugins/e-acsl/benchmarking/tools/fc-time.c
@@ -0,0 +1,467 @@
+/* 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;
+}