From 848c5f4070c79e913caf1d55cab54c06c2ffe788 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 7 Apr 2020 11:06:29 +0200
Subject: [PATCH] [eva] better exception handling in Db.Value
---
src/kernel_services/plugin_entry_points/db.ml | 16 ++++++++++++++--
1 file changed, 14 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 9d0a42e6ebd..f602bf07dcb 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -526,8 +526,20 @@ module Value = struct
let add_formals_to_state = mk_fun "add_formals_to_state"
+ let get_fundec_from_stmt stmt =
+ let kf =
+ try
+ Kernel_function.find_englobing_kf stmt
+ with Not_found ->
+ Kernel.fatal "Unknown statement '%a'" Printer.pp_stmt stmt
+ in
+ try
+ Kernel_function.get_definition kf
+ with Kernel_function.No_Definition ->
+ Kernel.fatal "No definition for function %a" Kernel_function.pretty kf
+
let noassert_get_stmt_state ~after s =
- if !no_results (Kernel_function.(get_definition (find_englobing_kf s)))
+ if !no_results (get_fundec_from_stmt s)
then Cvalue.Model.top
else
let (find, add), find_by_callstack =
@@ -586,7 +598,7 @@ module Value = struct
exception Is_reachable
let is_reachable_stmt stmt =
- if !no_results (Kernel_function.(get_definition (find_englobing_kf stmt)))
+ if !no_results (get_fundec_from_stmt stmt)
then true
else
let ho = try Some (Table_By_Callstack.find stmt) with Not_found -> None in
--
GitLab