Commit 49bfaf41 authored by François Bobot's avatar François Bobot

cpulimit : add time printing,

sorry for forgetting to add cpulimit_time.c no it is useless
parent c7ade7b7
......@@ -622,16 +622,13 @@ clean::
# tools
#######
TOOLS = bin/why3-cpulimit bin/why3-cpulimit_time
TOOLS = bin/why3-cpulimit
byte opt: $(TOOLS)
bin/why3-cpulimit: src/tools/@CPULIMIT@.c
$(CC) -Wall -o $@ $^
bin/why3-cpulimit_time: src/tools/@CPULIMIT@_time.c
$(CC) -Wall -o $@ $^
clean::
rm -f bin/why3-cpulimit src/tools/*~
......
......@@ -10,6 +10,7 @@ invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -8,6 +8,7 @@ filename "%f-%t-%g.gappa"
valid 0
unknown "no contradiction was found\\|some enclosures were not satisfied" "Unknown"
time "cpulimit_time : %s s"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\)" "Unknown"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -7,6 +7,7 @@ filename "%f-%t-%g.smt"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
time "cpulimit_time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
......
......@@ -11,7 +11,7 @@ version_ok = "0.92"
version_ok = "0.91"
version_old = "0.9"
version_old = "0.8"
command = "why3-cpulimit %t %m %e %f"
command = "why3-cpulimit %t %m yes %e %f"
driver = "drivers/alt_ergo.drv"
[ATP cvc3]
......@@ -21,7 +21,7 @@ version_switch = "-version"
version_regexp = "This is CVC3 version \\([^ \n]+\\)"
version_ok = "2.2"
version_old = "2.1"
command = "why3-cpulimit_time 0 %m %e -timeout %t -lang smt %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -timeout %t -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[ATP yices]
......@@ -32,7 +32,7 @@ version_regexp = "[Yices ]*\\([^ \n]+\\)"
version_ok = "1.0.27"
version_old = "1.0.17"
version_old = "1.0.24"
command = "why3-cpulimit %t %m %e -smt 2>&1"
command = "why3-cpulimit %t %m yes %e -smt 2>&1"
driver = "drivers/yices.drv"
[ATP eprover]
......@@ -40,7 +40,7 @@ name = "Eprover"
exec = "eprover"
version_switch = "--version"
version_regexp = "E \\([^\n]+\\)"
command = "why3-cpulimit_time 0 %m %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f 2>&1"
driver = "drivers/tptp.drv"
[ATP gappa]
......@@ -54,7 +54,7 @@ version_old = "0.12.2"
version_old = "0.12.1"
version_old = "0.12.0"
version_old = "0.11.2"
command = "why3-cpulimit %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/gappa.drv"
[ATP simplify]
......@@ -67,7 +67,7 @@ version_switch = "-version"
version_regexp = "Simplify version \\([^ \n,]+\\)"
version_ok = "1.5.5"
version_ok = "1.5.4"
command = "why3-cpulimit_time %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/simplify.drv"
[ATP spass]
......@@ -75,7 +75,7 @@ name = "Spass"
exec = "SPASS"
version_switch = "-TPTP || true"
version_regexp = "SPASS V \\([^ \n\t]+\\)"
command = "why3-cpulimit_time 0 %m %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
command = "why3-cpulimit 0 %m yes %e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f 2>&1"
driver = "drivers/tptp.drv"
[ATP verit]
......@@ -84,7 +84,7 @@ exec = "veriT"
exec = "verit"
version_switch = "--help"
version_regexp = "Version: \\([^ \n\r]+\\)"
command = "why3-cpulimit %t %m %e %f 2>&1"
command = "why3-cpulimit %t %m yes %e %f 2>&1"
driver = "drivers/verit.drv"
[ATP z3]
......@@ -96,7 +96,7 @@ version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "2.2"
version_old = "2.1"
version_old = "1.3"
command = "why3-cpulimit_time %t %m %e -smt %f 2>&1"
command = "why3-cpulimit %t %m yes %e -smt %f 2>&1"
driver = "drivers/z3.drv"
[ITP coq]
......
......@@ -27,24 +27,48 @@
#include <sys/types.h>
#include <sys/time.h>
#include <time.h>
#include <sys/times.h>
#include <sys/resource.h>
#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>
#include <errno.h>
#include <string.h>
#include <sys/wait.h>
int main(int argc, char *argv[]) {
int timelimit, memlimit;
struct rlimit res;
if (argc < 4) {
if (argc < 5) {
fprintf(stderr, "usage: %s <time limit in seconds> \
<virtual memory limit in MiB> <command>\n\
<virtual memory limit in MiB> <print time yes|no> <command>\n\
a null value sets no limit (keeps the actual limit)\n", argv[0]);
return 1;
}
/* Fork if requested */
if(strcmp("yes",argv[3]) == 0){
int pid = fork ();
if (pid == -1){
perror("fork");
exit(EXIT_FAILURE);
} else if (pid == 0){
/* The child continue to execute the program */
} else {
/* The parent will not exit this condition */
int status;
waitpid(pid, &status, 0);
struct tms tms;
times(&tms);
double time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
/ sysconf(_SC_CLK_TCK));
fprintf(stdout, "cpulimit_time : %f s\n",time);
return status;
}
}
/* get time limit in seconds from command line */
timelimit = atoi(argv[1]);
......@@ -66,8 +90,10 @@ a null value sets no limit (keeps the actual limit)\n", argv[0]);
}
/* execute the command */
execvp(argv[3],argv+3);
fprintf(stderr, "%s: exec of '%s' failed (%s)\n",argv[0],argv[3],strerror(errno));
return 1;
execvp(argv[4],argv+4);
fprintf(stderr, "%s: exec of '%s' failed (%s)\n",
argv[0],argv[4],strerror(errno));
return EXIT_FAILURE;
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment