MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit e6fda06c authored by Francois Bobot's avatar Francois Bobot
Browse files

why-cpulimit : add virtual memory limit

Since there is no install target in the makefile, and people can
prefer to use why-cpulimit of why2. We must add the bin directory of
why3 in our $Path when we use why3 in order to get this new
why-cpulimit. (Perhaps it can be backported to why2?)
parent df134a29
......@@ -34,11 +34,13 @@
#include <errno.h>
int main(int argc, char *argv[]) {
int timelimit;
int timelimit, memlimit;
struct rlimit res;
if (argc < 3) {
fprintf(stderr, "usage: %s <time limit in seconds> <command>\n", argv[0]);
if (argc < 4) {
fprintf(stderr, "usage: %s <time limit in seconds> \
<virtual memory limit in MiB> <command>\n\
a null value sets no limit (keeps the actual limit)\n", argv[0]);
return 1;
}
......@@ -52,8 +54,18 @@ int main(int argc, char *argv[]) {
setrlimit(RLIMIT_CPU,&res);
}
/* get virtual memory limit in MiB from command line */
memlimit = atol(argv[2]);
if (memlimit > 0) {
/* set the CPU time limit */
getrlimit(RLIMIT_AS,&res);
res.rlim_cur = memlimit * 1024 * 1024;
setrlimit(RLIMIT_AS,&res);
}
/* execute the command */
execvp(argv[2],argv+2);
execvp(argv[3],argv+3);
perror("why-cpulimit exec error");
return 1;
}
......
......@@ -4,7 +4,7 @@ timelimit = 2
[prover alt-ergo]
name = "Alt-Ergo"
command = "why-cpulimit %t alt-ergo %f 2>&1"
command = "why-cpulimit %t %m alt-ergo %f 2>&1"
driver = "drivers/alt_ergo.drv"
[prover coq]
......@@ -14,12 +14,12 @@ driver = "drivers/coq.drv"
[prover cvc3]
name = "CVC3"
command = "why-cpulimit %t cvc3 -lang smt %f 2>&1"
command = "why-cpulimit %t %m cvc3 -lang smt %f 2>&1"
driver = "drivers/cvc3.drv"
[prover z3]
name = "Z3"
command = "why-cpulimit %t z3 -smt %f 2>&1"
command = "why-cpulimit %t %m z3 -smt %f 2>&1"
driver = "drivers/z3.drv"
[prover spass]
......
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