diff --git a/Makefile b/Makefile
index 339672ee03a082413e90dd55a2b34768ec5b40dc..baf54d81140ef1b2dc33c065060e4938b7d2c313 100644
--- a/Makefile
+++ b/Makefile
@@ -43,7 +43,7 @@ VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME)
.PHONY: all
all: config.sed
- dune build
+ dune build @install
ifeq ($(HAS_DOT),yes)
OPTDOT=Some \"$(DOT)\"
diff --git a/ptests/dune b/ptests/dune
index 9ab643b2927faaaff59464be208ec14347b663fc..c5d76b85d38b894f64e104d69cbd0b41200639b3 100644
--- a/ptests/dune
+++ b/ptests/dune
@@ -1,5 +1,6 @@
(executable
(package frama-c)
(public_name ptests)
+ (modules ptests)
(libraries unix threads str)
)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index b3864bd8aa0ada7aaeb3cff4e79d772fcbf415fd..c8eff47171d25e13c024603ab59db95975d2a084 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -24,14 +24,6 @@
annotated with test options *)
let default_options = "-journal-disable -check"
-let system =
- if Sys.os_type = "Win32" then
- fun f ->
- Unix.system (Format.sprintf "bash -c %S" f)
- else
- fun f ->
- Unix.system f
-
module Filename = struct
include Filename
let concat =
@@ -185,7 +177,7 @@ let base_path = Filename.current_dir_name
(** Command-line flags *)
-type behavior = Examine | Update | Run | Show | Gui
+type behavior = Run | Show | Gui
let behavior = ref Run
let verbosity = ref 0
let dry_run = ref false
@@ -209,10 +201,6 @@ let additional_options_pre = ref ""
let special_config = ref ""
let do_error_code = ref false
-let exclude_suites = ref []
-
-let exclude s = exclude_suites := s :: !exclude_suites
-
let xunit = ref false
let io_mutex = Mutex.create ()
@@ -287,15 +275,11 @@ let umsg = "Usage: ptests [options] [names of test suites]";;
let rec argspec =
[
- "-examine", Arg.Unit (fun () -> behavior := Examine) ,
- " Examine the logs that are different from oracles.";
"-gui", Arg.Unit (fun () ->
behavior := Gui;
n := 1; (* Disable parallelism to see which GUI is launched *)
) ,
" Start the tests in Frama-C's gui.";
- "-update", Arg.Unit (fun () -> behavior := Update) ,
- " Take the current logs as oracles.";
"-show", Arg.Unit (fun () -> behavior := Show) ,
" Show the results of the tests.";
"-run", Arg.Unit (fun () -> behavior := Run) ,
@@ -335,8 +319,6 @@ let rec argspec =
that will be launched. <options> are added before standard test options.";
"-add-options-post", Arg.Set_string additional_options,
"Synonym of -add-options";
- "-exclude", Arg.String exclude,
- "<name> Exclude a test or a suite from the run";
"-xunit", Arg.Set xunit,
" Create a xUnit file named xunit.xml collecting results";
"-error-code", Arg.Set do_error_code,
@@ -454,8 +436,8 @@ let redefine_name name =
let dir_config_file = redefine_name dir_config_file
-let gen_make_file s dir file =
- Filename.concat (Filename.concat dir s) file
+let gen_make_file s _dir file =
+ Filename.concat s file
module SubDir: sig
type t
@@ -469,6 +451,8 @@ module SubDir: sig
val make_oracle_file: t -> string -> string
val make_result_file: t -> string -> string
val make_file: t -> string -> string
+ val oracle_dirname: string
+ val result_dirname: string
end = struct
type t = string
@@ -483,7 +467,7 @@ end = struct
let oracle_dirname = redefine_name "oracle"
let result_dirname = redefine_name "result"
- let make_result_file = gen_make_file result_dirname
+ let make_result_file _ x = x
let make_oracle_file = gen_make_file oracle_dirname
let make_file = Filename.concat
@@ -627,31 +611,8 @@ let default_config () =
dc_timeout = "";
}
-let launch command_string =
- if !dry_run then 0 (* do not run command; return as if no error *)
- else
- let result = system command_string in
- match result with
- | Unix.WEXITED 127 ->
- lock_printf "%% Couldn't execute command. Retrying once.@.";
- Thread.delay 0.125;
- ( match system command_string with
- Unix.WEXITED r when r <> 127 -> r
- | _ -> lock_printf "%% Retry failed with command:@\n%s@\nStopping@."
- command_string ;
- exit 1 )
- | Unix.WEXITED r -> r
- | Unix.WSIGNALED s ->
- lock_printf
- "%% SIGNAL %d received while executing command:@\n%s@\nStopping@."
- s command_string ;
- exit 1
- | Unix.WSTOPPED s ->
- lock_printf
- "%% STOP %d received while executing command:@\n%s@\nStopping@."
- s command_string;
- exit 1
-
+let launch _command_string =
+ assert false
let scan_execnow ~once dir ex_timeout (s:string) =
let rec aux (s:execnow) =
@@ -983,7 +944,7 @@ let gen_prefix gen_file cmd =
let log_prefix = gen_prefix SubDir.make_result_file
let oracle_prefix = gen_prefix SubDir.make_oracle_file
-let get_ptest_file cmd = SubDir.make_file cmd.directory cmd.file
+let get_ptest_file cmd = Filename.concat ".." cmd.file
let get_macros cmd =
let ptest_config =
@@ -1038,6 +999,7 @@ let basic_command_string =
toplevel ^ " " ^ file ^ " " ^ options
end
in
+
if command.timeout = "" then raw_command
else "ulimit -t " ^ command.timeout ^ " && " ^ raw_command
@@ -1075,7 +1037,7 @@ let find_in_path s =
with Exit ->
Some !found
-let command_string command =
+let command_string cout command =
let log_prefix = log_prefix command in
let errlog = log_prefix ^ ".err.log" in
let stderr = match command.filter with
@@ -1145,7 +1107,16 @@ let command_string command =
(Filename.sanitize errlog)
(Filename.sanitize stderr)
in
- command_string
+ Printf.fprintf cout
+ "(rule\n \
+ (targets %S %S %t)\n \
+ (deps (universe))\n \
+ (action (system %S))\n\
+ )\n"
+ errlog
+ res
+ (fun cout -> List.iter (Printf.fprintf cout "%S") command.log_files)
+ command_string
let update_log_files dir file =
mv (SubDir.make_result_file dir file) (SubDir.make_oracle_file dir file)
@@ -1175,12 +1146,6 @@ let update_toplevel_command command =
in
List.iter (update_log_files command.directory) log_files
-let rec update_command = function
- Toplevel cmd -> update_toplevel_command cmd
- | Target (execnow,cmds) ->
- List.iter (update_log_files execnow.ex_dir) execnow.ex_log;
- Queue.iter update_command cmds
-
let remove_execnow_results execnow =
List.iter
(fun f -> unlink (SubDir.make_result_file execnow.ex_dir f))
@@ -1263,116 +1228,106 @@ let xunit_report () =
end
-let do_command command =
- match command with
- | Toplevel command ->
- (* Update : copy the logs. Do not enqueue any cmp
- Run | Show: launch the command, then enqueue the cmp
- Gui: launch the command in the gui
- Examine : just enqueue the cmp *)
- if !behavior = Update
- then update_toplevel_command command
- else begin
- (* Run, Show, Gui or Examine *)
- if !behavior = Gui then begin
- (* basic_command_string does not redirect the outputs, and does
- not overwrite the result files *)
- let basic_command_string = basic_command_string command in
- lock_printf "%% launch %s@." basic_command_string ;
- ignore (launch basic_command_string)
- end
- else begin
- (* command string also replaces macros in logfiles names, which
- is useful for Examine as well. *)
- let command_string = command_string command in
- if !behavior <> Examine
- then begin
- if !verbosity >= 1
- then lock_printf "%% launch %s@." command_string ;
- let launch_result = launch command_string in
- let time = 0. (* Individual time is difficult to compute correctly
- for now, and currently unused *) in
- report_run command (launch_result, time)
- end;
- lock ();
- shared.summary_run <- succ shared.summary_run ;
- Queue.push (Cmp_Toplevel command) shared.cmps;
- List.iter
- (fun f -> Queue.push (Cmp_Log (command.directory, f)) shared.cmps)
- command.log_files;
- unlock ()
- end
- end
- | Target (execnow, cmds) ->
- let continue res =
- lock();
- shared.summary_log <- succ shared.summary_log;
- if res = 0
- then begin
- shared.summary_ok <- succ shared.summary_ok;
- Queue.transfer shared.commands cmds;
- shared.commands <- cmds;
- shared.building_target <- false;
- Condition.broadcast shared.work_available;
- if !behavior = Examine || !behavior = Run
- then begin
- List.iter
- (fun f -> Queue.push (Cmp_Log(execnow.ex_dir, f)) shared.cmps)
- execnow.ex_log
- end
- end
- else begin
- let rec treat_cmd = function
- Toplevel cmd ->
- shared.summary_run <- shared.summary_run + 1;
- let log_prefix = log_prefix cmd in
- unlink (log_prefix ^ ".res.log ")
- | Target (execnow,cmds) ->
- shared.summary_run <- succ shared.summary_run;
- remove_execnow_results execnow;
- Queue.iter treat_cmd cmds
- in
- Queue.iter treat_cmd cmds;
- Queue.push (Target_error execnow) shared.diffs;
- shared.building_target <- false;
- Condition.signal shared.diff_available
- end;
- unlock()
- in
-
- if !behavior = Update then begin
- update_command command;
- lock ();
- shared.building_target <- false;
- Condition.signal shared.work_available;
- unlock ();
- end else
- begin
- if !behavior <> Examine && not (!(execnow.ex_done) && execnow.ex_once)
- then begin
- remove_execnow_results execnow;
- let cmd =
- if !use_byte then
- execnow_opt_to_byte execnow.ex_cmd
- else
- execnow.ex_cmd
- in
- if !verbosity >= 1 then begin
- lock_printf "%% launch %s@." cmd;
- end;
- shared.summary_run <- succ shared.summary_run;
- let r = launch cmd in
- (* mark as already executed. For EXECNOW in test_config files,
- other instances (for example another test of the same
- directory), won't relaunch the command. For EXECNOW in
- stand-alone tests, there is only one copy of the EXECNOW
- anyway *)
- execnow.ex_done := true;
- continue r
- end
- else
- continue 0
- end
+(* let do_command command =
+ * match command with
+ * | Toplevel command ->
+ * (\* Update : copy the logs. Do not enqueue any cmp
+ * Run | Show: launch the command, then enqueue the cmp
+ * Gui: launch the command in the gui
+ * Examine : just enqueue the cmp *\)
+ * begin
+ * (\* Run, Show, Gui or Examine *\)
+ * if !behavior = Gui then begin
+ * (\* basic_command_string does not redirect the outputs, and does
+ * not overwrite the result files *\)
+ * let basic_command_string = basic_command_string command in
+ * lock_printf "%% launch %s@." basic_command_string ;
+ * ignore (launch basic_command_string)
+ * end
+ * else begin
+ * (\* command string also replaces macros in logfiles names, which
+ * is useful for Examine as well. *\)
+ * let command_string,_,_ = command_string command in
+ * begin
+ * if !verbosity >= 1
+ * then lock_printf "%% launch %s@." command_string ;
+ * let launch_result = launch command_string in
+ * let time = 0. (\* Individual time is difficult to compute correctly
+ * for now, and currently unused *\) in
+ * report_run command (launch_result, time)
+ * end;
+ * lock ();
+ * shared.summary_run <- succ shared.summary_run ;
+ * Queue.push (Cmp_Toplevel command) shared.cmps;
+ * List.iter
+ * (fun f -> Queue.push (Cmp_Log (command.directory, f)) shared.cmps)
+ * command.log_files;
+ * unlock ()
+ * end
+ * end
+ * | Target (execnow, cmds) ->
+ * let continue res =
+ * lock();
+ * shared.summary_log <- succ shared.summary_log;
+ * if res = 0
+ * then begin
+ * shared.summary_ok <- succ shared.summary_ok;
+ * Queue.transfer shared.commands cmds;
+ * shared.commands <- cmds;
+ * shared.building_target <- false;
+ * Condition.broadcast shared.work_available;
+ * if !behavior = Run
+ * then begin
+ * List.iter
+ * (fun f -> Queue.push (Cmp_Log(execnow.ex_dir, f)) shared.cmps)
+ * execnow.ex_log
+ * end
+ * end
+ * else begin
+ * let rec treat_cmd = function
+ * Toplevel cmd ->
+ * shared.summary_run <- shared.summary_run + 1;
+ * let log_prefix = log_prefix cmd in
+ * unlink (log_prefix ^ ".res.log ")
+ * | Target (execnow,cmds) ->
+ * shared.summary_run <- succ shared.summary_run;
+ * remove_execnow_results execnow;
+ * Queue.iter treat_cmd cmds
+ * in
+ * Queue.iter treat_cmd cmds;
+ * Queue.push (Target_error execnow) shared.diffs;
+ * shared.building_target <- false;
+ * Condition.signal shared.diff_available
+ * end;
+ * unlock()
+ * in
+ *
+ * begin
+ * if not (!(execnow.ex_done) && execnow.ex_once)
+ * then begin
+ * remove_execnow_results execnow;
+ * let cmd =
+ * if !use_byte then
+ * execnow_opt_to_byte execnow.ex_cmd
+ * else
+ * execnow.ex_cmd
+ * in
+ * if !verbosity >= 1 then begin
+ * lock_printf "%% launch %s@." cmd;
+ * end;
+ * shared.summary_run <- succ shared.summary_run;
+ * let r = launch cmd in
+ * (\* mark as already executed. For EXECNOW in test_config files,
+ * other instances (for example another test of the same
+ * directory), won't relaunch the command. For EXECNOW in
+ * stand-alone tests, there is only one copy of the EXECNOW
+ * anyway *\)
+ * execnow.ex_done := true;
+ * continue r
+ * end
+ * else
+ * continue 0
+ * end *)
let log_ext = function Res -> ".res" | Err -> ".err"
@@ -1469,58 +1424,58 @@ let do_cmp = function
| Cmp_Log(dir, f) ->
ignore (compare_one_log_file dir f)
-let worker_thread () =
- while true do
- lock () ;
- if (Queue.length shared.commands) + (Queue.length shared.cmps) < !n
- then Condition.signal shared.commands_empty;
- try
- let cmp = Queue.pop shared.cmps in
- unlock () ;
- do_cmp cmp
- with Queue.Empty ->
- try
- let rec real_command () =
- let command =
- try
- if shared.building_target then raise Queue.Empty;
- Queue.pop shared.target_queue
- with Queue.Empty ->
- Queue.pop shared.commands
- in
- match command with
- Target _ ->
- if shared.building_target
- then begin
- Queue.push command shared.target_queue;
- real_command()
- end
- else begin
- shared.building_target <- true;
- command
- end
- | _ -> command
- in
- let command = real_command() in
- unlock () ;
- do_command command
- with Queue.Empty ->
- if shared.commands_finished
- && Queue.is_empty shared.target_queue
- && not shared.building_target
- (* a target being built would mean work can still appear *)
-
- then (unlock () ; Thread.exit ());
-
- Condition.signal shared.commands_empty;
- (* we still have the lock at this point *)
-
- Condition.wait shared.work_available shared.lock;
- (* this atomically releases the lock and suspends
- the thread on the condition work_available *)
-
- unlock ();
- done
+(* let worker_thread () =
+ * while true do
+ * lock () ;
+ * if (Queue.length shared.commands) + (Queue.length shared.cmps) < !n
+ * then Condition.signal shared.commands_empty;
+ * try
+ * let cmp = Queue.pop shared.cmps in
+ * unlock () ;
+ * do_cmp cmp
+ * with Queue.Empty ->
+ * try
+ * let rec real_command () =
+ * let command =
+ * try
+ * if shared.building_target then raise Queue.Empty;
+ * Queue.pop shared.target_queue
+ * with Queue.Empty ->
+ * Queue.pop shared.commands
+ * in
+ * match command with
+ * Target _ ->
+ * if shared.building_target
+ * then begin
+ * Queue.push command shared.target_queue;
+ * real_command()
+ * end
+ * else begin
+ * shared.building_target <- true;
+ * command
+ * end
+ * | _ -> command
+ * in
+ * let command = real_command() in
+ * unlock () ;
+ * do_command command
+ * with Queue.Empty ->
+ * if shared.commands_finished
+ * && Queue.is_empty shared.target_queue
+ * && not shared.building_target
+ * (\* a target being built would mean work can still appear *\)
+ *
+ * then (unlock () ; Thread.exit ());
+ *
+ * Condition.signal shared.commands_empty;
+ * (\* we still have the lock at this point *\)
+ *
+ * Condition.wait shared.work_available shared.lock;
+ * (\* this atomically releases the lock and suspends
+ * the thread on the condition work_available *\)
+ *
+ * unlock ();
+ * done *)
let diff_check_exist old_file new_file =
if Sys.file_exists old_file then begin
@@ -1535,73 +1490,71 @@ let diff_check_exist old_file new_file =
new_file ^ "\";" ^ " cat " ^ new_file
end
-let do_diff = function
- | Command_error (diff, kind) ->
- let log_prefix = log_prefix diff in
- let log_ext = log_ext kind in
- let log_file = Filename.sanitize (log_prefix ^ log_ext ^ ".log") in
- let command_string = command_string diff in
- lock_printf "%tCommand:@\n%s@." print_default_env command_string;
- if !behavior = Show
- then ignore (launch ("cat " ^ log_file))
- else
- let oracle_prefix = oracle_prefix diff in
- let oracle_file =
- Filename.sanitize (oracle_prefix ^ log_ext ^ ".oracle")
- in
- let diff_string = diff_check_exist oracle_file log_file in
- ignore (launch diff_string)
- | Target_error execnow ->
- lock_printf "Custom command failed: %s@\n" execnow.ex_cmd;
- let print_redirected out redir_str =
- try
- ignore (Str.search_forward (Str.regexp redir_str) execnow.ex_cmd 0);
- let file = Str.matched_group 1 execnow.ex_cmd in
- lock_printf "%s redirected to %s:@\n" out file;
- if not (Sys.file_exists file) then
- lock_printf "error: file does not exist: %s:@\n" file
- else
- ignore (launch ("cat " ^ file));
- with Not_found -> ()
- in
- print_redirected "stdout" "[^2]> ?\\([-a-zA-Z0-9_/.]+\\)";
- print_redirected "stderr" "2> ?\\([-a-zA-Z0-9_/.]+\\)";
- | Log_error(dir, file) ->
- let result_file =
- Filename.sanitize (SubDir.make_result_file dir file)
- in
- lock_printf "Log of %s:@." result_file;
- if !behavior = Show
- then ignore (launch ("cat " ^ result_file))
- else
- let oracle_file =
- Filename.sanitize (SubDir.make_oracle_file dir file)
- in
- let diff_string = diff_check_exist oracle_file result_file in
- ignore (launch diff_string)
-
-let diff_thread () =
- lock () ;
- while true do
- try
- let diff = Queue.pop shared.diffs in
- unlock ();
- do_diff diff;
- lock ()
- with Queue.Empty ->
- if shared.cmp_finished then (unlock () ; Thread.exit ());
-
- Condition.wait shared.diff_available shared.lock
- (* this atomically releases the lock and suspends
- the thread on the condition cmp_available *)
- done
+(* let do_diff = function
+ * | Command_error (diff, kind) ->
+ * let log_prefix = log_prefix diff in
+ * let log_ext = log_ext kind in
+ * let log_file = Filename.sanitize (log_prefix ^ log_ext ^ ".log") in
+ * let command_string,_,_ = command_string diff in
+ * lock_printf "%tCommand:@\n%s@." print_default_env command_string;
+ * if !behavior = Show
+ * then ignore (launch ("cat " ^ log_file))
+ * else
+ * let oracle_prefix = oracle_prefix diff in
+ * let oracle_file =
+ * Filename.sanitize (oracle_prefix ^ log_ext ^ ".oracle")
+ * in
+ * let diff_string = diff_check_exist oracle_file log_file in
+ * ignore (launch diff_string)
+ * | Target_error execnow ->
+ * lock_printf "Custom command failed: %s@\n" execnow.ex_cmd;
+ * let print_redirected out redir_str =
+ * try
+ * ignore (Str.search_forward (Str.regexp redir_str) execnow.ex_cmd 0);
+ * let file = Str.matched_group 1 execnow.ex_cmd in
+ * lock_printf "%s redirected to %s:@\n" out file;
+ * if not (Sys.file_exists file) then
+ * lock_printf "error: file does not exist: %s:@\n" file
+ * else
+ * ignore (launch ("cat " ^ file));
+ * with Not_found -> ()
+ * in
+ * print_redirected "stdout" "[^2]> ?\\([-a-zA-Z0-9_/.]+\\)";
+ * print_redirected "stderr" "2> ?\\([-a-zA-Z0-9_/.]+\\)";
+ * | Log_error(dir, file) ->
+ * let result_file =
+ * Filename.sanitize (SubDir.make_result_file dir file)
+ * in
+ * lock_printf "Log of %s:@." result_file;
+ * if !behavior = Show
+ * then ignore (launch ("cat " ^ result_file))
+ * else
+ * let oracle_file =
+ * Filename.sanitize (SubDir.make_oracle_file dir file)
+ * in
+ * let diff_string = diff_check_exist oracle_file result_file in
+ * ignore (launch diff_string) *)
+
+(* let diff_thread () =
+ * lock () ;
+ * while true do
+ * try
+ * let diff = Queue.pop shared.diffs in
+ * unlock ();
+ * do_diff diff;
+ * lock ()
+ * with Queue.Empty ->
+ * if shared.cmp_finished then (unlock () ; Thread.exit ());
+ *
+ * Condition.wait shared.diff_available shared.lock
+ * (\* this atomically releases the lock and suspends
+ * the thread on the condition cmp_available *\)
+ * done *)
let test_pattern config =
let regexp = Str.regexp config.dc_test_regexp in
fun file -> str_string_match regexp file 0
-let files = Queue.create ()
-
(* test for a possible toplevel configuration. *)
let default_config () =
let general_config_file = Filename.concat test_path dir_config_file in
@@ -1622,6 +1575,77 @@ let update_dir_ref dir config =
let dc_execnow = List.map update_execnow config.dc_execnow in
{ config with dc_execnow }
+let dispatcher cout file directory config =
+ Printf.fprintf cout "(alias (name ptests) (deps %S))\n" file;
+ let config =
+ scan_test_file config directory file in
+ let i = ref 0 in
+ let e = ref 0 in
+ let nb_files = List.length config.dc_toplevels in
+ let make_toplevel_cmd (toplevel, options, log_files, macros, timeout) =
+ let n = !i in
+ {file; options; toplevel; nb_files; directory; n; log_files;
+ filter = config.dc_filter; macros;
+ execnow=false; timeout;
+ }
+ in
+ let mk_cmd (s, timeout) =
+ {
+ file = file;
+ nb_files = nb_files;
+ log_files = [];
+ options = "";
+ toplevel = s;
+ n = !e;
+ directory = directory;
+ filter = config.dc_filter;
+ macros = config.dc_macros;
+ execnow = true;
+ timeout;
+ }
+ in
+ let process_macros_cmd s = basic_command_string (mk_cmd s) in
+ let macros = get_macros (mk_cmd ("/bin/true","")) in
+ let process_macros s = Macros.expand macros s in
+ let make_execnow_cmd execnow =
+ let res =
+ {
+ ex_cmd = process_macros_cmd (execnow.ex_cmd, execnow.ex_timeout);
+ ex_log = List.map process_macros execnow.ex_log;
+ ex_bin = List.map process_macros execnow.ex_bin;
+ ex_dir = execnow.ex_dir;
+ ex_once = execnow.ex_once;
+ ex_done = execnow.ex_done;
+ ex_timeout = execnow.ex_timeout;
+ }
+ in
+ incr e; res
+ in
+ let treat_option option =
+ let toplevel = make_toplevel_cmd option in
+ command_string cout toplevel;
+ incr i
+ in
+ begin
+ (match config.dc_execnow with
+ | hd :: tl ->
+ let subworkqueue = Queue.create () in
+ List.iter treat_option config.dc_toplevels;
+ let target =
+ List.fold_left
+ (fun current_target execnow ->
+ let subworkqueue = Queue.create () in
+ Queue.add current_target subworkqueue;
+ Target(make_execnow_cmd execnow,subworkqueue))
+ (Target(make_execnow_cmd hd,subworkqueue)) tl
+ in
+ Queue.push target shared.commands
+ | [] ->
+ List.iter
+ treat_option
+ config.dc_toplevels)
+ end
+
let () =
(* enqueue the test files *)
let default_suites () =
@@ -1641,30 +1665,13 @@ let () =
else x::acc
) [] l
in
- let interpret_as_file suite =
- try
- let ext = Filename.chop_extension suite in
- ext <> ""
- with Invalid_argument _ -> false
- in
- let exclude_suite, exclude_file =
- List.fold_left
- (fun (suite,test) x ->
- if interpret_as_file x then (suite,x::test) else (x::suite,test))
- ([],[]) !exclude_suites
- in
List.iter
(fun suite ->
if !verbosity >= 2 then lock_printf "%% producer now treating test %s\n%!" suite;
(* the "suite" may be a directory or a single file *)
- let interpret_as_file = interpret_as_file suite in
- let directory =
- SubDir.create (if interpret_as_file
- then
- Filename.dirname suite
- else
- suite)
- in
+ let directory = SubDir.create suite in
+ let dune_file = Filename.concat (SubDir.make_file directory SubDir.result_dirname) "dune" in
+ let cout = open_out dune_file in
let config = SubDir.make_file directory dir_config_file in
let default = default_config () in
let default = update_dir_ref directory default in
@@ -1676,159 +1683,19 @@ let () =
end
else default
in
- if interpret_as_file
- then begin
- if not (List.mem suite exclude_file) then
- Queue.push (Filename.basename suite, directory, dir_config) files
- end
- else begin
- if not (List.mem suite exclude_suite) then begin
- let dir_files = Sys.readdir (SubDir.get directory) in
- for i = 0 to pred (Array.length dir_files) do
- let file = dir_files.(i) in
- assert (Filename.is_relative file);
- if test_pattern dir_config file &&
- (not (List.mem (SubDir.make_file directory file) exclude_file))
- then Queue.push (file, directory, dir_config) files;
- done
- end
- end)
+ let dir_files = Sys.readdir (SubDir.get directory) in
+ for i = 0 to pred (Array.length dir_files) do
+ let file = dir_files.(i) in
+ assert (Filename.is_relative file);
+ if test_pattern dir_config file
+ then begin
+ dispatcher cout file directory dir_config;
+ end;
+ done;
+ close_out cout;
+ )
suites
-let dispatcher () =
- try
- while true
- do
- lock ();
- while (Queue.length shared.commands) + (Queue.length shared.cmps) >= !n
- do
- Condition.wait shared.commands_empty shared.lock;
- done;
- (* we have the lock *)
- let file, directory, config = Queue.pop files in
- let config =
- scan_test_file config directory file in
- let i = ref 0 in
- let e = ref 0 in
- let nb_files = List.length config.dc_toplevels in
- let make_toplevel_cmd (toplevel, options, log_files, macros, timeout) =
- let n = !i in
- {file; options; toplevel; nb_files; directory; n; log_files;
- filter = config.dc_filter; macros;
- execnow=false; timeout;
- }
- in
- let mk_cmd (s, timeout) =
- {
- file = file;
- nb_files = nb_files;
- log_files = [];
- options = "";
- toplevel = s;
- n = !e;
- directory = directory;
- filter = config.dc_filter;
- macros = config.dc_macros;
- execnow = true;
- timeout;
- }
- in
- let process_macros_cmd s = basic_command_string (mk_cmd s) in
- let macros = get_macros (mk_cmd ("/bin/true","")) in
- let process_macros s = Macros.expand macros s in
- let make_execnow_cmd execnow =
- let res =
- {
- ex_cmd = process_macros_cmd (execnow.ex_cmd, execnow.ex_timeout);
- ex_log = List.map process_macros execnow.ex_log;
- ex_bin = List.map process_macros execnow.ex_bin;
- ex_dir = execnow.ex_dir;
- ex_once = execnow.ex_once;
- ex_done = execnow.ex_done;
- ex_timeout = execnow.ex_timeout;
- }
- in
- incr e; res
- in
- let treat_option q option =
- Queue.push
- (Toplevel (make_toplevel_cmd option))
- q;
- incr i
- in
- if not config.dc_dont_run
- then begin
- (match config.dc_execnow with
- | hd :: tl ->
- let subworkqueue = Queue.create () in
- List.iter (treat_option subworkqueue) config.dc_toplevels;
- let target =
- List.fold_left
- (fun current_target execnow ->
- let subworkqueue = Queue.create () in
- Queue.add current_target subworkqueue;
- Target(make_execnow_cmd execnow,subworkqueue))
- (Target(make_execnow_cmd hd,subworkqueue)) tl
- in
- Queue.push target shared.commands
- | [] ->
- List.iter
- (treat_option shared.commands)
- config.dc_toplevels);
- Condition.broadcast shared.work_available;
- end;
- unlock () ;
- done
- with Queue.Empty ->
- shared.commands_finished <- true;
- unlock ()
-
-let () =
- let worker_ids = Array.init !n
- (fun _ -> Thread.create worker_thread ())
- in
- let diff_id = Thread.create diff_thread () in
-
- dispatcher ();
- if !behavior = Run
- then
- lock_printf "%% Dispatch finished, waiting for workers to complete@.";
- ignore (Thread.create
- (fun () ->
- while true do
- Condition.broadcast shared.work_available;
- Thread.delay 0.5;
- done)
- ());
- Array.iter Thread.join worker_ids;
-
- if !behavior = Run
- then
- lock_printf "%% Comparisons finished, waiting for diffs to complete@.";
- lock();
- shared.cmp_finished <- true;
- unlock();
- ignore (Thread.create
- (fun () ->
- while true do
- Condition.broadcast shared.diff_available;
- Thread.delay 0.5;
- done)
- ());
- Thread.join diff_id;
- if !behavior = Run
- then
- lock_printf "%% Diffs finished. Summary:@\nRun = %d@\nOk = %d of %d@\nTime = %f s.@."
- shared.summary_run shared.summary_ok shared.summary_log
- ((Unix.times()).Unix.tms_cutime -. shared.summary_time);
- xunit_report ();
- let error_code =
- if !do_error_code && shared.summary_log <> shared.summary_ok
- then 1
- else 0
- in
- exit error_code
-
(*
Local Variables:
compile-command: "LC_ALL=C make -C .. ptests"
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index f66cdfea26159397015ca5e3e9f46690079d38e8..e1035857bdfe7f92e9fdccb135e796ede70ddf59 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -198,7 +198,7 @@ let load_module m =
| Some _ -> load_script base
| None -> Klog.error "Missing source file '%s'" m
end
- | "" | "." | ".cmo" | ".cma" | ".cmxs" ->
+ | _ ->
begin
(* load object or compile script or find package *)
match is_object base with
@@ -207,15 +207,16 @@ let load_module m =
match is_file base ".ml" with
| Some _ -> load_script base
| None ->
- if is_package m then load_packages [m]
+ if is_package m && Dune_site_plugins.V1.available m then load_packages [m]
else
let fc =
"frama-c-" ^ String.lowercase_ascii m
in
load_packages [fc]
end
- | _ ->
- Klog.error "don't know what to do with '%s' (unexpected %s)" m ext
+
+let load_plugin m =
+ Config_data.Plugins.Plugins.load m
(* ************************************************************************* *)
(** {2 Registering and accessing dynamic values} *)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index cf663dc88ff45bfbb3b31aee709d84a8727869c3..dc0947a0a3aab57ad0ba3d01c4865c7709e8474a 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -153,6 +153,8 @@ val load_module: string -> unit
(** Load the module specification. See -load-module option.
@modify Magnesium-20151001 new API. *)
+val load_plugin: string -> unit
+
(** Sets the load path for modules in FRAMAC_PLUGIN, prepending it with [path].
Does not load any plugins.
Must be invoked only once from boot during extending stage.
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index be9e4b003541e6de9630fbbb02d6ff64740e5e5c..5402977b89ee2ae8f19028fe6015c61c7c522784 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -812,7 +812,7 @@ module LoadModule =
let option_name = "-load-module"
let module_name = "LoadModule"
let arg_name = "SPEC,..."
- let help = "Dynamically load plug-ins, modules and scripts. \
+ let help = "Dynamically load modules and scripts. \
Each <SPEC> can be an OCaml source or object file, with \
or without extension, or a Findlib package. \
Loading order is preserved and \
@@ -820,6 +820,19 @@ module LoadModule =
end)
let () = LoadModule.add_aliases [ "-load-script" ]
+let () = Parameter_customize.set_group saveload
+let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
+let () = Parameter_customize.do_not_projectify ()
+module LoadPlugin =
+ String_list
+ (struct
+ let option_name = "-load-plugin"
+ let module_name = "LoadPlugin"
+ let arg_name = "SPEC,..."
+ let help = "Dynamically load plug-ins. \
+ Loading order is preserved."
+ end)
+
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.do_not_projectify ()
@@ -835,6 +848,7 @@ let bootstrap_loader () =
begin
Dynamic.set_module_load_path (AddPath.get ());
if AutoLoadPlugins.get () then Dynamic.load_plugin_path () ;
+ List.iter Dynamic.load_plugin (LoadPlugin.get()) ;
List.iter Dynamic.load_module (LoadModule.get()) ;
end
diff --git a/src/plugins/aorai/dune b/src/plugins/aorai/dune
index b1073c1cbd487930474de3de9388046a8a6a02b0..d5466a4fca006d32d3708b54bd5af26d9d337e06 100644
--- a/src/plugins/aorai/dune
+++ b/src/plugins/aorai/dune
@@ -8,4 +8,4 @@
(ocamllex promelalexer_withexps promelalexer ltllexer yalexer)
(ocamlyacc promelaparser_withexps promelaparser ltlparser yaparser)
-(plugin (name frama-c-plugins-aorai) (libraries frama-c-aorai.core) (site (frama-c plugins)))
+(plugin (name aorai) (libraries frama-c-aorai.core) (site (frama-c plugins)))
diff --git a/src/plugins/callgraph/dune b/src/plugins/callgraph/dune
index e491ec6eb5d0c590f079702bfdeaaf180e481fb5..21543299dd55d610e736bbd142386d16f17cf133 100644
--- a/src/plugins/callgraph/dune
+++ b/src/plugins/callgraph/dune
@@ -7,7 +7,7 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins)))
+(plugin (name callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins)))
( library
(name callgraph_gui)
@@ -19,4 +19,4 @@
(libraries callgraph frama-c.kernel frama-c.gui)
)
-(plugin (name frama-c-plugins-callgraph) (libraries frama-c-callgraph.gui) (site (frama-c plugins_gui)))
+(plugin (name callgraph) (libraries frama-c-callgraph.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index d30cb23a713ecb602462cfdc6996e326111ab967..5e72a8f200a9a1829cdd0e0483a6254f729b1f6f 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-constant_propagation) (libraries frama-c-constant_propagation.core) (site (frama-c plugins)))
+(plugin (name constant_propagation) (libraries frama-c-constant_propagation.core) (site (frama-c plugins)))
diff --git a/src/plugins/dive/dune b/src/plugins/dive/dune
index cc86e48cebdd17851e7edeb1da5014bae4cd2d78..131b5d5fbaef815399c716a53bd9e46151bf7d0b 100644
--- a/src/plugins/dive/dune
+++ b/src/plugins/dive/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-studia.core frama-c-server.core)
)
-(plugin (name frama-c-plugins-dive) (libraries frama-c-dive.core) (site (frama-c plugins)))
+(plugin (name dive) (libraries frama-c-dive.core) (site (frama-c plugins)))
diff --git a/src/plugins/e-acsl/dune b/src/plugins/e-acsl/dune
index f61d74412ed9268c383dcd5bbb79266d77e1c0a3..20fe8f9fd7b37f2ae5700d5e209ff61d1401f02a 100644
--- a/src/plugins/e-acsl/dune
+++ b/src/plugins/e-acsl/dune
@@ -5,7 +5,7 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins)))
+(plugin (name e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins)))
(copy_files# src/*.ml*)
(copy_files# src/analyses/*.ml*)
diff --git a/src/plugins/from/dune b/src/plugins/from/dune
index 3bdf9591656387ee1c429aa43e3c3dc0767e7cf2..7dee51648effd8004c2da646cb49d0a7cd37f0f6 100644
--- a/src/plugins/from/dune
+++ b/src/plugins/from/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core)
)
-(plugin (name frama-c-plugins-from) (libraries frama-c-from.core) (site (frama-c plugins)))
+(plugin (name from) (libraries frama-c-from.core) (site (frama-c plugins)))
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index e4b26bb7b4642f3402d63467b56def937183129e..de4569fa276452a51d62554e8f88e2196122002d 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
)
-(plugin (name frama-c-plugins-impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
+(plugin (name impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
diff --git a/src/plugins/inout/dune b/src/plugins/inout/dune
index 0560845e12c0d8a74f5a807767909193fda7ae47..29f2c98a08e3f34e18dfd9aa43434d073a08dab8 100644
--- a/src/plugins/inout/dune
+++ b/src/plugins/inout/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-from.core)
)
-(plugin (name frama-c-plugins-inout) (libraries frama-c-inout.core) (site (frama-c plugins)))
+(plugin (name inout) (libraries frama-c-inout.core) (site (frama-c plugins)))
diff --git a/src/plugins/instantiate/dune b/src/plugins/instantiate/dune
index 959aeac29829decb29f258dcca960bc316d216d1..26342cf2b66bc9649fdfb19fc0d475edd64f1b54 100644
--- a/src/plugins/instantiate/dune
+++ b/src/plugins/instantiate/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-instantiate) (libraries frama-c-instantiate.core) (site (frama-c plugins)))
+(plugin (name instantiate) (libraries frama-c-instantiate.core) (site (frama-c plugins)))
diff --git a/src/plugins/loop_analysis/dune b/src/plugins/loop_analysis/dune
index 70ffc9d6371bf9fe4008cdddc6610169d5ec031b..e44d6fe6b24e10a33c1e58611b32db3822c4282e 100644
--- a/src/plugins/loop_analysis/dune
+++ b/src/plugins/loop_analysis/dune
@@ -7,4 +7,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-loop-analysis) (libraries frama-c-loop-analysis.core) (site (frama-c plugins)))
+(plugin (name loop-analysis) (libraries frama-c-loop-analysis.core) (site (frama-c plugins)))
diff --git a/src/plugins/markdown-report/dune b/src/plugins/markdown-report/dune
index 18c46eaac3820d6c1dcc6f6e0e263ee7287e3c3d..0be220a665f59588b166f60bb7bad88e9717e6d1 100644
--- a/src/plugins/markdown-report/dune
+++ b/src/plugins/markdown-report/dune
@@ -7,4 +7,4 @@
(preprocess (pps ppx_deriving_yojson))
)
-(plugin (name frama-c-plugins-markdown-report) (libraries frama-c-markdown-report.core) (site (frama-c plugins)))
+(plugin (name markdown-report) (libraries frama-c-markdown-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune
index 3240bb3407ff88e49c9a029098a415703d21a093..135e423b3915f2c47250e557d80b1230a4982b39 100644
--- a/src/plugins/metrics/dune
+++ b/src/plugins/metrics/dune
@@ -8,7 +8,7 @@
(libraries frama-c.kernel frama-c-eva.core)
)
-(plugin (name frama-c-plugins-metrics) (libraries frama-c-metrics.core) (site (frama-c plugins)))
+(plugin (name metrics) (libraries frama-c-metrics.core) (site (frama-c plugins)))
( library
(name metrics_gui)
@@ -19,4 +19,4 @@
(libraries metrics frama-c.kernel frama-c.gui)
)
-(plugin (name frama-c-plugins-metrics) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui)))
+(plugin (name metrics) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/nonterm/dune b/src/plugins/nonterm/dune
index 78bb592a89a316a16002876c12d9746750881ea4..a43c9a5c53facb6ea21b0a85800dcfdd7cec388b 100644
--- a/src/plugins/nonterm/dune
+++ b/src/plugins/nonterm/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-nonterm) (libraries frama-c-nonterm.core) (site (frama-c plugins)))
+(plugin (name nonterm) (libraries frama-c-nonterm.core) (site (frama-c plugins)))
diff --git a/src/plugins/obfuscator/dune b/src/plugins/obfuscator/dune
index 6a71414de99e327169817291b7299f1e0acc5c9d..ecc6dda28ed138845bb222d4c9661236462a6061 100644
--- a/src/plugins/obfuscator/dune
+++ b/src/plugins/obfuscator/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-obfuscator) (libraries frama-c-obfuscator.core) (site (frama-c plugins)))
+(plugin (name obfuscator) (libraries frama-c-obfuscator.core) (site (frama-c plugins)))
diff --git a/src/plugins/occurrence/dune b/src/plugins/occurrence/dune
index 27e25ec02f3a1f1933bd96fe938f0a687e8fd5bc..c6851f4b2561550c8949087709b9fbe8a601d1c8 100644
--- a/src/plugins/occurrence/dune
+++ b/src/plugins/occurrence/dune
@@ -6,7 +6,7 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins)))
+(plugin (name occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins)))
( library
(name occurrence_gui)
@@ -17,4 +17,4 @@
(libraries occurrence frama-c.kernel frama-c.gui)
)
-(plugin (name frama-c-plugins-occurrence) (libraries frama-c-occurrence.gui) (site (frama-c plugins_gui)))
+(plugin (name occurrence) (libraries frama-c-occurrence.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 0ff2e85ddae88ce0412d8c7f32a91efa35b770ba..6db34c87a84796f22a70ce3eb741fd6d56d13f00 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
)
-(plugin (name frama-c-plugins-pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
+(plugin (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index 696623c9896bd9c2244c833de2f03d48fdb77284..a5d6bfaf051a2482841e320e1dd5f574493adc63 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
+(plugin (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/print_api/dune b/src/plugins/print_api/dune
index ad864970a02de07731d94653a24778a8076537b9..2dac1ebe3ee72fdbc1fb32b5f3de52d6bd9f6722 100644
--- a/src/plugins/print_api/dune
+++ b/src/plugins/print_api/dune
@@ -5,4 +5,4 @@
; (libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core)
; )
-; (plugin (name frama-c-plugins-print_api) (libraries frama-c-print_api.core) (site (frama-c plugins)))
+; (plugin (name print_api) (libraries frama-c-print_api.core) (site (frama-c plugins)))
diff --git a/src/plugins/report/dune b/src/plugins/report/dune
index a5c8e6f7f575133d649cfcb305fb5745432ac00b..1f3b331d61376e614426fcf48ca7a95235bc1279 100644
--- a/src/plugins/report/dune
+++ b/src/plugins/report/dune
@@ -7,4 +7,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-report) (libraries frama-c-report.core) (site (frama-c plugins)))
+(plugin (name report) (libraries frama-c-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune
index 585f60e1a9690da86293277fc16c3cc206120b9a..fa80e089e24daf7b5cca26c15803379e1cd8220f 100644
--- a/src/plugins/rte/dune
+++ b/src/plugins/rte/dune
@@ -6,4 +6,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-rtegen) (libraries frama-c-rtegen.core) (site (frama-c plugins)))
+(plugin (name rtegen) (libraries frama-c-rtegen.core) (site (frama-c plugins)))
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 95bc60aace09b2299a2bd1215b3223b27ed5a6fb..0416e08f88ce76f5399dc05f928dfc3230a3d221 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -15,5 +15,5 @@
(libraries frama-c.kernel frama-c.gui frama-c-scope.core)
)
-(plugin (name frama-c-plugins-scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
-(plugin (name frama-c-plugins-scope) (libraries frama-c-scope.gui) (site (frama-c plugins_gui)))
+(plugin (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
+(plugin (name scope) (libraries frama-c-scope.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index 0067ab236e44e18ce847be78d7c0a2c5e9728a2a..44daa472ecde8c2f5ea9f2d21506f1cdee835409 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -6,7 +6,7 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
+(plugin (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
( library
@@ -18,4 +18,4 @@
(libraries security_slicing frama-c.kernel frama-c.gui)
)
-(plugin (name frama-c-plugins-security_slicing) (libraries frama-c-security_slicing.gui) (site (frama-c plugins_gui)))
+(plugin (name security_slicing) (libraries frama-c-security_slicing.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/server/dune b/src/plugins/server/dune
index 509a77579bcdb4b041f4165a59af6f86a532f283..311f16add680fe5155291ab418e44824b837ac86 100644
--- a/src/plugins/server/dune
+++ b/src/plugins/server/dune
@@ -9,4 +9,4 @@
))
)
-(plugin (name frama-c-plugins-server) (libraries frama-c-server.core) (site (frama-c plugins)))
+(plugin (name server) (libraries frama-c-server.core) (site (frama-c plugins)))
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index d6e78e23d47fb626bd3dbd4ffe64a561e71076c8..ccb2f28636eece737f7afff36e24de57a77456ed 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core)
)
-(plugin (name frama-c-plugins-slicing) (libraries frama-c-slicing.core) (site (frama-c plugins)))
+(plugin (name slicing) (libraries frama-c-slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/sparecode/dune b/src/plugins/sparecode/dune
index c81c4d44ec376d0773a5f800ec0c9d132dec9bff..756d81267b8eb350292f519cf4e134518fa18167 100644
--- a/src/plugins/sparecode/dune
+++ b/src/plugins/sparecode/dune
@@ -6,4 +6,4 @@
(libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core)
)
-(plugin (name frama-c-plugins-sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins)))
+(plugin (name sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins)))
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index 691a1b91ae8c85b6d834be270bcfe4e75bbf757e..7cc32fc031d10ee168aa86f45d2e4ad4b9d2791f 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -6,7 +6,7 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-studia) (libraries frama-c-studia.core) (site (frama-c plugins)))
+(plugin (name studia) (libraries frama-c-studia.core) (site (frama-c plugins)))
( library
@@ -18,4 +18,4 @@
(libraries studia frama-c.kernel frama-c.gui frama-c-eva.gui)
)
-(plugin (name frama-c-plugins-studia) (libraries frama-c-studia.gui) (site (frama-c plugins_gui)))
+(plugin (name studia) (libraries frama-c-studia.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/users/dune b/src/plugins/users/dune
index f3a9ef31adc4fcda474299c18ae190107fbb235f..660b57e7ed19781991e234f1de415ac9e388d9b5 100644
--- a/src/plugins/users/dune
+++ b/src/plugins/users/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel frama-c-callgraph.core)
)
-(plugin (name frama-c-plugins-users) (libraries frama-c-users.core) (site (frama-c plugins)))
+(plugin (name users) (libraries frama-c-users.core) (site (frama-c plugins)))
diff --git a/src/plugins/value/dune b/src/plugins/value/dune
index 62af8574299546302fafa950636ffba0975fe16c..68f3533d98e3aa2e4056010adc0ca1df9c0efd35 100644
--- a/src/plugins/value/dune
+++ b/src/plugins/value/dune
@@ -58,7 +58,7 @@
(libraries frama-c.kernel frama-c-callgraph.core frama-c-rtegen.core frama-c-loop-analysis.core frama-c-scope.core)
)
-(plugin (name frama-c-plugins-eva) (libraries frama-c-eva.core) (site (frama-c plugins)))
+(plugin (name eva) (libraries frama-c-eva.core) (site (frama-c plugins)))
( library
(name numerors)
@@ -69,7 +69,7 @@
(optional)
)
-;(plugin (name frama-c-plugins-eva-numerors) (libraries frama-c-eva.numerors) (site (frama-c plugins)))
+;(plugin (name eva-numerors) (libraries frama-c-eva.numerors) (site (frama-c plugins)))
( library
(name apron_domain)
@@ -92,7 +92,7 @@
(libraries eva frama-c.kernel frama-c.gui)
)
-(plugin (name frama-c-plugins-eva-gui) (libraries frama-c-eva.gui) (site (frama-c plugins_gui)))
+(plugin (name eva-gui) (libraries frama-c-eva.gui) (site (frama-c plugins_gui)))
(copy_files# domains/*)
(copy_files# domains/equality/*)
diff --git a/src/plugins/variadic/dune b/src/plugins/variadic/dune
index 19a8a03154ab3f15f2dda2427b0c5a2eddc38594..f0e9c5b84458c03893a086cd776ba30d713b7f52 100644
--- a/src/plugins/variadic/dune
+++ b/src/plugins/variadic/dune
@@ -5,4 +5,4 @@
(libraries frama-c.kernel)
)
-(plugin (name frama-c-plugins-variadic) (libraries frama-c-variadic.core) (site (frama-c plugins)))
+(plugin (name variadic) (libraries frama-c-variadic.core) (site (frama-c plugins)))
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 0e648a050ac2babe59602ad1e38a9f38723a64b9..c2d2789e34a2a30a8d8925600189ecacefb5991d 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -5,7 +5,7 @@
(libraries frama-c.kernel why3 qed zarith ocamlgraph)
)
-(plugin (name frama-c-plugins-wp) (libraries frama-c-wp.core) (site (frama-c plugins)))
+(plugin (name wp) (libraries frama-c-wp.core) (site (frama-c plugins)))
(ocamllex driver rformat script)
diff --git a/tests/.gitignore b/tests/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..cc129cb16f5d6dfdc679d5fb58ea08837ae58cb6
--- /dev/null
+++ b/tests/.gitignore
@@ -0,0 +1 @@
+**/dune