From dd2cdf56fda29fb625272ae9e9ff5ba0e4d16fe1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 22 Aug 2018 10:24:42 +0200
Subject: [PATCH] synchronize with frama-c/frama-c!1936
---
src/plugins/e-acsl/main.ml | 2 +-
src/plugins/e-acsl/misc.ml | 6 +++---
src/plugins/e-acsl/tests/print.ml | 6 +++---
3 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index e1d7ac2aa2d..07328232f11 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/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))
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index c8fa6a0e325..8abbd4ab81d 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/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
diff --git a/src/plugins/e-acsl/tests/print.ml b/src/plugins/e-acsl/tests/print.ml
index 1eaf835068c..66946052058 100644
--- a/src/plugins/e-acsl/tests/print.ml
+++ b/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
--
GitLab