From f8b81bac0f412dd3e3207b8b4c7e50d051ea9de0 Mon Sep 17 00:00:00 2001 From: Vadim Zaliva Date: Tue, 29 Aug 2023 16:15:05 -0700 Subject: [PATCH] print return value of call_intrinsic --- memory/cheri-coq/impl_mem.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/memory/cheri-coq/impl_mem.ml b/memory/cheri-coq/impl_mem.ml index 5db7a93c1..2204a4c0b 100644 --- a/memory/cheri-coq/impl_mem.ml +++ b/memory/cheri-coq/impl_mem.ml @@ -1410,6 +1410,15 @@ module CHERIMorello : Memory = struct (toCoq_location loc) name args) + >>= + (fun res -> + Cerb_debug.print_debug 4 [] + (fun () -> + match res with + | Some mval -> "MEMOP_RET call_intrinsic = Just " ^ Pp_utils.to_plain_string (pp_mem_value mval) + | None -> "MEMOP_RET call_intrinsic = None" + ); + return res) let get_intrinsic_type_spec name = Option.map fromCoq_intrinsics_signature (MM.get_intrinsic_type_spec name)