From 4e1807e75d34204b1812700b3d36f15975d82a8c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 23 Feb 2021 17:21:23 +0100
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)
---
src/plugins/wp/MemoryContext.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 696574f8000..c3d5d846d72 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -29,9 +29,9 @@ type param =
| NotUsed | ByAddr | ByValue | ByShift | ByRef
| InContext of validity | InArray of validity
-let nullable_string = function
- | Valid -> ""
- | Nullable -> "(nullable)"
+let pp_nullable fmt = function
+ | Valid -> ()
+ | Nullable -> Format.pp_print_string fmt " (nullable)"
let pp_param fmt = function
| NotUsed -> Format.pp_print_string fmt "not used"
@@ -39,8 +39,8 @@ let pp_param fmt = function
| ByValue -> Format.pp_print_string fmt "by value"
| ByShift -> Format.pp_print_string fmt "by value with shift"
| ByRef -> Format.pp_print_string fmt "by ref"
- | InContext n -> Format.pp_print_string fmt ("in context" ^ nullable_string n)
- | InArray n -> Format.pp_print_string fmt ("in array" ^ nullable_string n)
+ | InContext n -> Format.fprintf fmt "in context%a" pp_nullable n
+ | InArray n -> Format.fprintf fmt "in array%a" pp_nullable n
(* -------------------------------------------------------------------------- *)
(* --- Separation Hypotheses --- *)
--
GitLab