From f88ddb494c3454f7d52a8ffeb17a6ef37847f874 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 9 Jul 2020 14:11:46 +0200
Subject: [PATCH] [eacsl:codegen] Fix translation of ranges
The ranges are inclusives, so the number of elements in `[n1 .. n2]` is
`n2 - n1 + 1`.
---
.../src/code_generator/mmodel_translate.ml | 18 +++++++++++-------
1 file changed, 11 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
index 7412783c89a..79332b59138 100644
--- a/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/mmodel_translate.ml
@@ -204,13 +204,17 @@ let call_memory_block ~loc kf name ctx env ptr r p =
we need to clone them in order to force retyping *)
let s = { s with term_node = s.term_node } in
let n1 = { n1 with term_node = n1.term_node } in
- Logic_const.term
- ~loc
- (TBinOp(
- Mult,
- s,
- Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
- Linteger
+ (* The range are inclusives, so the total number of elements is
+ [n2 - n1 + 1] *)
+ let count = Logic_const.term
+ ~loc
+ (TBinOp (
+ PlusA,
+ Logic_const.term ~loc (TBinOp (MinusA, n2, n1)) Linteger,
+ Logic_const.tinteger ~loc 1))
+ Linteger
+ in
+ Logic_const.term ~loc (TBinOp (Mult, s, count)) Linteger
in
Typing.type_term ~use_gmp_opt:false size_term;
let size, env = match Typing.get_number_ty size_term with
--
GitLab