diff --git a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c index 54948acabb34603ad326da9f69746e4e096e980f..1610681b16dbce6e48a5f08934ecb5fb1c24320d 100644 --- a/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c +++ b/src/plugins/e-acsl/doc/userman/examples/instrumented_first.c @@ -8,24 +8,24 @@ #include "stddef.h" #include "stdio.h" struct __e_acsl_contract_t; -typedef struct __e_acsl_contract_t __attribute__((__FC_BUILTIN__)) __e_acsl_contract_t; +typedef struct __e_acsl_contract_t __attribute__((FC_BUILTIN)) __e_acsl_contract_t; struct __e_acsl_mpz_struct { int _mp_alloc ; int _mp_size ; unsigned long *_mp_d ; }; typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct; -typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1]; +typedef __e_acsl_mpz_struct ( __attribute__((FC_BUILTIN)) __e_acsl_mpz_t)[1]; struct __e_acsl_mpq_struct { __e_acsl_mpz_struct _mp_num ; __e_acsl_mpz_struct _mp_den ; }; typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct; -typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1]; +typedef __e_acsl_mpq_struct ( __attribute__((FC_BUILTIN)) __e_acsl_mpq_t)[1]; typedef unsigned long __e_acsl_mp_bitcnt_t; /*@ requires pred != 0; assigns \nothing; */ - __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int pred, + __attribute__((FC_BUILTIN)) void __e_acsl_assert(int pred, char const *kind, char const *fct, char const *pred_txt, diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h index d39f910421780a69e719773ae8c89af29530d051..93396d88fe674b77adbde777bd3ee3709bf0ddb7 100644 --- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h +++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h @@ -52,7 +52,7 @@ /*! \brief Structure to hold pieces of information about function and statement * contracts at runtime. */ -typedef struct contract_t __attribute__((__FC_BUILTIN__)) contract_t; +typedef struct contract_t __attribute__((FC_BUILTIN)) contract_t; /*! \brief Allocate and initialize a structure to hold pieces of information * about `size` behaviors. diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h index eede828f6a9481e960d1612f2d0b9e5ac0b4f96a..6c6be0174ddd6c6a119d6a4f11ca4d9d68942834 100644 --- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h +++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h @@ -49,7 +49,7 @@ struct eacsl_mpz_struct { }; typedef struct eacsl_mpz_struct eacsl_mpz_struct; -typedef eacsl_mpz_struct(__attribute__((__FC_BUILTIN__)) eacsl_mpz_t)[1]; +typedef eacsl_mpz_struct(__attribute__((FC_BUILTIN)) eacsl_mpz_t)[1]; struct eacsl_mpq_struct { eacsl_mpz_struct _mp_num; @@ -57,7 +57,7 @@ struct eacsl_mpq_struct { }; typedef struct eacsl_mpq_struct eacsl_mpq_struct; -typedef eacsl_mpq_struct(__attribute__((__FC_BUILTIN__)) eacsl_mpq_t)[1]; +typedef eacsl_mpq_struct(__attribute__((FC_BUILTIN)) eacsl_mpq_t)[1]; /** * Counts of bits of a multi-precision number are represented in the C type