From 0a27ac2e455348a6a272a07091b2651c2ab96607 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 25 Mar 2021 16:28:30 +0100
Subject: [PATCH] [wp] catch dimension errors

---
 src/plugins/wp/Makefile.in | 5 +++--
 src/plugins/wp/ctypes.ml   | 9 +++++++--
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index d78ac2bd273..ffba8070d60 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -61,9 +61,10 @@ PLUGIN_NAME:=Wp
 PLUGIN_CMO:= \
 	rformat wprop \
 	wp_parameters wp_error \
-	dyncall ctypes clabels \
 	Why3Provers \
-	Context Warning AssignsCompleteness MemoryContext wpContext \
+	Context Warning \
+	dyncall ctypes clabels \
+	AssignsCompleteness MemoryContext wpContext \
 	LogicUsage RefUsage \
 	Layout Region \
 	RegionAnnot RegionAccess RegionDump RegionAnalysis \
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 542d8e41396..374fda3f939 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -237,8 +237,13 @@ let char c = Integer.to_int64 (Cil.charConstToInt c)
 
 let constant e =
   match (Cil.constFold true e).enode with
-  | Const(CInt64(k,_,_)) -> Integer.to_int64 k
-  | _ -> WpLog.fatal "Non-constant expression (%a)" Printer.pp_exp e
+  | Const(CInt64(k,_,_)) ->
+      begin
+        try Integer.to_int64 k
+        with Z.Overflow ->
+          Warning.error "Array size too large (%a)" (Integer.pretty ~hexa:true) k
+      end
+  | _ -> Warning.error "Non-constant expression (%a)" Printer.pp_exp e
 
 let get_int e =
   match (Cil.constFold true e).enode with
-- 
GitLab