[Libc] add spec for GCC builtin __sync_synchronize

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

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

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

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;
 
 */

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 , ...);