diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h new file mode 100644 index 0000000000000000000000000000000000000000..514be04fcfeb94f1f84669c0a73f57df8f8cfb63 --- /dev/null +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h @@ -0,0 +1,42 @@ +/**************************************************************************/ +/* */ +/* This file is part of Frama-C. */ +/* */ +/* Copyright (C) 2007-2017 */ +/* CEA (Commissariat à l'énergie atomique et aux énergies */ +/* alternatives) */ +/* */ +/* you can redistribute it and/or modify it under the terms of the GNU */ +/* Lesser General Public License as published by the Free Software */ +/* Foundation, version 2.1. */ +/* */ +/* It is distributed in the hope that it will be useful, */ +/* but WITHOUT ANY WARRANTY; without even the implied warranty of */ +/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ +/* GNU Lesser General Public License for more details. */ +/* */ +/* See the GNU Lesser General Public License version 2.1 */ +/* for more details (enclosed in the file licenses/LGPLv2.1). */ +/* */ +/**************************************************************************/ + +/*! *********************************************************************** + * \file e_acsl_alias.h + * + * \brief Function aliasing +***************************************************************************/ + +#ifndef E_ACSL_ALIAS +#define E_ACSL_ALIAS + +/** Define `aliasname` as a strong alias for `name`. */ +# define strong_alias(name, aliasname) _strong_alias(name, aliasname) +# define _strong_alias(name, aliasname) \ + extern __typeof (name) aliasname __attribute__ ((alias (#name))); + +/** Define `aliasname` as a weak alias for `name`. */ +# define weak_alias(name, aliasname) _weak_alias (name, aliasname) +# define _weak_alias(name, aliasname) \ + extern __typeof (name) aliasname __attribute__ ((weak, alias (#name))); + +#endif diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h index 4bcaeef93e2c2a5fc4acd17a54ccc3c6a4f5033d..4099f7bcbc88119eace53656a8b2ade37b9b0321 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h @@ -29,11 +29,11 @@ /* Should be included after * printf, debug and assert but before the actual code */ -#include <stddef.h> - #ifndef E_ACSL_MALLOC #define E_ACSL_MALLOC +#include <stddef.h> + /** Define `aliasname` as a strong alias for `name`. */ # define strong_alias(name, aliasname) _strong_alias(name, aliasname) # define _strong_alias(name, aliasname) \ diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c index 59cd3916d247e4d8801586e165c41531b6b3c518..bd3287a10eddfd17efec2bed210ed081aa0cc42c 100644 --- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c +++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel.c @@ -34,6 +34,7 @@ #include "e_acsl_printf.h" #include "e_acsl_debug.h" #include "e_acsl_assert.h" +#include "e_acsl_alias.h" #include "e_acsl_malloc.h" #include "e_acsl_safe_locations.h"