From 1f68974108c4a511bc49c9467d93d135258a01bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 13 Oct 2021 10:20:28 +0200
Subject: [PATCH] [kernel] Minor simplification and comment in cabs2cil.
---
src/kernel_internals/typing/cabs2cil.ml | 14 ++++++--------
1 file changed, 6 insertions(+), 8 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3f31de7afad..13bf2fc6abd 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8548,11 +8548,11 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
if first < 0 || first > last then
Kernel.error ~once:true ~current:true
"start index larger than end index in range initializer";
+ (* Arbitrary limit to avoid building an impractical AST. *)
+ if last - first > 100_000 then
+ Kernel.fatal ~current:true "INDEX_RANGE too large";
let rec loop (i: int) =
if i > last then restil
- else
- if last - i > 100_000 then
- Kernel.fatal ~current:true "INDEX_RANGE too large"
else
(top (Cabs.ATINDEX_INIT(
{ expr_node = Cabs.CONSTANT(Cabs.CONST_INT(string_of_int i));
@@ -10106,12 +10106,10 @@ and doStatement local_env (s : Cabs.statement) : chunk =
"Cannot understand the constants in case range"
in
if il > ih then Kernel.error ~once:true ~current:true "Empty case range";
+ (* Arbitrary limit to avoid building an impractical AST. *)
+ if ih - il > 100_000 then Kernel.fatal ~current:true "Case range too large";
let rec mkAll (i: int) =
- if i > ih then [] else
- if ih - i > 100_000 then
- Kernel.fatal ~current:true "Case range too large"
- else
- integer ~loc i :: mkAll (i + 1)
+ if i > ih then [] else integer ~loc i :: mkAll (i + 1)
in
(sel @@ (seh,ghost)) @@
(caseRangeChunk ~ghost (mkAll il) loc' (doStatement local_env s),
--
GitLab