From e461aef502d80f3ff9c14e38aac060d9f661f7bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 22 Apr 2026 19:42:12 +0100 Subject: [PATCH] add error messages on some call failures When using call with invariant on procedures whose argument or return types do not match, we raised an exception without catching it. This adds an error message. --- src/phl/ecPhlCall.ml | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 6191c7300..7c6a84353 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -500,12 +500,25 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr = let defl = EcEnv.Fun.by_xpath fl env in let defr = EcEnv.Fun.by_xpath fr env in let sigl, sigr = defl.f_sig, defr.f_sig in - let testty = - EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg - && EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret + + let error s tl tr = + let ppe = EcPrinting.PPEnv.ofenv env in + tc_error _pf "@[The procedures do not have the same %s types:@]@;<2 2>\ + @[Left side: @[%a@]@,\ + Right side: @[%a@]@]@;<2 0>\ + A full contract cannot be inferred; consider providing a full contract using@;<2 2>\ + call (: ...==> ...)@," + s + (EcPrinting.pp_type ppe) tl + (EcPrinting.pp_type ppe) tr in - if not testty then raise EqObsInError; + if not (EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg) + then error "argument" sigl.fs_arg sigr.fs_arg; + + if not (EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret) + then error "return" sigl.fs_ret sigr.fs_ret; + let eq_params = ts_inv_eqparams sigl.fs_arg sigl.fs_anames ml