From 4f07a48bed8a09ca550df9679910559557e86398 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 7 Apr 2021 13:46:12 +0200
Subject: [PATCH] [Kernel] avoid crash in unroll pragma with large integer
---
src/kernel_internals/typing/unroll_loops.ml | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index c60b1bb3b5a..e09cbae6a55 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -51,7 +51,14 @@ let update_info global_find_init emitter info spec =
in
let i = Logic_utils.constFoldTermToInt t in
match i with
- | Some i -> { info with unroll_number = Some (Integer.to_int i) }
+ | Some i ->
+ begin
+ match Integer.to_int_opt i with
+ | Some _ as unroll_number -> { info with unroll_number }
+ | None -> Kernel.abort ~current:true
+ "count too large in unrolling directive: %a"
+ (Integer.pretty ~hexa:false) i
+ end
| None ->
Kernel.warning ~once:true ~current:true
"ignoring unrolling directive (not an understood constant \
--
GitLab