From 274827ccda287a1bd4eb84397d4316ed9922b45f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 23 Nov 2021 11:51:24 +0100
Subject: [PATCH] [kernel] Usable_emitter.get returns [orphan] when the emitter
does not exists.
Instead of raising a [Not_found] exception.
Fixes crashes when loading a Frama-C save when an original emitter is not
available.
---
src/kernel_services/ast_data/annotations.ml | 9 +--------
src/kernel_services/plugin_entry_points/emitter.ml | 9 ++++++++-
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 8869fe97088..56739c79dd7 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -365,14 +365,7 @@ let code_annot_emitter ?filter stmt =
try
let tbl = Code_annots.find stmt in
let filter e l acc =
- let e =
- try Emitter.Usable_emitter.get e
- with Not_found ->
- (* in some cases, e.g. when loading a state with a different set
- of plugins loaded, the original emitter might not be available,
- leading to discarding annotations. Let the kernel adopt them. *)
- Emitter.orphan
- in
+ let e = Emitter.Usable_emitter.get e in
match filter with
| None -> List.map (fun a -> a, e) l @ acc
| Some f ->
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 7d53caca822..9f5ada97cc5 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -155,7 +155,7 @@ module Usable_emitter = struct
let mem_project = Datatype.never_any_project
end)
- let get e =
+ let unsafe_get e =
let get_params map =
Datatype.String.Map.fold
(fun s _ acc -> Typed_parameter.get s :: acc)
@@ -167,6 +167,13 @@ module Usable_emitter = struct
correctness_parameters = get_params e.correctness_values;
tuning_parameters = get_params e.tuning_values }
+ (* In some cases, e.g. when loading a state with a different set
+ of plugins loaded, the original emitter might not be available,
+ leading to discarding annotations. Let the kernel adopt them. *)
+ let get e =
+ try unsafe_get e
+ with Not_found -> orphan
+
let get_name e = e.u_name
let get_unique_name e = Format.asprintf "%a" pretty e
--
GitLab