diff --git a/src/plugins/wp/cores.c b/src/plugins/wp/cores.c new file mode 100644 index 0000000000000000000000000000000000000000..2a4d0e6c995074f7c5e983b21c70b128f579540d --- /dev/null +++ b/src/plugins/wp/cores.c @@ -0,0 +1,45 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2024 */ +/* 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 licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + +#include <caml/memory.h> +#include <caml/mlvalues.h> + +#ifdef _WIN32 +#include <windows.h> +#else +#include <unistd.h> +#endif + +int cores(void) { +#ifdef WIN32 + SYSTEM_INFO sysinfo; + GetSystemInfo(&sysinfo); + return sysinfo.dwNumberOfProcessors; +#else + return sysconf(_SC_NPROCESSORS_CONF); +#endif +} + +CAMLprim value caml_cores(value unit) { + CAMLparam1(unit); + CAMLreturn(Val_int(cores())); +} diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune index 763e5af8cbc84a4f68d39f8c96ffe9d32fa4e562..6f393270237475ee5eb2c886e0111e358fe797bd 100644 --- a/src/plugins/wp/dune +++ b/src/plugins/wp/dune @@ -44,6 +44,7 @@ (select wp_eva.ml from (frama-c-eva.core -> wp_eva.enabled.ml) ( -> wp_eva.disabled.ml))) + (foreign_stubs (language c) (names cores)) (instrumentation (backend landmarks)) (instrumentation (backend bisect_ppx))) diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml index 9268c9e87a80e682a9c5a7c346a9a1c04da61d68..efb064a639de06c19ba50ed0590885f962904aac 100644 --- a/src/plugins/wp/wp_parameters.ml +++ b/src/plugins/wp/wp_parameters.ml @@ -885,12 +885,14 @@ module TimeMargin = (default: %s)." default end) +external cores : unit -> int = "caml_cores" + let () = Parameter_customize.set_group wp_prover module Procs = Int(struct let option_name = "-wp-par" let arg_name = "p" - let default = 4 + let default = cores () let help = Printf.sprintf "Number of parallel proof process (default: %d)" default