From 5141907fbd6d575d6321766c8fb0fb06cdb8acc9 Mon Sep 17 00:00:00 2001
From: Guillaume Petiot <guillaume.petiot@cea.fr>
Date: Mon, 4 Feb 2013 07:57:47 +0000
Subject: [PATCH] [e-acsl] Renamed function Cil.alignOf_int into
 Cil.bytesAlignOf

---
 src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c   | 1 -
 .../e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h        | 2 +-
 src/plugins/e-acsl/typing.ml                                    | 2 +-
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index c378f1bdfa8..5dcc2de5a21 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -8,7 +8,6 @@
 #include "e_acsl_bittree.h"
 #include "e_acsl_mmodel.h"
 
-#define WORDBITS 64
 
 #if WORDBITS == 16
 
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index 6c3c77861ed..84a4316338d 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -13,7 +13,7 @@
 #elif E_ACSL_MACHDEP == x86_16
 #define WORDBITS 16
 #else
-#define WORDBITS 64
+#define WORDBITS 32
 #endif
 
 /* Memory block allocated and may be deallocated */
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 7e304dd9f63..7f58d325974 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -213,7 +213,7 @@ let size_of ty =
   try int_to_interv (Cil.sizeOf_int ty)
   with Cil.SizeOfError _ -> eacsl_typ_of_typ Cil.ulongLongType
 
-let align_of ty = int_to_interv (Cil.alignOf_int ty)
+let align_of ty = int_to_interv (Cil.bytesAlignOf ty)
 
 type offset_ty = Ty_no_offset | Ty_field of eacsl_typ | Ty_index of eacsl_typ
 
-- 
GitLab