From 8269bc7456a23784730a01a3cb5b6abf29462efa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Jun 2020 10:17:23 +0200
Subject: [PATCH] [Wp] Fixes a crash in the GUI.
---
src/plugins/wp/GuiNavigator.ml | 30 +++++++++++++++++-------------
1 file changed, 17 insertions(+), 13 deletions(-)
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 9c55dc735e2..74669b99420 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -407,19 +407,23 @@ let model_varinfo :
| PLval(Some kf, _ , (Var x,NoOffset))
| PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset))
when button=1 ->
- let init = WpStrategy.is_main_init kf in
- let acc = RefUsage.get ~kf ~init x in
- let model = match acc with
- | RefUsage.NoAccess -> "any"
- | RefUsage.ByValue -> "'var'"
- | RefUsage.ByRef -> "'ref'"
- | RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype
- -> "'caveat'"
- | _ -> "'typed'"
- in
- main#pretty_information
- "Is is accessed as %t and fits in %s wp-model@."
- (RefUsage.print x acc) model ;
+ begin
+ try
+ let init = WpStrategy.is_main_init kf in
+ let acc = RefUsage.get ~kf ~init x in
+ let model = match acc with
+ | RefUsage.NoAccess -> "any"
+ | RefUsage.ByValue -> "'var'"
+ | RefUsage.ByRef -> "'ref'"
+ | RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype
+ -> "'caveat'"
+ | _ -> "'typed'"
+ in
+ main#pretty_information
+ "Is is accessed as %t and fits in %s wp-model@."
+ (RefUsage.print x acc) model ;
+ with _ -> ()
+ end
| _ -> ()
(* -------------------------------------------------------------------------- *)
--
GitLab