From e185f6452dc47f38ad9cffebbc024fe7dd37c8ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 28 Sep 2020 15:34:21 +0200
Subject: [PATCH] Add directly ptests_config since there is no generated values
Except for numerors but the tests should be activated only when the modules
used in it are available
---
.gitignore | 1 -
ptests/ptests.ml | 37 ++++++-------------------------------
tests/ptests_config | 1 +
3 files changed, 7 insertions(+), 32 deletions(-)
create mode 100644 tests/ptests_config
diff --git a/.gitignore b/.gitignore
index 7af9b4730c1..f70695811c0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -40,7 +40,6 @@ autom4te.cache
#tests
-/tests/ptests_config
/tests/**/result/
/tests/**/result_*/
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index a390bf7f52c..bdb5f3f9c6b 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -217,22 +217,6 @@ let make_test_suite s =
(* Those variables are read from a ptests_config file *)
let default_suites = ref []
-let toplevel_path = ref ""
-
-let change_toplevel_to_gui () =
- let s = !toplevel_path in
- match string_del_suffix "toplevel.opt" s with
- | Some s -> toplevel_path := s ^ "viewer.opt"
- | None ->
- match string_del_suffix "toplevel.byte" s with
- | Some s -> toplevel_path := s ^ "viewer.byte"
- | None ->
- match string_del_suffix "frama-c" s with
- | Some s -> toplevel_path := s ^ "frama-c-gui"
- | None ->
- match string_del_suffix "frama-c.byte" s with
- | Some s -> toplevel_path := s ^ "frama-c-gui.byte"
- | None -> ()
let () =
@@ -389,8 +373,6 @@ let parse_config_line =
| "DEFAULT_SUITES" ->
let l = Str.split regexp_blank value in
default_suites := List.map (Filename.concat test_path) l
- | "TOPLEVEL_PATH" ->
- toplevel_path := value
| _ -> default_env key value (* Environnement variable that Frama-C reads*)
@@ -414,11 +396,7 @@ let () =
end
done
with
- | End_of_file ->
- if !toplevel_path = "" then begin
- Format.eprintf "Missing TOPLEVEL_PATH variable. Aborting.@.";
- exit 1
- end
+ | End_of_file -> ()
end
else begin
Format.eprintf
@@ -426,9 +404,6 @@ let () =
exit 1
end
-(** Must be done after reading config *)
-let () = if !behavior = Gui then change_toplevel_to_gui ()
-
(* redefine name if special configuration expected *)
let redefine_name name =
if !special_config = "" then name else
@@ -595,7 +570,7 @@ type config =
let default_macros () =
let l = [
- "frama-c", !toplevel_path;
+ "frama-c", "frama-c";
] in
Macros.add_list l Macros.empty
@@ -607,8 +582,8 @@ let default_config () =
dc_deps = [];
dc_plugins = [];
dc_filter = None ;
- dc_default_toplevel = !toplevel_path;
- dc_toplevels = [ !toplevel_path, default_options, [], Macros.empty, "" ];
+ dc_default_toplevel = "frama-c";
+ dc_toplevels = [ "frama-c", default_options, [], Macros.empty, "" ];
dc_dont_run = false;
dc_framac = true;
dc_default_log = [];
@@ -649,10 +624,10 @@ let scan_execnow ~once dir ex_timeout (s:string) =
}
(* the default toplevel for the current level of options. *)
-let current_default_toplevel = ref !toplevel_path
+let current_default_toplevel = ref "frama-c"
let current_default_log = ref []
let current_default_cmds =
- ref [!toplevel_path,default_options,[], Macros.empty, ""]
+ ref ["frama-c",default_options,[], Macros.empty, ""]
let make_custom_opts =
let space = Str.regexp " " in
diff --git a/tests/ptests_config b/tests/ptests_config
new file mode 100644
index 00000000000..8f123e46456
--- /dev/null
+++ b/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= dynamic dynamic_plugin journal saveload spec misc syntax cil pretty_printing builtins libc value fc_script jcdb metrics callgraph value/traces occurrence rte rte_manual idct test float constant_propagation impact pdg scope sparecode slicing
--
GitLab