Commit 2946eca7 authored by Andrei Paskevich's avatar Andrei Paskevich

cpulimit-win: produce the same output as cpulimit.c

Drivers that parse the cpulimit output expect a line of the form
"why3cpulimit time : XXX s" for the total cpu time of the prover run.

The Win version of cpulimit prints an additional line
"why3cpulimit real time : XXX s" for the wall-clock time.
This line is ignored by drivers, since we use the cpu time
and not the real time to establish time limits.
parent 96c294fe
......@@ -192,7 +192,7 @@ int main(int argc, char *argv[]) {
((ull_system.QuadPart + ull_user.QuadPart + 0.0) / 10000000.);
wall_time = (ull_stop.QuadPart - ull_start.QuadPart + 0.0) / 10000000.;
fprintf(stdout,
"why3cpulimit cpu time: %fs wall time: %fs\n", cpu_time, wall_time);
"why3cpulimit time : %f s\nwhy3cpulimit real time : %f s\n", cpu_time, wall_time);
fflush(stdout);
}
CloseHandle(pi.hProcess);
......
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