diff --git a/.gitignore b/.gitignore
index 0c9a3ffad1279180824a46972c05496b083c2975..636040ada80e28913493dbc55c1c8815751ea412 100644
--- a/.gitignore
+++ b/.gitignore
@@ -59,7 +59,6 @@ autom4te.cache
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
-/tests/spec/preprocess_dos.c
/tests/*/*.opt
/devel_tools/fc-time
diff --git a/dune-project b/dune-project
index 25c7d8d3861402277fd5f80171c78b6613921bb7..acebea6b4983d92807c188bcd83d32ef624b4e98 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/headers/dune-project b/headers/dune-project
index fbf0f7596d7c6516f5ff8dfdf77da73007aa5b0a..3a50a77564ad624c2ef212b0448c2bc7e92281e3 100644
--- a/headers/dune-project
+++ b/headers/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/headers/hdrck.ml b/headers/hdrck.ml
index cb620a850c1b874908afffc8d9b22a6ec064b00d..e8fd61024ec531b223e662b26ccf70d4aac4ae5d 100644
--- a/headers/hdrck.ml
+++ b/headers/hdrck.ml
@@ -592,10 +592,6 @@ let check_headache_config_file () =
let set_opt (var:'a option ref) (value:'a) = var := Some value
-let get_opt = function
- | None -> assert false
- | Some v -> v
-
let executable_name = Sys.argv.(0)
let umsg =
diff --git a/ptests/dune-project b/ptests/dune-project
index f1d0ae6fb8abc78f00208e171b3534bb2ee0930a..c4f77831ca36459149f84d772cf80397a5c2c508 100644
--- a/ptests/dune-project
+++ b/ptests/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 237390a125c21138f9a0165921223c76e89e6aa5..13254fdc71308c2a8615f2d77739283e874eb773 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -62,6 +62,7 @@ module Filename = struct
fun a b -> cygpath (temp_file a b)
else
fun a b -> temp_file a b
+ [@@ warning "-32"]
let sanitize f = String.escaped f
@@ -107,8 +108,6 @@ let trim_right s =
(** the pattern that ends the parsing of options in a test file *)
let end_comment = Str.regexp ".*\\*/"
-let regex_cmxs = Str.regexp ("\\([^/]+\\)[.]cmxs\\($\\|[ \t]\\)")
-
let output_unix_error (exn : exn) =
match exn with
| Unix.Unix_error (error, _function, arg) ->
@@ -124,6 +123,7 @@ let mv src dest =
Unix.rename src dest
with Unix.Unix_error _ as e ->
output_unix_error e
+[@@ warning "-32"]
let unlink ?(silent = true) file =
let open Unix in
@@ -275,7 +275,7 @@ let example_msg =
let umsg = "Usage: frama-c-ptests [options] [names of test suites]"
let default_dune_alias = ref "ptests"
-let rec argspec =
+let argspec =
[
("-v", Arg.Unit (fun () -> incr verbosity),
"Increase verbosity (up to twice)") ;
@@ -317,7 +317,6 @@ let rec argspec =
("-dune-alias", Arg.String (fun s -> default_dune_alias := s),
" <name> Use @<name> as dune alias to exectute tests (defaults to "^ !default_dune_alias ^")");
]
-and help_msg () = Arg.usage (Arg.align argspec) umsg
let fail s =
Format.printf "Error: %s@.Aborting (CWD=%s).@." s (Sys.getcwd());
@@ -419,7 +418,6 @@ module SubDir: sig
Anyway, fails if the given dirname doesn't exists *)
val make_file: t -> string -> string
- val make_subdir: t -> string -> t
val oracle_subdir: env:env_t -> t -> t
val result_subdir: env:env_t -> t -> t
@@ -443,7 +441,6 @@ end = struct
let result_subdir ~env dir = Filename.concat dir (config_name ~env "result")
let make_file = Filename.concat
- let make_subdir = Filename.concat
let oracle_dir ~env = oracle_subdir ~env ".."
let get_oracle_dir = oracle_dir
@@ -474,8 +471,6 @@ module Macros = struct
let empty = StringMap.empty
- let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
-
let pp_macros fmt macros =
Format.fprintf fmt "Macros (%d):@." (StringMap.cardinal macros);
StringMap.iter (fun key data -> Format.fprintf fmt "- %s -> %s@." key data) macros;
@@ -546,8 +541,10 @@ module Macros = struct
let s = expand ~file macros s in
if String.equal s "" then None else Some s) ls
- let get ?(default="") name macros =
- try StringMap.find name macros with Not_found -> default
+ let expand_enabled_if ~file (macros:t) enabled_if =
+ Option.map (fun s ->
+ let s = String.trim (expand ~file macros s) in
+ if s = "" then "true" else s) enabled_if
let add_list l map =
List.fold_left (fun acc (k,v) -> StringMap.add k v acc) map l
@@ -555,9 +552,6 @@ module Macros = struct
let add_expand ~file name def macros =
StringMap.add name (expand ~file macros def) macros
- let append_expand ~file name def macros =
- StringMap.add name (get name macros ^ expand ~file macros def) macros
-
let default_macros () = add_list
[ "frama-c-exe", !macro_frama_c_exe;
"frama-c-cmd", !macro_frama_c_cmd;
@@ -576,6 +570,7 @@ module Macros = struct
"PTEST_MODULE", "";
"PTEST_SCRIPT", "";
"PTEST_PLUGIN", "";
+ "PTEST_ENABLED_IF", "true";
] empty
end
@@ -586,6 +581,7 @@ type deps = {
load_libs: string list option;
load_module: string list option;
deps_cmd: string list option;
+ enabled_if: string option;
}
type execnow =
@@ -619,6 +615,7 @@ type config =
*)
dc_libs : string list option; (** libraries to compile *)
dc_deps : string list option ; (** deps *)
+ dc_enabled_if : string option ; (** enabled if condition *)
dc_plugin : string list option; (** only plugins to load *)
dc_module : string list option; (** module to load *)
dc_macros: Macros.t; (** existing macros. *)
@@ -670,11 +667,13 @@ end = struct
"PTEST_FILE", ptest_file;
"PTEST_NAME", ptest_name;
] in
- let subst = Macros.expand_list ~file
- (Macros.add_list ptest_vars Macros.empty)
+ let ptest_macros = Macros.add_list ptest_vars Macros.empty in
+ let subst = Macros.expand_list ~file ptest_macros in
+ let dc_enabled_if = Macros.expand_enabled_if ~file ptest_macros config.dc_enabled_if
in
ptest_name,
{ config with
+ dc_enabled_if;
dc_execnow = List.rev config.dc_execnow;
dc_deps = Option.map subst config.dc_deps ;
dc_plugin = Option.map subst config.dc_plugin;
@@ -698,6 +697,7 @@ end = struct
load_libs=None;
load_module=None;
deps_cmd=None;
+ enabled_if=None;
};
timeout=""
} ]
@@ -709,6 +709,7 @@ end = struct
dc_execnow = [];
dc_libs = None;
dc_deps = None;
+ dc_enabled_if = None;
dc_plugin = None;
dc_module = None;
dc_filter = None ;
@@ -788,7 +789,7 @@ end = struct
(* preserve options ordering *)
List.fold_right (fun x s -> s ^ " " ^ x) opts ""
- let deps_of_config ?(deps={load_module=None;load_libs=None;load_plugin=None;deps_cmd=None}) config =
+ let deps_of_config ?(deps={load_module=None;load_libs=None;load_plugin=None;deps_cmd=None;enabled_if=None}) config =
let select ~prev ~config = match config with
| None -> prev
| _ -> config
@@ -796,7 +797,8 @@ end = struct
{ load_module = select ~prev:deps.load_module ~config:config.dc_module;
load_plugin = select ~prev:deps.load_plugin ~config:config.dc_plugin;
load_libs= select ~prev:deps.load_libs ~config:config.dc_libs;
- deps_cmd = select ~prev:deps.deps_cmd ~config:config.dc_deps
+ deps_cmd = select ~prev:deps.deps_cmd ~config:config.dc_deps;
+ enabled_if = select ~prev:deps.enabled_if ~config:config.dc_enabled_if
}
let config_exec ~once ~drop:_ ~file ~dir s current =
@@ -828,6 +830,13 @@ end = struct
let _,_,res = (add "" acc) in
res
+ let config_enabled_if ~drop:_ ~file ~dir:_ s current =
+ let s = Macros.expand ~file current.dc_macros s in
+ let s = if s = "" then "true" else s in
+ { current with
+ dc_enabled_if = Some s;
+ dc_macros = Macros.add_list ["PTEST_ENABLED_IF", s] current.dc_macros }
+
let config_deps ~drop:_ ~file ~dir:_ s current =
let s = Macros.expand ~file current.dc_macros s in
let l = split_list s in
@@ -985,6 +994,7 @@ end = struct
"MACRO", config_macro;
"LIBS", config_libs;
"DEPS", config_deps;
+ "ENABLED_IF", config_enabled_if;
"MODULE", config_module "PTEST_MODULE";
"SCRIPT", config_module "PTEST_SCRIPT";
"PLUGIN", config_plugin;
@@ -1019,12 +1029,12 @@ end = struct
let r = ref { default with dc_commands = [] } in
let treat_line s =
try
- Scanf.sscanf s "%[ *]%[A-Za-z0-9]: %s@\n"
+ Scanf.sscanf s "%[ *]%[_A-Za-z0-9]: %s@\n"
(fun _ name opt ->
try
r := (List.assoc name config_options) ~drop ~file ~dir opt !r
with Not_found ->
- Format.eprintf "@[%s: unknown configuration option: %s@.@]" file name)
+ Format.eprintf "@[%s: unknown directive: %s@.@]" file name)
with
| Scanf.Scan_failure _ ->
if Str.string_match end_comment s 0
@@ -1143,21 +1153,6 @@ type toplevel_command =
deps: deps;
}
-type command =
- | Toplevel of toplevel_command
- | Target of execnow * command Queue.t
-
-type log = Err | Res
-
-type diff =
- | Command_error of toplevel_command * log
- | Target_error of execnow
- | Log_error of SubDir.t (* directory *) * string (* file *)
-
-type cmps =
- | Cmp_Toplevel of toplevel_command
- | Cmp_Log of SubDir.t (* directory *) * string (* file *)
-
let catenate_number nb_files prefix n =
if nb_files > 1
then prefix ^ "." ^ (string_of_int n)
@@ -1264,6 +1259,11 @@ let pp_list_deps fmt l =
(* kind={env_var,source_tree,glob_files,...} *)
Format.fprintf fmt " (%s %S)" kind deps) l
+let pp_enabled_if fmt deps =
+ Format.fprintf fmt "(and %s%a)"
+ (Option.value ~default:"true" deps.enabled_if)
+ Fmt.(list (var_libavailable framac_plugin)) (list_of_deps deps.load_plugin)
+
let pp_command_deps fmt command =
Format.fprintf fmt "%S %a (package frama-c) %a"
(* the test file *)
@@ -1408,7 +1408,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %S %S %S %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (run %s %S %S %a))\n\
)@."
(* rule: *)
@@ -1427,7 +1427,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
pp_list (List.map (Filename.concat wtest.oracle_dir) command.log_files)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
!wrapper_cmd
wrapper_basename
@@ -1451,7 +1451,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (with-stderr-to %S (with-stdout-to %S (%s (system %S)))))\n\
)@."
(* rule: *)
@@ -1466,7 +1466,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
cmderrlog
cmdreslog
@@ -1478,7 +1478,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; FILTER %s #%d OF TEST FILE %S\n \
(deps %S)
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\
)@."
(* rule: *)
@@ -1488,7 +1488,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
fin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
fout cmd
in
@@ -1498,7 +1498,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF TEST #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* rule: *)
@@ -1506,7 +1506,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* alias: *)
(ptests_alias ~env)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
(SubDir.make_file (SubDir.oracle_dir ~env) log)
log
@@ -1515,7 +1515,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; REPRODUCE TEST #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (%s (system %S)))\n\
)@."
(* rule: *)
@@ -1525,7 +1525,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
accepted_exit_code
command_string
@@ -1534,7 +1534,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; SHOW TEST COMMAND #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1544,7 +1544,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command (* to get an updated build even in case of using the result *)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'");
@@ -1553,37 +1553,37 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
diff_alias
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
wtest.oracle_out
reslog;
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
diff_alias
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
wtest.oracle_err
errlog;
Format.fprintf result_fmt
"(alias (name %S)\n \
(deps (alias %S))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
)@."
(ptests_alias ~env)
diff_alias
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
;
let oracle_subdir = SubDir.oracle_subdir ~env command.directory in
oracle_target oracle_fmt oracle_subdir (Filename.basename (oracle_prefix ^ ".err.oracle"));
@@ -1593,11 +1593,12 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
let deps_command ~file macros deps =
let subst = Macros.expand_list ~file macros in
+ let enabled_if = Macros.expand_enabled_if ~file macros deps.enabled_if in
let load_plugin = Option.map subst deps.load_plugin in
let load_module = Option.map subst deps.load_module in
let load_libs = Option.map (fun libs -> List.map (fun s -> s^".cmxs") (subst libs)) deps.load_libs in
let deps_cmd = Option.map subst deps.deps_cmd in
- { load_plugin; load_module; load_libs;
+ { enabled_if; load_plugin; load_module; load_libs;
(* Merge LIBS: MODULE: and DEPS: directives as a dependency to files *)
deps_cmd = Some ((list_of_deps load_libs) @ (list_of_deps load_module) @ (list_of_deps deps_cmd));
}
@@ -1697,7 +1698,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps %a %a)\n \
(targets %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (run %s %%{dep:%s} %S))\n\
)@."
(* rule: *)
@@ -1711,7 +1712,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
pp_list wtest.log
pp_list wtest.bin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
!wrapper_cmd
wrapper_basename
@@ -1731,7 +1732,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps (package frama-c)%a)\n \
(targets %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1744,7 +1745,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
pp_list wtest.log
pp_list wtest.bin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
wtest.cmd
end;
@@ -1755,7 +1756,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
"(rule ; SHOW EXECNOW COMMAND #%d OF TEST FILE %S\n \
(alias %s)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1765,7 +1766,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(* deps: *)
pp_command_deps cmd (* to get an updated build even in case of using the result *)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'");
;
@@ -1773,7 +1774,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF EXECNOW #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* rule: *)
@@ -1781,7 +1782,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(* alias: *)
(ptests_alias ~env)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
(SubDir.make_file (SubDir.oracle_dir ~env) log)
log
diff --git a/src/plugins/aorai/dune-project b/src/plugins/aorai/dune-project
index d7317b50ddbb90e03fc21e044cb2b8449ea987f3..6310f54128592bdb3969562b7a0000369b24fd76 100644
--- a/src/plugins/aorai/dune-project
+++ b/src/plugins/aorai/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Aorai plug-in of Frama-C. ;;
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index abaf6d16f737c744fb157a8d30f8b150e562dcef..b8685eec176b5ff0400d728af807018ade5571ee 100644
--- a/src/plugins/aorai/tests/ltl/goto.c
+++ b/src/plugins/aorai/tests/ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index 6325177b5bd437c00db0b8dfde3cf6e93afdfe76..242401c8d41a5c9b4a97646e6c6c5cebeae180d8 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c
index b66e6a7c829a6641fee515eb30d1d5d629babb42..3f24248397ef975cbd10cb7b8f794b5735b7bdcd 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle1.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c
index 257a9a19b810a573fd18230f49c00c6d9eb04c2d..a37e79e10971fbe6ed463bf315bfa4fbcbc60704 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle2.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c
index 1cdc2b029c0761d92a9581b3357538be358e2cfc..3cd384b94a561399d1536d315f09008026ec004e 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle3.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
diff --git a/src/plugins/aorai/tests/ltl/test_config b/src/plugins/aorai/tests/ltl/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..96c1d0d716a3ae949b1bd19b2fd92a2b13ccfbd8
--- /dev/null
+++ b/src/plugins/aorai/tests/ltl/test_config
@@ -0,0 +1,2 @@
+ENABLED_IF: %{bin-available:ltl2ba}
+STDOPT:
diff --git a/src/plugins/aorai/tests/ltl/test_config_prove b/src/plugins/aorai/tests/ltl/test_config_prove
new file mode 100644
index 0000000000000000000000000000000000000000..96c1d0d716a3ae949b1bd19b2fd92a2b13ccfbd8
--- /dev/null
+++ b/src/plugins/aorai/tests/ltl/test_config_prove
@@ -0,0 +1,2 @@
+ENABLED_IF: %{bin-available:ltl2ba}
+STDOPT:
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 313ecfbaa750192ad1cdd36a783fbcb75034e141..009b6db869a7439b1fcda0bd16ea439e39b00490 100644
--- a/src/plugins/aorai/tests/ltl/test_factorial.c
+++ b/src/plugins/aorai/tests/ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl}
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index a3f69a89db840f6a582edc7e2c8eaec921b3354e..bed9bf66e83256498aae83e2faa46b693e5cb92c 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion1.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index 7effcb5bfed5a06821d505ee9632fce32bffdcc0..a51847f8c6b5473bd08eb35f9ffa995b2b6b11e6 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion2.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance
- STDOPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance
+ STDOPT: -aorai-buchi %{dep:@PTEST_NAME@.promela} -aorai-acceptance
+ STDOPT: -aorai-buchi %{dep:test_recursion3.promela} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c
index 637be79d815d361f9bfc46c8a9e4a5ed15a33768..77290f3f226e7c9f42bac747c78b41f648e1232b 100644
--- a/src/plugins/aorai/tests/ltl/test_switch2.c
+++ b/src/plugins/aorai/tests/ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c
index 037f58fb2c440a7277b5aed83fb53308be15fde5..090c0769545f6092b0ef082458e88f1153e6059a 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
index 9ef5f759998d7cbc088c6db9030f90ee378ac2ca..9756ddb36ee09942926236b1920eb63db685071e 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ptests_config b/src/plugins/aorai/tests/ptests_config
index 34b21cc61881d5f098943d7647fde26effacf51e..7fc044169e395ade683964186f5cbf36c046eea5 100644
--- a/src/plugins/aorai/tests/ptests_config
+++ b/src/plugins/aorai/tests/ptests_config
@@ -1,2 +1,2 @@
-DEFAULT_SUITES= ya
-prove_SUITES= ya
+DEFAULT_SUITES= ya ltl
+prove_SUITES= ya ltl
diff --git a/src/plugins/api-generator/dune-project b/src/plugins/api-generator/dune-project
index bbff6793075aec958bdc1f7458c3101b437a75a9..572790587d344dcbc049c3f6cabe6a6302532763 100644
--- a/src/plugins/api-generator/dune-project
+++ b/src/plugins/api-generator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/callgraph/dune-project b/src/plugins/callgraph/dune-project
index 95a622cf6c73fea62d85b4f9a1ac1760f8448e7d..f0c8f918da8eee6f140dc0ccec184570c1d9fe56 100644
--- a/src/plugins/callgraph/dune-project
+++ b/src/plugins/callgraph/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/constant_propagation/dune-project b/src/plugins/constant_propagation/dune-project
index 874ac889d2378b673e657f86a0da41a0a59c60b1..e455736b22b6e7e1b7129d532ec861a17930799b 100644
--- a/src/plugins/constant_propagation/dune-project
+++ b/src/plugins/constant_propagation/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/dive/dune-project b/src/plugins/dive/dune-project
index 222120b30265a63e311a111f5e5d658ee7717549..0a45c5e58bba18590aa1c31aac005ddadca7a2f0 100644
--- a/src/plugins/dive/dune-project
+++ b/src/plugins/dive/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/e-acsl/dune-project b/src/plugins/e-acsl/dune-project
index ff6fc87f7ce11a88bdf8aaf7e2a1850c4512c6e4..0b479545c886aec70e2641247c72343264ed482a 100644
--- a/src/plugins/e-acsl/dune-project
+++ b/src/plugins/e-acsl/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of the Frama-C's E-ACSL plug-in. ;;
diff --git a/src/plugins/from/dune-project b/src/plugins/from/dune-project
index 0c2a0998893f740fb875bb5465efcd90823df8fe..4f636dba24bab4bb183a1195ea99fc23cc6f4490 100644
--- a/src/plugins/from/dune-project
+++ b/src/plugins/from/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/impact/dune-project b/src/plugins/impact/dune-project
index 8cde0454d8be5cdedef669b27b4eaffce756d8c6..3c590eff01801f722fdea3b386882e5c8b2924e0 100644
--- a/src/plugins/impact/dune-project
+++ b/src/plugins/impact/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/inout/dune-project b/src/plugins/inout/dune-project
index 3e4099fe3c8d2a19d708db3a80e3aec1a0e65d6c..f1e420b2977367d9680cb65fb4c61753b0ac4049 100644
--- a/src/plugins/inout/dune-project
+++ b/src/plugins/inout/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/instantiate/dune-project b/src/plugins/instantiate/dune-project
index 53c2c30c6ef2756e9369b0ac52a69b4559bc3689..21067e40127356e7414f2e693db558fa645cb0c8 100644
--- a/src/plugins/instantiate/dune-project
+++ b/src/plugins/instantiate/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/loop_analysis/dune-project b/src/plugins/loop_analysis/dune-project
index 5b2cde9de76f488f0fb8da759f3349920056d2e3..c7d0e2e99d61b1b5adfbf9a9d2dd5f741343e5f8 100644
--- a/src/plugins/loop_analysis/dune-project
+++ b/src/plugins/loop_analysis/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/markdown-report/dune-project b/src/plugins/markdown-report/dune-project
index 98b4a10aabdc0430efa57f0f63de3deaa9149852..2f95b35d7a3fffbca58549b1a31d884f3e10bcba 100644
--- a/src/plugins/markdown-report/dune-project
+++ b/src/plugins/markdown-report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/metrics/dune-project b/src/plugins/metrics/dune-project
index a0c509088c21d1d5c883d7cdac93ae994ac4c1e9..507ccd298ba0e12e7906bc998ef38d344c7c88ba 100644
--- a/src/plugins/metrics/dune-project
+++ b/src/plugins/metrics/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/nonterm/dune-project b/src/plugins/nonterm/dune-project
index cee289176ac86670db2066aab38c5eb07f69b100..a91cdce8beaa366f997c06157a79ccc10e464b9c 100644
--- a/src/plugins/nonterm/dune-project
+++ b/src/plugins/nonterm/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/obfuscator/dune-project b/src/plugins/obfuscator/dune-project
index b5af7a24e43ea372916f5eec62993e256e950310..c74dfe1f855719718015f2986c9b183ebe09c4d5 100644
--- a/src/plugins/obfuscator/dune-project
+++ b/src/plugins/obfuscator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/occurrence/dune-project b/src/plugins/occurrence/dune-project
index ea66e0e48be27b4e9384b9f5d46b895f5b5756a6..c4d46ce003e6e51858792b9f473077381506b0ac 100644
--- a/src/plugins/occurrence/dune-project
+++ b/src/plugins/occurrence/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/pdg/dune-project b/src/plugins/pdg/dune-project
index 1d13e366f656f5cac6d4e1179849b0c3b77f25ad..12ff9bf17de9a6ee74274b32b49f5fc6f4a1b7d2 100644
--- a/src/plugins/pdg/dune-project
+++ b/src/plugins/pdg/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/postdominators/dune-project b/src/plugins/postdominators/dune-project
index 269ba4e18cba9a1e48cf84f7b6ef99461f401ae2..db21480e1f5cffa508aabcf63e6c2c28be05ba01 100644
--- a/src/plugins/postdominators/dune-project
+++ b/src/plugins/postdominators/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/print_api/dune-project b/src/plugins/print_api/dune-project
index 75b5944a83a6a05215ca80168a07d34f889b8e13..f4887f33a78bd82e30ce3ed1c67d36a0ad3584e6 100644
--- a/src/plugins/print_api/dune-project
+++ b/src/plugins/print_api/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/qed/dune-project b/src/plugins/qed/dune-project
index db151b2fb0545c053eaec88989826467b64ec4f6..cc71f1946f8869a92c1a460d797f88b6d4e0c4e1 100644
--- a/src/plugins/qed/dune-project
+++ b/src/plugins/qed/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/reduc/dune-project b/src/plugins/reduc/dune-project
index e77db938c6df60b65e33c1a357f26fd9cb11a439..e9d7fc8b47138992aaad83218578bd65c7dc223c 100644
--- a/src/plugins/reduc/dune-project
+++ b/src/plugins/reduc/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/report/dune-project b/src/plugins/report/dune-project
index 2358c8daf8d46a33f77938ec0827539ac519df80..e58864153062c3c28c43d89445771e5481e80f77 100644
--- a/src/plugins/report/dune-project
+++ b/src/plugins/report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/rte/dune-project b/src/plugins/rte/dune-project
index 517150a660e00f264aa9cd69ec7f2972d85b57e9..8faf68e3c1d0a623682081a1d83c1c1a85879abb 100644
--- a/src/plugins/rte/dune-project
+++ b/src/plugins/rte/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/scope/dune-project b/src/plugins/scope/dune-project
index cbd34d3aa5114c3af36dd380f4f6142ee00a674f..b2f3282105ebdb366cdec8b2901b7fc23c76e7ae 100644
--- a/src/plugins/scope/dune-project
+++ b/src/plugins/scope/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/security_slicing/dune-project b/src/plugins/security_slicing/dune-project
index bbbfc8dda3bc773e60531f53292d5cd1a40e0063..153f462fbfbca972919cb52b318ad1e5027bbbf2 100644
--- a/src/plugins/security_slicing/dune-project
+++ b/src/plugins/security_slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/server/dune-project b/src/plugins/server/dune-project
index 3ab499b378067490ab2037dfd96e5a9df2f990fc..f9fc8ba242d6e1999f496ef5570b92e9bb62ba18 100644
--- a/src/plugins/server/dune-project
+++ b/src/plugins/server/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/slicing/dune-project b/src/plugins/slicing/dune-project
index 07b8be3ec010811cb28ee5a546d75925af68c25b..8f75251e779d289edc199385618c0eba0689d3e7 100644
--- a/src/plugins/slicing/dune-project
+++ b/src/plugins/slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/sparecode/dune-project b/src/plugins/sparecode/dune-project
index 9967b38940a329207d1c7689408c95cb65c390db..99f06f41fd6cf50c41b7afc9534a29c862e6da01 100644
--- a/src/plugins/sparecode/dune-project
+++ b/src/plugins/sparecode/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/studia/dune-project b/src/plugins/studia/dune-project
index e9862343663fd58dcacc9361068df3ffb05c1538..2eedff1444093bc8ff4f7c1571a531842fa3ecdb 100644
--- a/src/plugins/studia/dune-project
+++ b/src/plugins/studia/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/users/dune-project b/src/plugins/users/dune-project
index 248478937b36c65300155fedc54933cfa597d606..757332f51263519c8544aea6b3ebbb0325f0c329 100644
--- a/src/plugins/users/dune-project
+++ b/src/plugins/users/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/value/dune-project b/src/plugins/value/dune-project
index 64ad5aeb1eca481599f8350259027afc89702fc1..11c27712d8fea2942b649cb15f48c6a5991a913e 100644
--- a/src/plugins/value/dune-project
+++ b/src/plugins/value/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/variadic/dune-project b/src/plugins/variadic/dune-project
index 49aa75b87ea1410ce4d46d7268b15163973ebdea..9b6a2b3bd3ab4519ad3857454a0cf5640526bef7 100644
--- a/src/plugins/variadic/dune-project
+++ b/src/plugins/variadic/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/wp/dune-project b/src/plugins/wp/dune-project
index 5142a747c3fc9c61e4e7aaebb0a89acbe93a2701..68f619f079bada578f1480cb7495a4f4dfc45706 100644
--- a/src/plugins/wp/dune-project
+++ b/src/plugins/wp/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/tests/spec/preprocess_dos.c b/tests/spec/preprocess_dos.c
new file mode 100644
index 0000000000000000000000000000000000000000..fad1137e4f47452a05fd11c815e5e59b7c673ad9
--- /dev/null
+++ b/tests/spec/preprocess_dos.c
@@ -0,0 +1,13 @@
+/* run.config*
+DEPS: preprocess_dos.sh
+ENABLED_IF: %{bin-available:unix2dos}
+OPT: -cpp-command="./@PTEST_NAME@.sh unix2dos %i %o" -cpp-frama-c-compliant -print
+*/
+
+int main() {
+ int a = 0;
+ /*@
+ assert a == 0;
+ */
+ return a;
+}
diff --git a/tests/spec/preprocess_dos.c.in b/tests/spec/preprocess_dos.c.in
deleted file mode 100644
index abae8ad374b159cd60043731308ac57df1f96498..0000000000000000000000000000000000000000
--- a/tests/spec/preprocess_dos.c.in
+++ /dev/null
@@ -1,13 +0,0 @@
-/* run.config*
-COMMENT: Don't edit directly preprocess_dos.c, but preprocess_dos.c.in
-@DONTRUN@
-OPT: -cpp-command="@PTEST_DIR@/@PTEST_NAME@.sh @UNIX2DOS@ %i %o" -cpp-frama-c-compliant -print
-*/
-
-int main() {
- int a = 0;
- /*@
- assert a == 0;
- */
- return a;
-}