Merge branch 'fix/andre/load-module-with-space' into 'master'

[Kernel] fix -load-module/-load-script with filenames containing spaces

Closes #823

See merge request frama-c/frama-c!2570

.Makefile.lint

@@ -102,8 +102,6 @@ ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.mli
 ML_LINT_KO+=src/kernel_services/parsetree/logic_ptree.mli
 ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.ml
 ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/dynamic.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/dynamic.mli
 ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.ml
 ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.mli
 ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml

Makefile.generating

@@ -47,8 +47,9 @@ MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION)
 $(CONFIG_FILE): $(CONFIG_FILE).in VERSION VERSION_CODENAME share/Makefile.config Makefile.generating configure.in
 	$(SED) \
 	  -e "s|@VERSION@|$(VERSION)|" \
-         -e "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" \
+          -e "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" \
           -e "s|@CURR_DATE@|$$(LC_ALL=C date)|" \
+          -e "s|@LABLGTK@|$(LABLGTK)|" \
 	  -e "s|@OCAMLC@|$(OCAMLC)|" \
           -e "s|@OCAMLOPT@|$(OCAMLOPT)|" \
 	  -e "s|@WARNINGS@|$(WARNINGS)|" \

src/kernel_internals/runtime/fc_config.ml.in

@@ -32,6 +32,8 @@ let minor_version = @MINOR_VERSION@
 
 let is_gui = ref false
 
+let lablgtk = "@LABLGTK@"
+
 let ocamlc = "@OCAMLC@"
 let ocamlopt = "@OCAMLOPT@"
 let ocaml_wflags = "@WARNINGS@"

src/kernel_internals/runtime/fc_config.mli

@@ -46,6 +46,10 @@ val is_gui: bool ref
 (** Is the Frama-C GUI running?
     @since Beryllium-20090601-beta1 *)
 
+val lablgtk: string
+(** Name of the lablgtk version against which Frama-C has been compiled.
+    blank if only command-line mode is available. *)
+
 val ocamlc: string
 (** Name of the bytecode compiler.
     @since Boron-20100401 *)

src/kernel_services/plugin_entry_points/dynamic.ml

@@ -55,24 +55,24 @@ exception Unbound_value = Tbl.Unbound_value
 
 let dynlib_error name = function
   | Dynlink.Error e ->
-      error ~name ~message:"cannot load module" ~details:(Dynlink.error_message e) ;
+    error ~name ~message:"cannot load module" ~details:(Dynlink.error_message e) ;
   | Sys_error _ as e ->
-      error ~name ~message:"system error" ~details:(Printexc.to_string e)
+    error ~name ~message:"system error" ~details:(Printexc.to_string e)
   | Unloadable details ->
-      error ~name ~message:"incompatible with current set-up" ~details
+    error ~name ~message:"incompatible with current set-up" ~details
   (* the three next errors may be raised in case of incompatibilities with
      another plug-in *)
   | Incompatible_type s ->
-      error ~name ~message:"code incompatibility" ~details:s
+    error ~name ~message:"code incompatibility" ~details:s
   | Unbound_value s ->
-      error ~name ~message:"code incompatibility" ~details:("unbound value " ^ s)
+    error ~name ~message:"code incompatibility" ~details:("unbound value " ^ s)
   | Type.No_abstract_type s ->
-      error ~name ~message:"code incompatibility" ~details:("unbound abstract type " ^ s)
+    error ~name ~message:"code incompatibility" ~details:("unbound abstract type " ^ s)
   | Log.AbortError _ | Log.AbortFatal _ | Log.FeatureRequest _ as e ->
-      raise e
+    raise e
   | e ->
-      error ~name ~message:("unexpected exception: " ^ Printexc.to_string e)
-        ~details:(Printexc.get_backtrace ())
+    error ~name ~message:("unexpected exception: " ^ Printexc.to_string e)
+      ~details:(Printexc.get_backtrace ())
 
 let dynlib_module name file =
   Klog.feedback ~dkey "Loading module '%s' from '%s'." name file ;
@@ -241,13 +241,15 @@ let load_script base =
   let fmt = Format.formatter_of_buffer cmd in
   begin
     if Dynlink.is_native then
-      Format.fprintf fmt "%s -shared -o %s.cmxs" Fc_config.ocamlopt base
+      Format.fprintf fmt "%s -shared -o %S.cmxs" Fc_config.ocamlopt base
     else
       Format.fprintf fmt "%s -c" Fc_config.ocamlc ;
-    Format.fprintf fmt " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
-    if !Fc_config.is_gui then Format.pp_print_string fmt " -package lablgtk2" ;
+    Format.fprintf fmt
+      " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
+    if !Fc_config.is_gui && Fc_config.lablgtk <> "" then
+      Format.fprintf fmt " -package %s" Fc_config.lablgtk;
     List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
-    Format.fprintf fmt " %s.ml" base ;
+    Format.fprintf fmt " %S.ml" base ;
     Format.pp_print_flush fmt () ;
     let cmd = Buffer.contents cmd in
     Klog.feedback ~dkey "running '%s'" cmd ;
@@ -321,31 +323,31 @@ let load_module m =
   let base,ext = split_ext m in
   match ext with
   | ".ml" ->
-      begin
-        (* force script compilation *)
+    begin
+      (* force script compilation *)
+      match is_file base ".ml" with
+      | 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
+      | Some file -> dynlib_module (Filename.basename base) file
+      | None ->
         match is_file base ".ml" with
         | 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
-        | Some file -> dynlib_module (Filename.basename base) file
         | None ->
-            match is_file base ".ml" with
-            | Some _ -> load_script base
-            | None ->
-                if is_package m && mem_package m then load_packages [m]
-                else
-                  let fc =
-                    "frama-c-" ^ String.lowercase_ascii m
-                  in
-                  if mem_package fc then load_packages [fc]
-                  else Klog.error "package or module '%s' not found" m
-      end
+          if is_package m && mem_package m then load_packages [m]
+          else
+            let fc =
+              "frama-c-" ^ String.lowercase_ascii m
+            in
+            if mem_package fc then load_packages [fc]
+            else Klog.error "package or module '%s' not found" m
+    end
   | _ ->
-      Klog.error "don't know what to do with '%s' (unexpected %s)" m ext
+    Klog.error "don't know what to do with '%s' (unexpected %s)" m ext
 
 (* ************************************************************************* *)
 (** {2 Registering and accessing dynamic values} *)

src/kernel_services/plugin_entry_points/dynamic.mli

@@ -28,8 +28,8 @@
 (* ************************************************************************* *)
 
 val register:
-  ?comment:string -> 
-  plugin:string -> 
+  ?comment:string ->
+  plugin:string ->
   string -> 'a Type.t -> journalize:bool -> 'a -> 'a
 (** [register ~plugin name ty v] registers [v] with the name
     [name], the type [ty] and the plug-in [plugin].
@@ -71,7 +71,7 @@ val iter_comment : (string -> string -> unit) -> unit
 (* ************************************************************************* *)
 
 (** Module to use for accessing parameters of plug-ins.
-    Assume that the plug-in is already loaded. 
+    Assume that the plug-in is already loaded.
     @plugin development guide *)
 module Parameter : sig
 
@@ -99,7 +99,7 @@ module Parameter : sig
   (** Not for casual users *)
   (**/**)
 
-  (** Boolean parameters. 
+  (** Boolean parameters.
       @plugin development guide *)
   module Bool: sig
     include Common with type t = bool

tests/misc/oracle/with-space.res.oracle

+[kernel] Parsing tests/misc/with-space.i (no preprocessing)
+[kernel] module successfully loaded

tests/misc/with space/module.ml

+let () = Db.Main.extend (fun () ->
+    Kernel.feedback "module successfully loaded"
+  )

tests/misc/with-space.i

+/* run.config
+   OPT: -load-module @PTEST_DIR@/with\ space/module.ml
+ */