From 70d5f60f6fc1748d8b0e6ac71c39630bf743a227 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 19 Feb 2016 10:36:08 +0100
Subject: [PATCH] [RTL] Fixed a bug where the bittree memory model was always
using 64-bit words
---
.../e-acsl/share/e-acsl/adt_models/e_acsl_adt_api.h | 12 ------------
.../e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h | 3 ++-
2 files changed, 2 insertions(+), 13 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_api.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_api.h
index 33babbd4b2a..a103888b280 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_api.h
@@ -26,18 +26,6 @@
#include "stdlib.h"
#include "stdbool.h"
-#if E_ACSL_MACHDEP == x86_64
-#define WORDBITS 64
-#elif E_ACSL_MACHDEP == x86_32
-#define WORDBITS 32
-#elif E_ACSL_MACHDEP == ppc_32
-#define WORDBITS 32
-#elif E_ACSL_MACHDEP == x86_16
-#define WORDBITS 16
-#else
-#define WORDBITS 32
-#endif
-
/* Memory block allocated and may be deallocated */
struct _block {
size_t ptr; /* begin address */
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
index 655caa5ded3..680006f7fb9 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
@@ -31,6 +31,8 @@
#include "e_acsl_assert.h"
#include "e_acsl_adt_api.h"
+#define WORDBITS __WORDSIZE
+
static size_t mask(size_t, size_t);
#if WORDBITS == 16
@@ -79,7 +81,6 @@ static const size_t Tmasks[] = {
0xffffffffffffff80,0xffffffffffffffc0,0xffffffffffffffe0,0xfffffffffffffff0,
0xfffffffffffffff8,0xfffffffffffffffc,0xfffffffffffffffe,0xffffffffffffffff};
-
static const int Teq[] =
{ 0,-1,3,-3,6,-5,7,-7,12,-9,11,-11,14,-13,15,-15,24,-17,19,-19,22,-21,23,-23,
28,-25,27,-27,30,-29,31,-31,48,-33,35,-35,38,-37,39,-39,44,-41,43,-43,46,
--
GitLab