diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 08a207993..5c8ff8249 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -825,7 +825,7 @@ let jump_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list = type code = Llair.inst list * Llair.term * Llair.block list let pp_code fs (insts, term, blocks) = - Format.fprintf fs "@[@[%a%t@]%t@[%a@]@]" + Format.fprintf fs "@[@,@[%a%t@]%t@[%a@]@]" (List.pp "@ " Llair.Inst.pp) insts (fun fs -> @@ -1048,8 +1048,8 @@ let xlate_instr : | _ -> false in let return, blocks = + let args = trampoline_args x instr return_blk in if not (need_return_trampoline instr return_blk) then - let args = trampoline_args x instr return_blk in (Llair.Jump.mk return_dst args, []) else let lbl = name ^ ".ret" in diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 60795597f..113f66bd2 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -248,7 +248,7 @@ module Jump = struct let pp = pp_jump let invariant ?(accept_return = false) jmp = - Invariant.invariant [%here] jmp [%sexp_of: t] + Invariant.invariant [%here] (jmp, accept_return) [%sexp_of: t * bool] @@ fun () -> let {dst= {params; parent}; args} = jmp in if parent == dummy_func then