diff --git a/share/libc/__fc_gcc_builtins.h b/share/libc/__fc_gcc_builtins.h
index 875f746cc4d71193055c581c0054ece30d86c456..6fb694b3dba48b4fc1d13026f43203d437816c60 100644
--- a/share/libc/__fc_gcc_builtins.h
+++ b/share/libc/__fc_gcc_builtins.h
@@ -254,6 +254,13 @@ int __builtin_popcountl (unsigned long x);
*/
int __builtin_popcountll (unsigned long long x);
+// According to the GCC docs
+// (https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html),
+// this creates a 'full memory barrier'; we do not model the concurrency
+// aspects yet.
+/*@ assigns \nothing; */
+void __sync_synchronize(void);
+
__END_DECLS
__POP_FC_STDLIB
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index f070c99028da28b9602d3c19c0742bad4fb22a6d..b990e16a029101eeb3a1762514523a6ba30e7914 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -647,7 +647,9 @@ let initGccBuiltins () : unit =
true;
| None -> ())
atomic_instances;
- add ~prefix:"" "__sync_synchronize" voidType [] true
+ (* __sync_synchronize has been declared non-variadic and a spec was added
+ to __fc_gcc_builtins.h; to avoid issues with pretty-printing, we removed
+ it from this list. *)
;;
(* Builtins related to va_list. Added to all non-msvc machdeps, because
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 946e4913da2a899e027877ced620e96ebdca02d5..eaeeebc57c865f7366b0125fa9ecd8769abf7639 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -64,7 +64,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (427)
+ Specified-only functions (428)
==============================
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);
@@ -89,24 +89,25 @@
__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);
- __va_openat_void (0 call); _exit (0 call); abort (0 call); accept (0 call);
- access (0 call); acos (0 call); acosf (0 call); acosh (0 call);
- acoshf (0 call); acoshl (0 call); acosl (0 call); alloca (0 call);
- asctime (0 call); asin (0 call); asinf (0 call); asinl (0 call);
- at_quick_exit (0 call); atan (0 call); atan2 (0 call); atan2f (0 call);
- atan2l (0 call); atanf (0 call); atanl (0 call); atexit (0 call);
- atof (0 call); atol (0 call); atoll (0 call); basename (0 call);
- bind (0 call); bsearch (0 call); bzero (0 call); ceil (0 call);
- ceilf (0 call); ceill (0 call); cfgetispeed (0 call); cfgetospeed (0 call);
- cfsetispeed (0 call); cfsetospeed (0 call); chdir (0 call); chown (0 call);
- chroot (0 call); clearerr (0 call); clearerr_unlocked (0 call);
- clock (0 call); clock_gettime (0 call); clock_nanosleep (0 call);
- close (0 call); closedir (0 call); closelog (0 call); connect (0 call);
- cos (0 call); cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
+ __sync_synchronize (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); __va_openat_void (0 call); _exit (0 call);
+ abort (0 call); accept (0 call); access (0 call); acos (0 call);
+ acosf (0 call); acosh (0 call); acoshf (0 call); acoshl (0 call);
+ acosl (0 call); alloca (0 call); asctime (0 call); asin (0 call);
+ asinf (0 call); asinl (0 call); at_quick_exit (0 call); atan (0 call);
+ atan2 (0 call); atan2f (0 call); atan2l (0 call); atanf (0 call);
+ atanl (0 call); atexit (0 call); atof (0 call); atol (0 call);
+ atoll (0 call); basename (0 call); bind (0 call); bsearch (0 call);
+ bzero (0 call); ceil (0 call); ceilf (0 call); ceill (0 call);
+ cfgetispeed (0 call); cfgetospeed (0 call); cfsetispeed (0 call);
+ cfsetospeed (0 call); chdir (0 call); chown (0 call); chroot (0 call);
+ clearerr (0 call); clearerr_unlocked (0 call); clock (0 call);
+ clock_gettime (0 call); clock_nanosleep (0 call); close (0 call);
+ closedir (0 call); closelog (0 call); connect (0 call); cos (0 call);
+ cosf (0 call); cosl (0 call); creat (0 call); ctime (0 call);
difftime (0 call); dirname (0 call); div (0 call); drand48 (0 call);
dup (0 call); dup2 (0 call); erand48 (0 call); execl (0 call);
execle (0 call); execlp (0 call); execv (0 call); execve (0 call);
@@ -221,7 +222,7 @@
Goto = 118
Assignment = 717
Exit point = 128
- Function = 556
+ Function = 557
Function call = 165
Pointer dereferencing = 350
Cyclomatic complexity = 435
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b5f06ccc75be5ebb84b9d3bcd50242b02460dd9f..c4986b27502f39b78667dc392d8fcf35ccac5af0 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8691,6 +8691,9 @@ int __builtin_popcountl(unsigned long x);
*/
int __builtin_popcountll(unsigned long long x);
+/*@ assigns \nothing; */
+void __sync_synchronize(void);
+
/*@ logic 𔹠bit_test(ℤ x, ℤ pos) = (x & (1 << pos)) ≢ 0;
*/
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 653ae8b9d4372589488a1ec1e37a4a5c555a5465..32d925b4bfe4c3c97c19d67815d1f978afa4b0b1 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -915,8 +915,6 @@
unsigned char __sync_sub_and_fetch_uint8_t(unsigned char volatile *__x0,
unsigned char __x1 , ...);
- void __sync_synchronize(...);
-
short __sync_val_compare_and_swap_int16_t(short volatile *__x0, short __x1,
short __x2 , ...);