Merge branch 'feature/andre/safe-filepath' into 'master'

synchronize with frama-c/frama-c!1936

See merge request frama-c/e-acsl!231

src/plugins/e-acsl/main.ml

@@ -64,7 +64,7 @@ let unmemoized_extend_ast () =
     let register s =
       File.pre_register
         (File.NeedCPP
-           (s,
+           (Datatype.Filepath.of_string s,
             ppc
             ^ Format.asprintf " -I%s" share,
             ppk))

src/plugins/e-acsl/misc.ml

@@ -35,10 +35,10 @@ let library_files () =
       "e_acsl.h" ]
 
 let normalized_library_files =
-  lazy (List.map Filepath.normalize (library_files ()))
+  lazy (List.map Datatype.Filepath.of_string (library_files ()))
 
 let is_library_loc (loc, _) =
-  List.mem loc.Lexing.pos_fname (Lazy.force normalized_library_files)
+  List.mem loc.Filepath.pos_path (Lazy.force normalized_library_files)
 
 let library_functions = Datatype.String.Hashtbl.create 17
 let register_library_function vi =
@@ -111,7 +111,7 @@ let mk_e_acsl_guard ?(reverse=false) kind kf e p =
     Kernel.Unicode.without_unicode
       (Format.asprintf "%a@?" Printer.pp_predicate) p
   in
-  let line = (fst loc).Lexing.pos_lnum in
+  let line = (fst loc).Filepath.pos_lnum in
   let e =
     if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
   in

src/plugins/e-acsl/tests/print.ml

@@ -27,9 +27,9 @@ module Printer_extension(X:Printer.PrinterClass) = struct
 
     method! global fmt g =
       let loc, _ = Cil_datatype.Global.loc g in
-      let file = loc.Lexing.pos_fname in
-      if file = "" || List.exists
-        (fun s -> Filepath.normalize s = file)
+      let file = loc.Filepath.pos_path in
+      if file = Datatype.Filepath.dummy || List.exists
+        (fun s -> Datatype.Filepath.of_string s = file)
         (Kernel.Files.get ())
       then super#global fmt g