From df80027b129cb5d96d42db0ec3401213d2cd9610 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 16 Feb 2023 17:34:21 +0100
Subject: [PATCH] Handle exception of find_by_name when building a destructor
call.
---
src/kernel_services/analysis/destructors.ml | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml
index bb96f993598..47f549d68de 100644
--- a/src/kernel_services/analysis/destructors.ml
+++ b/src/kernel_services/analysis/destructors.ml
@@ -28,7 +28,11 @@ let add_destructor (_, l as acc) var =
| [] -> acc
| [ attr ] ->
let mk_call f e args =
- let kf = Globals.Functions.find_by_name f in
+ let kf =
+ try Globals.Functions.find_by_name f
+ with Not_found ->
+ Kernel.fatal "Destructor function %s does not exist" f
+ in
let e =
match Globals.Functions.get_params kf with
| vi :: _ ->
--
GitLab