From 86589b84169ee4f87a703ba25b170da9e4efc0e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 8 Jun 2021 12:04:20 +0200
Subject: [PATCH] [Eva] Minor simplifications when using Integer.to_int[_opt].
---
src/plugins/value/partitioning/partition.ml | 8 ++------
.../partitioning/partitioning_parameters.ml | 18 +++++-------------
2 files changed, 7 insertions(+), 19 deletions(-)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 9dc56a4aa9d..78b80a60185 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -336,15 +336,11 @@ struct
let eval_exp_to_int state exp =
let _valuation, ival = evaluate_exp_to_ival state exp in
- try
- match Integer.to_int_opt (Ival.project_int ival) with
- | Some i -> i
- | None -> fail ~exp "this partitioning parameter overflows an integer"
+ try Integer.to_int (Ival.project_int ival)
with
| Ival.Not_Singleton_Int ->
fail ~exp "this partitioning parameter must evaluate to a singleton"
- | Failure _ ->
- fail ~exp "this partitioning parameter is too big"
+ | Z.Overflow -> fail ~exp "this partitioning parameter overflows an integer"
let split_by_predicate state predicate =
let env =
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 567f2b5f2cb..1c8dae31e04 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -93,19 +93,11 @@ struct
let t =
Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
in
- match Logic_utils.constFoldTermToInt t with
- | Some n ->
- begin
- match Integer.to_int_opt n with
- | Some n' -> Partition.IntLimit n'
- | None ->
- warn "invalid loop unrolling parameter (%a); ignoring"
- (Integer.pretty ~hexa:false) n;
- default
- end
- | None ->
- try
- Partition.ExpLimit (term_to_exp t)
+ let i = Logic_utils.constFoldTermToInt t in
+ match Option.bind i Integer.to_int_opt with
+ | Some n -> Partition.IntLimit n
+ | None ->
+ try Partition.ExpLimit (term_to_exp t)
with Db.Properties.Interp.No_conversion ->
warn "loop unrolling parameters must be valid expressions; \
ignoring";
--
GitLab