diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h
index df845fa24bd02f32bb687b907bf774776ff084f2..aef4f536c808adcd12ea9bfdbc82d645e3d81418 100644
--- a/share/libc/__fc_gcc_builtins.h
+++ b/share/libc/__fc_gcc_builtins.h
@@ -26,6 +26,7 @@
#ifndef __FC_GCC_BUILTINS
#define __FC_GCC_BUILTINS
#include "features.h"
+#include "__fc_machdep.h"
__PUSH_FC_STDLIB
@@ -193,6 +194,66 @@ _Bool __builtin_umull_overflow (unsigned long a, unsigned long b, unsigned long
*/
_Bool __builtin_umulll_overflow (unsigned long long a, unsigned long long b, unsigned long long *res);
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_clz (unsigned int x);
+
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_clzl (unsigned long x);
+
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_clzll (unsigned long long x);
+
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_ctz (unsigned int x);
+
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_ctzl (unsigned long x);
+
+/*@
+ requires x_nonzero: x != 0;
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result < __CHAR_BIT * sizeof(x);
+ */
+int __builtin_ctzll (unsigned long long x);
+
+/*@
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
+ */
+int __builtin_popcount (unsigned int x);
+
+/*@
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
+ */
+int __builtin_popcountl (unsigned long x);
+
+/*@
+ assigns \result \from indirect:x;
+ ensures result_is_bit_count: 0 <= \result <= __CHAR_BIT * sizeof(x);
+ */
+int __builtin_popcountll (unsigned long long x);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/__fc_machdep.h b/share/libc/__fc_machdep.h
index 6411df164b8ce1a9ac78aa3eabb30942dcf41e0e..39a8c7b78a436263450fdc5f9e7ffa35ccdfcdf7 100644
--- a/share/libc/__fc_machdep.h
+++ b/share/libc/__fc_machdep.h
@@ -26,9 +26,6 @@
#if defined(__FC_MACHDEP_X86_32) || defined(__FC_MACHDEP_GCC_X86_32)
#define __FC_FORCE_INCLUDE_MACHDEP__
#include "__fc_machdep_linux_shared.h"
-#ifdef __FC_MACHDEP_GCC_X86_32
-#include "__fc_gcc_builtins.h"
-#endif
#undef __FC_FORCE_INCLUDE_MACHDEP__
#define __FC_BYTE_ORDER __LITTLE_ENDIAN
/* Required */
@@ -112,14 +109,15 @@
#define __FC_WINT_MIN 0
#define __FC_WINT_MAX __FC_UINT_MAX
+#ifdef __FC_MACHDEP_GCC_X86_32
+#include "__fc_gcc_builtins.h"
+#endif
+
// End of X86_32 || GCC_X86_32
#else
#if defined(__FC_MACHDEP_X86_64) || defined(__FC_MACHDEP_GCC_X86_64)
#define __FC_FORCE_INCLUDE_MACHDEP__
#include "__fc_machdep_linux_shared.h"
-#ifdef __FC_MACHDEP_GCC_X86_64
-#include "__fc_gcc_builtins.h"
-#endif
#undef __FC_FORCE_INCLUDE_MACHDEP__
#define __FC_BYTE_ORDER __LITTLE_ENDIAN
/* Required */
@@ -212,14 +210,15 @@
#define __FC_WINT_MIN 0
#define __FC_WINT_MAX __FC_UINT_MAX
+#ifdef __FC_MACHDEP_GCC_X86_64
+#include "__fc_gcc_builtins.h"
+#endif
+
// End of X86_64 || GCC_X86_64
#else
#if defined(__FC_MACHDEP_X86_16) || defined(__FC_MACHDEP_GCC_X86_16)
#define __FC_FORCE_INCLUDE_MACHDEP__
#include "__fc_machdep_linux_shared.h"
-#ifdef __FC_MACHDEP_GCC_X86_16
-#include "__fc_gcc_builtins.h"
-#endif
#undef __FC_FORCE_INCLUDE_MACHDEP__
#define __FC_BYTE_ORDER __LITTLE_ENDIAN
/* Required */
@@ -315,6 +314,10 @@
#define __FC_WINT_MIN 0
#define __FC_WINT_MAX __FC_ULONG_MAX
+#ifdef __FC_MACHDEP_GCC_X86_16
+#include "__fc_gcc_builtins.h"
+#endif
+
// End of X86_16 || GCC_X86_16
#else
#ifdef __FC_MACHDEP_PPC_32
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index e8ae6d486057747ea1dcc2ea5e5b18d52fd7756c..544e912ca692472f847d2aa060ffd96c604f2c19 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4994,13 +4994,7 @@ let initGccBuiltins () : unit =
add "coshf" floatType [ floatType ] false;
add "coshl" longDoubleType [ longDoubleType ] false;
- add "clz" intType [ uintType ] false;
- add "clzl" intType [ ulongType ] false;
- add "clzll" intType [ ulongLongType ] false;
add "constant_p" intType [ intType ] false;
- add "ctz" intType [ uintType ] false;
- add "ctzl" intType [ ulongType ] false;
- add "ctzll" intType [ ulongLongType ] false;
add "exp" doubleType [ doubleType ] false;
add "expf" floatType [ floatType ] false;
@@ -5071,10 +5065,6 @@ let initGccBuiltins () : unit =
add "parityl" intType [ ulongType ] false;
add "parityll" intType [ ulongLongType ] false;
- add "popcount" intType [ uintType ] false;
- add "popcountl" intType [ ulongType ] false;
- add "popcountll" intType [ ulongLongType ] false;
-
add "powi" doubleType [ doubleType; intType ] false;
add "powif" floatType [ floatType; intType ] false;
add "powil" longDoubleType [ longDoubleType; intType ] false;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 42381d641e8bc28066722d4c81e162c4763744cd..8a80b25247831cfca43226478f5dced6e8568b54 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -232,61 +232,6 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_h_short(int s)
-{
- return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
- return x;
-}
-
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__10;
- __gmpq_init(__gen_e_acsl__8);
- __gmpq_set_str(__gen_e_acsl__8,"1",10);
- __gmpq_init(__gen_e_acsl__9);
- __gmpq_set_d(__gen_e_acsl__9,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
- __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__8);
- __gmpq_clear(__gen_e_acsl__9);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
- return __gen_e_acsl__10;
-}
-
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
-int __gen_e_acsl_p1(int x, int y)
-{
- int __retres = x + (long)y > 0L;
- return __retres;
-}
-
-long __gen_e_acsl_t2(mystruct m)
-{
- long __retres = m.k + (long)m.l;
- return __retres;
-}
-
int __gen_e_acsl_p2(int x, int y)
{
int __retres = x + (long)y > 0L;
@@ -384,4 +329,59 @@ int __gen_e_acsl_h_char(int c)
return c;
}
+int __gen_e_acsl_h_short(int s)
+{
+ return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"1",10);
+ __gmpq_init(__gen_e_acsl__9);
+ __gmpq_set_d(__gen_e_acsl__9,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__8);
+ __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ return __gen_e_acsl__10;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ int __retres = x + (long)y > 0L;
+ return __retres;
+}
+
+long __gen_e_acsl_t2(mystruct m)
+{
+ long __retres = m.k + (long)m.l;
+ return __retres;
+}
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b9015c95933c865e01c9d365c7a3b2c73c8c4a4f..d7e6ba9cda321e94b0312fcf67ef5007ba3a8486 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -105,6 +105,88 @@ int main(void)
return __retres;
}
+int __gen_e_acsl_g(int n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_g_5(long n)
+{
+ int __retres = 0;
+ return __retres;
+}
+
+int __gen_e_acsl_f3(int n)
+{
+ int __gen_e_acsl_if_6;
+ if (n > 0) {
+ int __gen_e_acsl_g_2;
+ int __gen_e_acsl_f3_5;
+ __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+ __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_8;
+ __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+int __gen_e_acsl_f3_2(long n)
+{
+ int __gen_e_acsl_if_5;
+ if (n > 0L) {
+ int __gen_e_acsl_g_4;
+ int __gen_e_acsl_f3_4;
+ __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
+ __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_6;
+ __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
+ __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
+ }
+ return __gen_e_acsl_if_5;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+ unsigned long __gen_e_acsl_if_10;
+ if (n < 100) {
+ unsigned long __gen_e_acsl_f4_5;
+ __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_9;
+ if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
+ else __gen_e_acsl_if_9 = 6UL;
+ __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
+ }
+ return __gen_e_acsl_if_10;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_8;
+ if (n < 100L) {
+ unsigned long __gen_e_acsl_f4_4;
+ __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+ __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_7;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+ else __gen_e_acsl_if_7 = 6UL;
+ __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+ }
+ return __gen_e_acsl_if_8;
+}
+
void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
{
__e_acsl_mpz_t __gen_e_acsl_if_2;
@@ -235,86 +317,4 @@ int __gen_e_acsl_f2_2(long n)
return __gen_e_acsl_if_3;
}
-int __gen_e_acsl_g(int n)
-{
- int __retres = 0;
- return __retres;
-}
-
-int __gen_e_acsl_g_5(long n)
-{
- int __retres = 0;
- return __retres;
-}
-
-int __gen_e_acsl_f3(int n)
-{
- int __gen_e_acsl_if_6;
- if (n > 0) {
- int __gen_e_acsl_g_2;
- int __gen_e_acsl_f3_5;
- __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
- __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
- }
- else {
- int __gen_e_acsl_g_8;
- __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
- }
- return __gen_e_acsl_if_6;
-}
-
-int __gen_e_acsl_f3_2(long n)
-{
- int __gen_e_acsl_if_5;
- if (n > 0L) {
- int __gen_e_acsl_g_4;
- int __gen_e_acsl_f3_4;
- __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
- __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
- }
- else {
- int __gen_e_acsl_g_6;
- __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
- }
- return __gen_e_acsl_if_5;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
-{
- unsigned long __gen_e_acsl_if_10;
- if (n < 100) {
- unsigned long __gen_e_acsl_f4_5;
- __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
- }
- else {
- unsigned long __gen_e_acsl_if_9;
- if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
- else __gen_e_acsl_if_9 = 6UL;
- __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
- }
- return __gen_e_acsl_if_10;
-}
-
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_8;
- if (n < 100L) {
- unsigned long __gen_e_acsl_f4_4;
- __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
- __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
- }
- else {
- unsigned long __gen_e_acsl_if_7;
- if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
- else __gen_e_acsl_if_7 = 6UL;
- __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
- }
- return __gen_e_acsl_if_8;
-}
-
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 2bdf4cd9f28dee2f151cd9ff921dc647cbbcff9d..91010d0c7a4cd82b480d4e6cbf53122b5e49ce5b 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -277,92 +277,6 @@ void __gen_e_acsl_k(int x)
return;
}
-int __gen_e_acsl_h_short(int s)
-{
- return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
- return x;
-}
-
-double __gen_e_acsl_f2(double x)
-{
- __e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl_div;
- double __gen_e_acsl__15;
- __gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"1",10);
- __gmpq_init(__gen_e_acsl__14);
- __gmpq_set_d(__gen_e_acsl__14,x);
- __gmpq_init(__gen_e_acsl_div);
- __gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
- __gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
- __gmpq_clear(__gen_e_acsl_div);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
- return __gen_e_acsl__15;
-}
-
-int __gen_e_acsl_g(int x)
-{
- int __gen_e_acsl_g_hidden_2;
- __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
- return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
- return m;
-}
-
-int __gen_e_acsl_p1(int x, int y)
-{
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_gt;
- __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
- __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- int __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl_);
- return __retres;
-}
-
-void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
-{
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
- __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_add_7);
- return;
-}
-
int __gen_e_acsl_p2(int x, int y)
{
__e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -477,4 +391,90 @@ int __gen_e_acsl_h_char(int c)
return c;
}
+int __gen_e_acsl_h_short(int s)
+{
+ return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+ return x;
+}
+
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__13;
+ __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__15;
+ __gmpq_init(__gen_e_acsl__13);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
+ return __gen_e_acsl__15;
+}
+
+int __gen_e_acsl_g(int x)
+{
+ int __gen_e_acsl_g_hidden_2;
+ __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+ return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+ return m;
+}
+
+int __gen_e_acsl_p1(int x, int y)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+ __gmpz_init_set_si(__gen_e_acsl_y,(long)y);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ int __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl_);
+ return __retres;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
+{
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
+ __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ return;
+}
+
diff --git a/tests/libc/more_gcc_builtins.c b/tests/libc/more_gcc_builtins.c
index 835f64e8cc80a61eacd93ae770e9db917b75881f..d3d023ac786338c8701dd77e2a3baaefbc959b03 100644
--- a/tests/libc/more_gcc_builtins.c
+++ b/tests/libc/more_gcc_builtins.c
@@ -2,7 +2,7 @@
STDOPT: #"-machdep gcc_x86_32"
*/
-
+volatile int v;
#include <limits.h>
int main() {
@@ -42,5 +42,32 @@ int main() {
r = __builtin_smulll_overflow(-1, LLONG_MIN, &llres);
//@ assert llres == (long long)(-1 * LLONG_MIN);
//@ assert r == 1;
+ if (v) {
+ __builtin_clz(0);
+ //@ assert unreachable:\false;
+ }
+ res = __builtin_clz(1);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(int);
+ res = __builtin_clzl(ULONG_MAX);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(long);
+ res = __builtin_clzll(ULLONG_MAX);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(long long);
+ if (v) {
+ __builtin_ctz(0);
+ //@ assert unreachable:\false;
+ }
+ res = __builtin_ctz(42);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(int);
+ res = __builtin_ctzl(1234567);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(long);
+ res = __builtin_ctzll(1);
+ //@ assert 0 <= res < CHAR_BIT * sizeof(long long);
+
+ res = __builtin_popcount(0);
+ //@ assert 0 <= res <= CHAR_BIT * sizeof(int);
+ res = __builtin_popcountl(ULONG_MAX);
+ //@ assert 0 <= res <= CHAR_BIT * sizeof(long);
+ res = __builtin_popcountll(ULLONG_MAX);
+ //@ assert 0 <= res <= CHAR_BIT * sizeof(long long);
return 0;
}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index f0d8a56d9da389ed98ffffb2f82d20a89d8716b8..fefd9fce133ac0e463ea535e54a79caec09fc2af 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -40,7 +40,7 @@
unsetenv (0 call); wcscat (0 call); wcscpy (0 call); wcslen (2 calls);
wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call); wmemset (0 call);
- Undefined functions (397)
+ Undefined functions (406)
=========================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -51,18 +51,21 @@
Frama_C_unsigned_long_interval (0 call);
Frama_C_unsigned_long_long_interval (0 call);
Frama_C_unsigned_short_interval (0 call); _Exit (0 call);
- __builtin_abort (1 call); __builtin_sadd_overflow (0 call);
- __builtin_saddl_overflow (0 call); __builtin_saddll_overflow (0 call);
- __builtin_smul_overflow (0 call); __builtin_smull_overflow (0 call);
- __builtin_smulll_overflow (0 call); __builtin_ssub_overflow (0 call);
- __builtin_ssubl_overflow (0 call); __builtin_ssubll_overflow (0 call);
- __builtin_uadd_overflow (0 call); __builtin_uaddl_overflow (0 call);
- __builtin_uaddll_overflow (0 call); __builtin_umul_overflow (0 call);
- __builtin_umull_overflow (0 call); __builtin_umulll_overflow (0 call);
- __builtin_usub_overflow (0 call); __builtin_usubl_overflow (0 call);
- __builtin_usubll_overflow (0 call); __fc_fpclassify (0 call);
- __fc_fpclassifyf (0 call); __fc_infinity (0 call); __fc_nan (0 call);
- __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
+ __builtin_abort (1 call); __builtin_clz (0 call); __builtin_clzl (0 call);
+ __builtin_clzll (0 call); __builtin_ctz (0 call); __builtin_ctzl (0 call);
+ __builtin_ctzll (0 call); __builtin_popcount (0 call);
+ __builtin_popcountl (0 call); __builtin_popcountll (0 call);
+ __builtin_sadd_overflow (0 call); __builtin_saddl_overflow (0 call);
+ __builtin_saddll_overflow (0 call); __builtin_smul_overflow (0 call);
+ __builtin_smull_overflow (0 call); __builtin_smulll_overflow (0 call);
+ __builtin_ssub_overflow (0 call); __builtin_ssubl_overflow (0 call);
+ __builtin_ssubll_overflow (0 call); __builtin_uadd_overflow (0 call);
+ __builtin_uaddl_overflow (0 call); __builtin_uaddll_overflow (0 call);
+ __builtin_umul_overflow (0 call); __builtin_umull_overflow (0 call);
+ __builtin_umulll_overflow (0 call); __builtin_usub_overflow (0 call);
+ __builtin_usubl_overflow (0 call); __builtin_usubll_overflow (0 call);
+ __fc_fpclassify (0 call); __fc_fpclassifyf (0 call); __fc_infinity (0 call);
+ __fc_nan (0 call); __va_fcntl_flock (0 call); __va_fcntl_int (0 call);
__va_fcntl_void (0 call); __va_ioctl_int (0 call); __va_ioctl_ptr (0 call);
__va_ioctl_void (0 call); __va_open_mode_t (0 call);
__va_open_void (0 call); __va_openat_mode_t (0 call);
@@ -181,7 +184,7 @@
Goto = 89
Assignment = 438
Exit point = 82
- Function = 479
+ Function = 488
Function call = 89
Pointer dereferencing = 158
Cyclomatic complexity = 286
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index c4e0a539a60ff3e4315e6d03fc56aa523733ffe4..f940ecca0a0a3bd89df54454c6c97cbe5cbfa77a 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -7238,6 +7238,66 @@ _Bool __builtin_umull_overflow(unsigned long a, unsigned long b,
_Bool __builtin_umulll_overflow(unsigned long long a, unsigned long long b,
unsigned long long *res);
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_clz(unsigned int x);
+
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_clzl(unsigned long x);
+
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_clzll(unsigned long long x);
+
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_ctz(unsigned int x);
+
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_ctzl(unsigned long x);
+
+/*@ requires x_nonzero: x ≢ 0;
+ ensures result_is_bit_count: 0 ≤ \result < 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_ctzll(unsigned long long x);
+
+/*@ ensures result_is_bit_count: 0 ≤ \result ≤ 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_popcount(unsigned int x);
+
+/*@ ensures result_is_bit_count: 0 ≤ \result ≤ 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_popcountl(unsigned long x);
+
+/*@ ensures result_is_bit_count: 0 ≤ \result ≤ 8 * sizeof(\old(x));
+ assigns \result;
+ assigns \result \from (indirect: x);
+ */
+int __builtin_popcountll(unsigned long long x);
+
/*@ requires valid_filename: valid_read_string(filename);
assigns \result;
assigns \result \from (indirect: *(filename + (0 ..))), (indirect: mode);
diff --git a/tests/libc/oracle/more_gcc_builtins.res.oracle b/tests/libc/oracle/more_gcc_builtins.res.oracle
index 0ad30701226b8bdd8f77ce8a05a61da4d36caca3..91b6a0d432d63d1e7c29f12e19155a1da1251880 100644
--- a/tests/libc/oracle/more_gcc_builtins.res.oracle
+++ b/tests/libc/oracle/more_gcc_builtins.res.oracle
@@ -3,7 +3,7 @@
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-
+ v ∈ [--..--]
[eva] computing for function __builtin_sadd_overflow <- main.
Called from tests/libc/more_gcc_builtins.c:10.
[eva] using specification for function __builtin_sadd_overflow
@@ -82,11 +82,78 @@
[eva] Done for function __builtin_smulll_overflow
[eva] tests/libc/more_gcc_builtins.c:43: assertion got status valid.
[eva] tests/libc/more_gcc_builtins.c:44: assertion got status valid.
+[eva] computing for function __builtin_clz <- main.
+ Called from tests/libc/more_gcc_builtins.c:46.
+[eva] using specification for function __builtin_clz
+[eva:alarm] tests/libc/more_gcc_builtins.c:46: Warning:
+ function __builtin_clz: precondition 'x_nonzero' got status invalid.
+[eva] Done for function __builtin_clz
+[eva] computing for function __builtin_clz <- main.
+ Called from tests/libc/more_gcc_builtins.c:49.
+[eva] tests/libc/more_gcc_builtins.c:49:
+ function __builtin_clz: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_clz
+[eva] tests/libc/more_gcc_builtins.c:50: assertion got status valid.
+[eva] computing for function __builtin_clzl <- main.
+ Called from tests/libc/more_gcc_builtins.c:51.
+[eva] using specification for function __builtin_clzl
+[eva] tests/libc/more_gcc_builtins.c:51:
+ function __builtin_clzl: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_clzl
+[eva] tests/libc/more_gcc_builtins.c:52: assertion got status valid.
+[eva] computing for function __builtin_clzll <- main.
+ Called from tests/libc/more_gcc_builtins.c:53.
+[eva] using specification for function __builtin_clzll
+[eva] tests/libc/more_gcc_builtins.c:53:
+ function __builtin_clzll: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_clzll
+[eva] tests/libc/more_gcc_builtins.c:54: assertion got status valid.
+[eva] computing for function __builtin_ctz <- main.
+ Called from tests/libc/more_gcc_builtins.c:56.
+[eva] using specification for function __builtin_ctz
+[eva:alarm] tests/libc/more_gcc_builtins.c:56: Warning:
+ function __builtin_ctz: precondition 'x_nonzero' got status invalid.
+[eva] Done for function __builtin_ctz
+[eva] computing for function __builtin_ctz <- main.
+ Called from tests/libc/more_gcc_builtins.c:59.
+[eva] tests/libc/more_gcc_builtins.c:59:
+ function __builtin_ctz: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_ctz
+[eva] tests/libc/more_gcc_builtins.c:60: assertion got status valid.
+[eva] computing for function __builtin_ctzl <- main.
+ Called from tests/libc/more_gcc_builtins.c:61.
+[eva] using specification for function __builtin_ctzl
+[eva] tests/libc/more_gcc_builtins.c:61:
+ function __builtin_ctzl: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_ctzl
+[eva] tests/libc/more_gcc_builtins.c:62: assertion got status valid.
+[eva] computing for function __builtin_ctzll <- main.
+ Called from tests/libc/more_gcc_builtins.c:63.
+[eva] using specification for function __builtin_ctzll
+[eva] tests/libc/more_gcc_builtins.c:63:
+ function __builtin_ctzll: precondition 'x_nonzero' got status valid.
+[eva] Done for function __builtin_ctzll
+[eva] tests/libc/more_gcc_builtins.c:64: assertion got status valid.
+[eva] computing for function __builtin_popcount <- main.
+ Called from tests/libc/more_gcc_builtins.c:66.
+[eva] using specification for function __builtin_popcount
+[eva] Done for function __builtin_popcount
+[eva] tests/libc/more_gcc_builtins.c:67: assertion got status valid.
+[eva] computing for function __builtin_popcountl <- main.
+ Called from tests/libc/more_gcc_builtins.c:68.
+[eva] using specification for function __builtin_popcountl
+[eva] Done for function __builtin_popcountl
+[eva] tests/libc/more_gcc_builtins.c:69: assertion got status valid.
+[eva] computing for function __builtin_popcountll <- main.
+ Called from tests/libc/more_gcc_builtins.c:70.
+[eva] using specification for function __builtin_popcountll
+[eva] Done for function __builtin_popcountll
+[eva] tests/libc/more_gcc_builtins.c:71: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
- res ∈ {-2147483607}
+ res ∈ [0..64]
r ∈ {1}
lres ∈ {2147483647}
llres ∈ {-9223372036854775808}
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 4e0e7ae6c6aa45fbc67adee69362135b5dd1fcb6..091c7d8002d8a53274789b3887edaaec956ffbe2 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -81,12 +81,6 @@
long double __builtin_ceill(long double);
- int __builtin_clz(unsigned int);
-
- int __builtin_clzl(unsigned long);
-
- int __builtin_clzll(unsigned long long);
-
int __builtin_constant_p(int);
double __builtin_cos(double);
@@ -101,12 +95,6 @@
long double __builtin_cosl(long double);
- int __builtin_ctz(unsigned int);
-
- int __builtin_ctzl(unsigned long);
-
- int __builtin_ctzll(unsigned long long);
-
double __builtin_exp(double);
long __builtin_expect(long, long);
@@ -217,12 +205,6 @@
int __builtin_parityll(unsigned long long);
- int __builtin_popcount(unsigned int);
-
- int __builtin_popcountl(unsigned long);
-
- int __builtin_popcountll(unsigned long long);
-
double __builtin_powi(double, int);
float __builtin_powif(float, int);