From d91eb3c809f1bc22731b05fcefa1418469e69826 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 13 Oct 2021 09:15:24 +0200
Subject: [PATCH] [Eva] Minor simplification to catch exceptions when reading
loop unroll limits.
---
.../partitioning/partitioning_parameters.ml | 23 ++++++-------------
.../oracle/very_large_integers.11.res.oracle | 2 +-
2 files changed, 8 insertions(+), 17 deletions(-)
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 83bd2e974ce..4ddcf183521 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -93,22 +93,13 @@ 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)
- with Db.Properties.Interp.No_conversion ->
- warn "loop unrolling parameters must be valid expressions; \
- ignoring";
- default
+ try
+ match Logic_utils.constFoldTermToInt t with
+ | Some n -> Partition.IntLimit (Integer.to_int_exn n)
+ | None -> Partition.ExpLimit (term_to_exp t)
+ with Z.Overflow | Db.Properties.Interp.No_conversion ->
+ warn "invalid loop unrolling parameter; ignoring";
+ default
end
| _ ->
warn "invalid unroll annotation; ignoring";
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index f34db553ef8..fca174f9e70 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -10,6 +10,6 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[kernel:annot-error] tests/syntax/very_large_integers.c:92: Warning:
- invalid loop unrolling parameter (-9999999999999999999); ignoring
+ invalid loop unrolling parameter; ignoring
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] Frama-C aborted: invalid user input.
--
GitLab