diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 864a56737..340795f80 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -75,12 +75,12 @@ let exec_inst inst pre = let areturn = Option.map ~f:X.reg reg in let intrinsic = Llair.Intrinsic.to_string name in let actuals = IArray.map ~f:X.term args in - Exec.intrinsic ~skip_throw:true pre areturn intrinsic actuals + Exec.intrinsic_func ~skip_throw:true pre areturn intrinsic actuals |> Option.get_lazy (fail "exec_inst: %a" Llair.Inst.pp inst) ) |> Option.map ~f:simplify let exec_intrinsic ~skip_throw r i es q = - Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) + Exec.intrinsic_func ~skip_throw q (Option.map ~f:X.reg r) (Llair.Function.name i) (IArray.map ~f:X.term es) |> Option.map ~f:(Option.map ~f:simplify) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index f85f260e6..28e486af0 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -737,7 +737,7 @@ let free pre ~ptr = exec_spec pre (free_spec ptr) let nondet pre = function Some reg -> kill pre reg | None -> pre let abort _ = None -let intrinsic ~skip_throw : +let intrinsic_func ~skip_throw : Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option = fun pre areturn intrinsic actuals -> let name = diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli index 7dc2258fa..ec3e15dd9 100644 --- a/sledge/src/exec.mli +++ b/sledge/src/exec.mli @@ -22,7 +22,7 @@ val free : Sh.t -> ptr:Term.t -> Sh.t option val nondet : Sh.t -> Var.t option -> Sh.t val abort : Sh.t -> Sh.t option -val intrinsic : +val intrinsic_func : skip_throw:bool -> Sh.t -> Var.t option