From ffcde68d64de82b87a7212dc003b9efce7826782 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 11 Jun 2021 16:24:15 +0200
Subject: [PATCH] [eacsl] Fix generated pointer in `&a[x..y]` annotation
The previous version generated `&a + x` instead of `a + x` but the
pointer arithmetic on `&a + x` is that we move the pointer `x` times the
size of the entire array instead of `x` times the size of an element of
the array.
---
src/plugins/e-acsl/src/code_generator/memory_translate.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 41fedc2159b..8c05dec0200 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -339,7 +339,6 @@ let extract_quantifiers ~loc args =
([], [])
args
-
(* [call_with_tset
~loc
~arg_from_range
@@ -443,7 +442,7 @@ let call_with_tset ~loc ~arg_from_range ~arg_from_term ?(prepend_n_args=false) k
assert (Logic_const.is_set_type t.term_type);
let lty_noset = Logic_const.type_of_element t.term_type in
let ptr =
- Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset
+ Logic_const.term ~loc (TStartOf (TVar lv, TNoOffset)) lty_noset
in
arg_from_range ~loc kf env rev_args ptr r p
| _ ->
--
GitLab