From 9b0c81b7520d5b9fc3cebd2e928625905939d606 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Mar 2024 17:13:27 +0100
Subject: [PATCH] [wp] fix extension usage
---
src/libraries/utils/filepath.ml | 1 +
src/libraries/utils/filepath.mli | 15 +++++++++++----
src/plugins/wp/ProverWhy3.ml | 5 +++--
3 files changed, 15 insertions(+), 6 deletions(-)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 959969454f5..4998c5f9d50 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -277,6 +277,7 @@ module Normalized = struct
type t = string
let of_string ?existence ?base_name s = normalize ?existence ?base_name s
+ let extend ?existence t ext = normalize ?existence (t ^ ext)
let concat ?existence t s = normalize ?existence (t ^ "/" ^ s)
let concats ?existence t sl =
let s' = List.fold_left (fun acc s -> acc ^ "/" ^ s) "" sl in
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index cdcaac29a44..cb514384a96 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -74,6 +74,14 @@ module Normalized: sig
*)
val of_string: ?existence:existence -> ?base_name:string -> string -> t
+ (** [extend ~existence file ext] returns the normalized path to the file
+ [file] ^ [ext]. Note that it does not introduce a dot.
+ The resulting path must respect [existence].
+
+ @since Frama-C+dev
+ *)
+ val extend: ?existence:existence -> t -> string -> t
+
(** [concat ~existence dir file] returns the normalized path
resulting from the concatenation of [dir] ^ "/" ^ [file].
The resulting path must respect [existence].
@@ -82,11 +90,10 @@ module Normalized: sig
*)
val concat: ?existence:existence -> t -> string -> t
- (**
- [concats ~existence dir paths] concatenates a list of paths, as per
- the [concat] function.
+ (** [concats ~existence dir paths] concatenates a list of paths, as per
+ the [concat] function.
- @since 28.0-Nickel
+ @since 28.0-Nickel
*)
val concats: ?existence:existence -> t -> string list -> t
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 62935c0fd4e..46700b024bb 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1413,10 +1413,11 @@ let editor_command pconf =
let scriptfile ~force ~ext wpo =
let dir = Wp_parameters.get_session_dir ~force "interactive" in
- Filepath.Normalized.concat dir (wpo.Wpo.po_sid ^ ext)
+ let filenoext = Filepath.Normalized.concat dir wpo.Wpo.po_sid in
+ Filepath.Normalized.extend filenoext ext
let updatescript ~script driver task =
- let backup = Filepath.Normalized.concat script ".bak" in
+ let backup = Filepath.Normalized.extend script ".bak" in
Filepath.rename script backup ;
let old = open_in (backup :> string) in
Command.pp_to_file script
--
GitLab