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 c378f1bdfa8f5e89321b2daea06ade7a3ee86859..5dcc2de5a21ce3139e20862557446d4299299c1b 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 6c3c77861ed8667589c2fb64981aba467a1dea4d..84a4316338db453bc483f0e311c93e0eebb69ded 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 7e304dd9f6346d6ccc3c9ac22ab6000f7ad7250f..7f58d32597472b8d888b386b64547b1602bf8684 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