print return value of call_intrinsic

rems-project · Aug 29, 2023 · f8b81ba · f8b81ba
1 parent 0b367a1
commit f8b81ba
Showing 1 changed file with 9 additions and 0 deletions.
diff --git 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)