From 3dcd4ce3be780b81568bf62b8bcadfa49c40614d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 15 Mar 2022 15:28:36 +0100
Subject: [PATCH] [wp] detailed chunk printer
---
src/plugins/wp/MemLoader.ml | 4 ++--
src/plugins/wp/MemTyped.ml | 11 +++++------
2 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 61a8efc1d40..9587d9eac5d 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -149,8 +149,8 @@ struct
[ (Trigger.of_term value1 :: triggers );
(Trigger.of_term value2 :: triggers ) ]
in
- let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
- prefix name Chunk.pretty chunk i in
+ let l_name = Pretty_utils.sfprintf "%s_%s_%s%d"
+ prefix name (Chunk.basename_of_chunk chunk) i in
let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
Definitions.define_lemma {
l_kind = Admit ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 50a414265a5..aaead6141ed 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -147,7 +147,7 @@ struct
| T_alloc -> 12
| T_init -> 13
let hash = rank
- let name = function
+ let basename = function
| M_int i when Ctypes.is_char i -> "Mchar"
| M_int _ -> "Mint"
| M_f32 -> "Mf32"
@@ -157,10 +157,9 @@ struct
| T_init -> "Init"
let compare a b = rank a - rank b
let equal = (=)
- let pretty fmt c = Format.pp_print_string fmt (name c)
- let detailed_pretty fmt = function
+ let pretty fmt = function
| M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
- | m -> Format.pp_print_string fmt (name m)
+ | m -> Format.pp_print_string fmt (basename m)
let val_of_chunk = function
| M_int _ -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -175,7 +174,7 @@ struct
| M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
| T_alloc -> t_malloc
| T_init -> t_init
- let basename_of_chunk = name
+ let basename_of_chunk = basename
let is_framed _ = false
end
@@ -1213,7 +1212,7 @@ and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
let mchunk c =
match c with
| T_init -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KInit)
- | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c, KValue)
+ | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
let lookup s e =
try mchunk (Tmap.find e s)
--
GitLab