[wp] Avoid name clashes in Mchunk

src/plugins/wp/MemTyped.ml

@@ -157,6 +157,9 @@ struct
   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
+    | M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
+    | m -> Format.pp_print_string fmt (name m)
   let val_of_chunk = function
     | M_int _ | M_char -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -1098,7 +1101,7 @@ and lookup_f f es =
 
 and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
 
-let mchunk c = Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c)
+let mchunk c = Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c)
 
 let lookup s e =
   try mchunk (Tmap.find e s)

src/plugins/wp/tests/wp_tip/chunk_printing.i

+/* run.config
+   OPT: -wp-rte -wp-msg-key state
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+struct V {
+	int* a ;
+	unsigned* b ;
+};
+
+struct V* y ;
+
+/*@
+	assigns \nothing;
+	ensures \result == v->a || \result == y->a;
+*/
+int* get_int(struct V* v);
+
+/*@
+	assigns \nothing;
+	ensures \result == v->b || \result == y->b;
+*/
+unsigned* get_uint(struct V* v);
+
+int main(void){
+	struct V x ;
+	x.a = get_int(&x);
+	x.b = get_uint(&x);
+
+	//@ assert *(x.a) == *(x.b);
+}

src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle

+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_tip/chunk_printing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function main
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_tip/chunk_printing.i, line 32):
+Let x_1 = « *`v_1 »@L1.
+Let x_2 = « *`v »@L1.
+Assume {
+  Type: is_sint32_chunk(µ:Msint32@L1) /\ is_uint32_chunk(µ:Muint32@L1) /\
+      is_uint32(`x_1) /\ is_sint32(`x_2).
+  (* Heap *)
+  Type: framed(µ:Mptr@L1).
+  Stmt { L1:  }
+  Stmt { x.a = `v;  }
+  (* Call 'get_int' *)
+  Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
+  Stmt { x.b = `v_1;  }
+  (* Call 'get_uint' *)
+  Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
+}
+Prove: `x_2 = `x_1.
+
+------------------------------------------------------------