2048/.frama-c/2048.eva/metrics.log

@@ -11,7 +11,7 @@ Unreached functions (1) =
 Function main references signal_callback_handler (at 2048.c:383)
 [metrics] Statements analyzed by Eva
 --------------------------
-329 stmts in analyzed functions, 326 stmts analyzed (99.1%)
+328 stmts in analyzed functions, 325 stmts analyzed (99.1%)
 addRandom: 32 stmts out of 32 (100.0%)
 countEmpty: 16 stmts out of 16 (100.0%)
 drawBoard: 51 stmts out of 51 (100.0%)
@@ -19,7 +19,7 @@ findPairDown: 19 stmts out of 19 (100.0%)
 gameEnded: 20 stmts out of 20 (100.0%)
 getColor: 20 stmts out of 20 (100.0%)
 initBoard: 18 stmts out of 18 (100.0%)
-main: 48 stmts out of 48 (100.0%)
+main: 47 stmts out of 47 (100.0%)
 moveDown: 6 stmts out of 6 (100.0%)
 moveLeft: 6 stmts out of 6 (100.0%)
 moveRight: 6 stmts out of 6 (100.0%)

2048/.frama-c/2048.parse/framac.ast

@@ -1127,50 +1127,48 @@ int main(int argc, char **argv)
   initBoard(board);
   setBufferedInput((_Bool)0);
   while (1) {
-    {
-      int tmp;
-      tmp = getchar();
-      c = (char)tmp;
-      switch ((int)c) {
-        case 97: case 104: case 68: success = moveLeft(board);
-        break;
-        case 100: case 108: case 67: success = moveRight(board);
-        break;
-        case 119: case 107: case 65: success = moveUp(board);
-        break;
-        case 115: case 106: case 66: success = moveDown(board);
+    int tmp;
+    tmp = getchar();
+    c = (char)tmp;
+    switch ((int)c) {
+      case 97: case 104: case 68: success = moveLeft(board);
+      break;
+      case 100: case 108: case 67: success = moveRight(board);
+      break;
+      case 119: case 107: case 65: success = moveUp(board);
+      break;
+      case 115: case 106: case 66: success = moveDown(board);
+      break;
+      default: success = (_Bool)0;
+    }
+    if (success) {
+      _Bool tmp_0;
+      drawBoard(board);
+      usleep((useconds_t)150000);
+      addRandom(board);
+      drawBoard(board);
+      tmp_0 = gameEnded(board);
+      if (tmp_0) {
+        printf("         GAME OVER          \n"); /* printf_va_31 */
         break;
-        default: success = (_Bool)0;
-      }
-      if (success) {
-        _Bool tmp_0;
-        drawBoard(board);
-        usleep((useconds_t)150000);
-        addRandom(board);
-        drawBoard(board);
-        tmp_0 = gameEnded(board);
-        if (tmp_0) {
-          printf("         GAME OVER          \n"); /* printf_va_31 */
-          break;
-        }
-      }
-      if ((int)c == 'q') {
-        int tmp_1;
-        printf("        QUIT? (y/n)         \n"); /* printf_va_32 */
-        tmp_1 = getchar();
-        c = (char)tmp_1;
-        if ((int)c == 'y') break;
-        drawBoard(board);
-      }
-      if ((int)c == 'r') {
-        int tmp_2;
-        printf("       RESTART? (y/n)       \n"); /* printf_va_33 */
-        tmp_2 = getchar();
-        c = (char)tmp_2;
-        if ((int)c == 'y') initBoard(board);
-        drawBoard(board);
       }
     }
+    if ((int)c == 'q') {
+      int tmp_1;
+      printf("        QUIT? (y/n)         \n"); /* printf_va_32 */
+      tmp_1 = getchar();
+      c = (char)tmp_1;
+      if ((int)c == 'y') break;
+      drawBoard(board);
+    }
+    if ((int)c == 'r') {
+      int tmp_2;
+      printf("       RESTART? (y/n)       \n"); /* printf_va_33 */
+      tmp_2 = getchar();
+      c = (char)tmp_2;
+      if ((int)c == 'y') initBoard(board);
+      drawBoard(board);
+    }
   }
   setBufferedInput((_Bool)1);
   printf("\033[?25h\033[m"); /* printf_va_34 */

2048/.frama-c/2048.parse/metrics.log

@@ -26,7 +26,7 @@ Potential entry points (2)
 
 Global metrics
 ============== 
-Sloc = 399
+Sloc = 398
 Decision point = 61
 Global variables = 5
 If = 57

c-testsuite/.frama-c/00034.eva/metrics.log

@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-25 stmts in analyzed functions, 25 stmts analyzed (100.0%)
-main: 25 stmts out of 25 (100.0%)
+24 stmts in analyzed functions, 24 stmts analyzed (100.0%)
+main: 24 stmts out of 24 (100.0%)

c-testsuite/.frama-c/00034.parse/framac.ast

@@ -5,8 +5,7 @@ int main(void)
   int x;
   x = 0;
   while (1) break;
-  while (1) {
-    if (x == 5) break;
+  while (! (x == 5)) {
     x ++;
     continue;
   }

c-testsuite/.frama-c/00034.parse/metrics.log

@@ -20,7 +20,7 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 25
+Sloc = 24
 Decision point = 3
 Global variables = 0
 If = 3

chrony/.frama-c/chrony-ntp-core.eva/metrics.log

@@ -74,7 +74,7 @@ Function update_leap_status calls LCL_SetSystemLeap (at reference.c:807)
 Function write_log calls UTI_RefidToString (at reference.c:860)
 [metrics] Statements analyzed by Eva
 --------------------------
-7608 stmts in analyzed functions, 6647 stmts analyzed (87.4%)
+7606 stmts in analyzed functions, 6646 stmts analyzed (87.4%)
 ADF_Allow: 2 stmts out of 2 (100.0%)
 ADF_AllowAll: 2 stmts out of 2 (100.0%)
 ADF_CreateTable: 6 stmts out of 6 (100.0%)
@@ -383,13 +383,13 @@ CNF_GetBindAddress: 3 stmts out of 6 (50.0%)
 NCR_ProcessTxUnknown: 12 stmts out of 24 (50.0%)
 source_to_string: 6 stmts out of 12 (50.0%)
 NCR_SetConnectivity: 20 stmts out of 47 (42.6%)
-check_packet_auth: 19 stmts out of 55 (34.5%)
 CLG_LogNTPAccess: 7 stmts out of 21 (33.3%)
 LCL_ReadRawTime: 3 stmts out of 9 (33.3%)
+check_packet_auth: 18 stmts out of 54 (33.3%)
 generate_ntp_auth: 1 stmts out of 3 (33.3%)
 UTI_SockaddrFamilyToString: 4 stmts out of 17 (23.5%)
 handle_slew_0: 3 stmts out of 20 (15.0%)
-get_record: 6 stmts out of 81 (7.4%)
+get_record: 6 stmts out of 80 (7.5%)
 special_mode_sync: 3 stmts out of 57 (5.3%)
 SCH_AddTimeout: 0 stmts out of 23 (0.0%)
 Transform: 0 stmts out of 265 (0.0%)

chrony/.frama-c/chrony-ntp-core.parse/framac.ast

@@ -706,9 +706,8 @@ extern void LOG_Initialise(void);
 extern void LOG_Finalise(void);
-extern void ( /* format attribute */ LOG_Message)(LOG_Severity severity,
-                                                  char const *format,
-                                                  void * const *__va_params);
+extern void LOG_Message(LOG_Severity severity, char const *format,
+                        void * const *__va_params);
 extern void LOG_SetDebugLevel(int level);
@@ -716,9 +715,8 @@ extern void LOG_OpenFileLog(char const *log_file);
 extern LOG_FileID LOG_FileOpen(char const *name, char const *banner);
-extern void ( /* format attribute */ LOG_FileWrite)(LOG_FileID id,
-                                                    char const *format,
-                                                    void * const *__va_params);
+extern void LOG_FileWrite(LOG_FileID id, char const *format,
+                          void * const *__va_params);
 void lcl_InvokeDispersionNotifyHandlers(double dispersion);
@@ -1856,51 +1854,49 @@ static Record *get_record(IPAddr *ip)
         goto return_label;
       }
   while (1) {
-    {
-      uint32_t tmp;
-      int tmp_3;
-      tmp = UTI_IPToHash(ip);
-      first = (tmp % slots) * (1U << 4);
-      i = (unsigned int)0;
-      oldest_record = (Record *)0;
-      while (i < 1U << 4) {
-        {
-          int tmp_0;
-          int tmp_1;
-          record = (Record *)ARR_GetElement(records,first + i);
-          tmp_0 = UTI_CompareIPs(ip,& record->ip_addr,(IPAddr *)0);
-          if (! tmp_0) {
-            __retres = record;
-            goto return_label;
-          }
-          if ((int)record->ip_addr.family == 0) break;
-          tmp_1 = compare_ts(record->last_ntp_hit,record->last_cmd_hit);
-          if (tmp_1 > 0) last_hit = (time_t)record->last_ntp_hit;
-          else last_hit = (time_t)record->last_cmd_hit;
-          if (! oldest_record) goto _LOR;
-          else {
-            int tmp_2;
-            tmp_2 = compare_ts((uint32_t)oldest_hit,(uint32_t)last_hit);
-            if (tmp_2 > 0) goto _LOR;
-            else 
-              if (oldest_hit == last_hit) 
-                if (record->ntp_hits + record->cmd_hits < oldest_record->ntp_hits + oldest_record->cmd_hits) {
-                  _LOR: {
-                          oldest_record = record;
-                          oldest_hit = last_hit;
-                        }
-                }
-          }
+    uint32_t tmp;
+    int tmp_3;
+    tmp = UTI_IPToHash(ip);
+    first = (tmp % slots) * (1U << 4);
+    i = (unsigned int)0;
+    oldest_record = (Record *)0;
+    while (i < 1U << 4) {
+      {
+        int tmp_0;
+        int tmp_1;
+        record = (Record *)ARR_GetElement(records,first + i);
+        tmp_0 = UTI_CompareIPs(ip,& record->ip_addr,(IPAddr *)0);
+        if (! tmp_0) {
+          __retres = record;
+          goto return_label;
+        }
+        if ((int)record->ip_addr.family == 0) break;
+        tmp_1 = compare_ts(record->last_ntp_hit,record->last_cmd_hit);
+        if (tmp_1 > 0) last_hit = (time_t)record->last_ntp_hit;
+        else last_hit = (time_t)record->last_cmd_hit;
+        if (! oldest_record) goto _LOR;
+        else {
+          int tmp_2;
+          tmp_2 = compare_ts((uint32_t)oldest_hit,(uint32_t)last_hit);
+          if (tmp_2 > 0) goto _LOR;
+          else 
+            if (oldest_hit == last_hit) 
+              if (record->ntp_hits + record->cmd_hits < oldest_record->ntp_hits + oldest_record->cmd_hits) {
+                _LOR: {
+                        oldest_record = record;
+                        oldest_hit = last_hit;
+                      }
+              }
         }
-        i ++;
       }
-      if ((int)record->ip_addr.family == 0) break;
-      tmp_3 = expand_hashtable();
-      if (tmp_3) continue;
-      record = oldest_record;
-      total_record_drops ++;
-      break;
+      i ++;
     }
+    if ((int)record->ip_addr.family == 0) break;
+    tmp_3 = expand_hashtable();
+    if (tmp_3) continue;
+    record = oldest_record;
+    total_record_drops ++;
+    break;
   }
   record->ip_addr = *ip;
   tmp_4 = (uint32_t)0;
@@ -15605,49 +15601,47 @@ int UTI_CreateDirAndParents(char const *path, mode_t mode_0, uid_t uid,
   k = 0;
   i = k;
   while (1) {
-    {
-      int tmp_2;
-      int tmp_3;
-      tmp_2 = i;
-      i ++;
-      tmp_3 = k;
-      k ++;
-      *(p + tmp_2) = *(path + tmp_3);
-      if ((int)*(path + k) == '/') goto _LOR;
-      else 
-        if (! *(path + k)) {
-          _LOR:
-          {
-            int tmp_7;
-            gid_t tmp_4;
-            uid_t tmp_5;
-            mode_t tmp_6;
-            last = 1;
-            j = k;
-            while (*(path + j)) {
-              if ((int)*(path + j) != '/') {
-                k = j - 1;
-                last = 0;
-                break;
-              }
-              j ++;
-            }
-            *(p + i) = (char)0;
-            if (last) tmp_4 = gid; else tmp_4 = (gid_t)0;
-            if (last) tmp_5 = uid; else tmp_5 = (uid_t)0;
-            if (last) tmp_6 = mode_0; else tmp_6 = (mode_t)0755;
-            ;
-            tmp_7 = create_dir(p,tmp_6,tmp_5,tmp_4);
-            if (! tmp_7) {
-              free((void *)p);
-              __retres = 0;
-              goto return_label;
+    int tmp_2;
+    int tmp_3;
+    tmp_2 = i;
+    i ++;
+    tmp_3 = k;
+    k ++;
+    *(p + tmp_2) = *(path + tmp_3);
+    if ((int)*(path + k) == '/') goto _LOR;
+    else 
+      if (! *(path + k)) {
+        _LOR:
+        {
+          int tmp_7;
+          gid_t tmp_4;
+          uid_t tmp_5;
+          mode_t tmp_6;
+          last = 1;
+          j = k;
+          while (*(path + j)) {
+            if ((int)*(path + j) != '/') {
+              k = j - 1;
+              last = 0;
+              break;
             }
-            if (last) break;
+            j ++;
           }
+          *(p + i) = (char)0;
+          if (last) tmp_4 = gid; else tmp_4 = (gid_t)0;
+          if (last) tmp_5 = uid; else tmp_5 = (uid_t)0;
+          if (last) tmp_6 = mode_0; else tmp_6 = (mode_t)0755;
+          ;
+          tmp_7 = create_dir(p,tmp_6,tmp_5,tmp_4);
+          if (! tmp_7) {
+            free((void *)p);
+            __retres = 0;
+            goto return_label;
+          }
+          if (last) break;
         }
-      if (! *(path + k)) break;
-    }
+      }
+    if (! *(path + k)) break;
   }
   free((void *)p);
   __retres = 1;

chrony/.frama-c/chrony-ntp-core.parse/metrics.log

@@ -313,7 +313,7 @@ Potential entry points (114)
 
 Global metrics
 ============== 
-Sloc = 10449
+Sloc = 10445
 Decision point = 1910
 Global variables = 254
 If = 1794

chrony/.frama-c/chrony-regress.parse/framac.ast

@@ -596,9 +596,8 @@ extern void LOG_Initialise(void);
 
 extern void LOG_Finalise(void);
 
-extern void ( /* format attribute */ LOG_Message)(LOG_Severity severity,
-                                                  char const *format,
-                                                  void * const *__va_params);
+extern void LOG_Message(LOG_Severity severity, char const *format,
+                        void * const *__va_params);
 
 extern void LOG_SetDebugLevel(int level);
 
@@ -606,9 +605,8 @@ extern void LOG_OpenFileLog(char const *log_file);
 
 extern LOG_FileID LOG_FileOpen(char const *name, char const *banner);
 
-extern void ( /* format attribute */ LOG_FileWrite)(LOG_FileID id,
-                                                    char const *format,
-                                                    void * const *__va_params);
+extern void LOG_FileWrite(LOG_FileID id, char const *format,
+                          void * const *__va_params);
 
 void lcl_InvokeDispersionNotifyHandlers(double dispersion);
 
@@ -1746,51 +1744,49 @@ static Record *get_record(IPAddr *ip)
         goto return_label;
       }
   while (1) {
-    {
-      uint32_t tmp;
-      int tmp_3;
-      tmp = UTI_IPToHash(ip);
-      first = (tmp % slots) * (1U << 4);
-      i = (unsigned int)0;
-      oldest_record = (Record *)0;
-      while (i < 1U << 4) {
-        {
-          int tmp_0;
-          int tmp_1;
-          record = (Record *)ARR_GetElement(records,first + i);
-          tmp_0 = UTI_CompareIPs(ip,& record->ip_addr,(IPAddr *)0);
-          if (! tmp_0) {
-            __retres = record;
-            goto return_label;
-          }
-          if ((int)record->ip_addr.family == 0) break;
-          tmp_1 = compare_ts(record->last_ntp_hit,record->last_cmd_hit);
-          if (tmp_1 > 0) last_hit = (time_t)record->last_ntp_hit;
-          else last_hit = (time_t)record->last_cmd_hit;
-          if (! oldest_record) goto _LOR;
-          else {
-            int tmp_2;
-            tmp_2 = compare_ts((uint32_t)oldest_hit,(uint32_t)last_hit);
-            if (tmp_2 > 0) goto _LOR;
-            else 
-              if (oldest_hit == last_hit) 
-                if (record->ntp_hits + record->cmd_hits < oldest_record->ntp_hits + oldest_record->cmd_hits) {
-                  _LOR: {
-                          oldest_record = record;
-                          oldest_hit = last_hit;
-                        }
-                }
-          }
+    uint32_t tmp;
+    int tmp_3;
+    tmp = UTI_IPToHash(ip);
+    first = (tmp % slots) * (1U << 4);
+    i = (unsigned int)0;
+    oldest_record = (Record *)0;
+    while (i < 1U << 4) {
+      {
+        int tmp_0;
+        int tmp_1;
+        record = (Record *)ARR_GetElement(records,first + i);
+        tmp_0 = UTI_CompareIPs(ip,& record->ip_addr,(IPAddr *)0);
+        if (! tmp_0) {
+          __retres = record;
+          goto return_label;
+        }
+        if ((int)record->ip_addr.family == 0) break;
+        tmp_1 = compare_ts(record->last_ntp_hit,record->last_cmd_hit);
+        if (tmp_1 > 0) last_hit = (time_t)record->last_ntp_hit;
+        else last_hit = (time_t)record->last_cmd_hit;
+        if (! oldest_record) goto _LOR;
+        else {
+          int tmp_2;
+          tmp_2 = compare_ts((uint32_t)oldest_hit,(uint32_t)last_hit);
+          if (tmp_2 > 0) goto _LOR;
+          else 
+            if (oldest_hit == last_hit) 
+              if (record->ntp_hits + record->cmd_hits < oldest_record->ntp_hits + oldest_record->cmd_hits) {
+                _LOR: {
+                        oldest_record = record;
+                        oldest_hit = last_hit;
+                      }
+              }
         }
-        i ++;
       }
-      if ((int)record->ip_addr.family == 0) break;
-      tmp_3 = expand_hashtable();
-      if (tmp_3) continue;
-      record = oldest_record;
-      total_record_drops ++;
-      break;
+      i ++;
     }
+    if ((int)record->ip_addr.family == 0) break;
+    tmp_3 = expand_hashtable();
+    if (tmp_3) continue;
+    record = oldest_record;
+    total_record_drops ++;
+    break;
   }
   record->ip_addr = *ip;
   tmp_4 = (uint32_t)0;
@@ -14632,49 +14628,47 @@ int UTI_CreateDirAndParents(char const *path, mode_t mode_0, uid_t uid,
   k = 0;
   i = k;
   while (1) {
-    {
-      int tmp_2;
-      int tmp_3;
-      tmp_2 = i;
-      i ++;
-      tmp_3 = k;
-      k ++;
-      *(p + tmp_2) = *(path + tmp_3);
-      if ((int)*(path + k) == '/') goto _LOR;
-      else 
-        if (! *(path + k)) {
-          _LOR:
-          {
-            int tmp_7;
-            gid_t tmp_4;
-            uid_t tmp_5;
-            mode_t tmp_6;
-            last = 1;
-            j = k;
-            while (*(path + j)) {
-              if ((int)*(path + j) != '/') {
-                k = j - 1;
-                last = 0;
-                break;
-              }
-              j ++;
-            }
-            *(p + i) = (char)0;
-            if (last) tmp_4 = gid; else tmp_4 = (gid_t)0;
-            if (last) tmp_5 = uid; else tmp_5 = (uid_t)0;
-            if (last) tmp_6 = mode_0; else tmp_6 = (mode_t)0755;
-            ;
-            tmp_7 = create_dir(p,tmp_6,tmp_5,tmp_4);
-            if (! tmp_7) {
-              free((void *)p);
-              __retres = 0;
-              goto return_label;
+    int tmp_2;
+    int tmp_3;
+    tmp_2 = i;
+    i ++;
+    tmp_3 = k;
+    k ++;
+    *(p + tmp_2) = *(path + tmp_3);
+    if ((int)*(path + k) == '/') goto _LOR;
+    else 
+      if (! *(path + k)) {
+        _LOR:
+        {
+          int tmp_7;
+          gid_t tmp_4;
+          uid_t tmp_5;
+          mode_t tmp_6;
+          last = 1;
+          j = k;
+          while (*(path + j)) {
+            if ((int)*(path + j) != '/') {
+              k = j - 1;
+              last = 0;
+              break;
             }
-            if (last) break;
+            j ++;
           }
+          *(p + i) = (char)0;
+          if (last) tmp_4 = gid; else tmp_4 = (gid_t)0;
+          if (last) tmp_5 = uid; else tmp_5 = (uid_t)0;
+          if (last) tmp_6 = mode_0; else tmp_6 = (mode_t)0755;
+          ;
+          tmp_7 = create_dir(p,tmp_6,tmp_5,tmp_4);
+          if (! tmp_7) {
+            free((void *)p);
+            __retres = 0;
+            goto return_label;
+          }
+          if (last) break;
         }
-      if (! *(path + k)) break;
-    }
+      }
+    if (! *(path + k)) break;
   }
   free((void *)p);
   __retres = 1;

chrony/.frama-c/chrony-regress.parse/metrics.log

@@ -292,7 +292,7 @@ Potential entry points (161)
 
 Global metrics
 ============== 
-Sloc = 8288
+Sloc = 8285
 Decision point = 1426
 Global variables = 241
 If = 1367

debie1/.frama-c/debie1.parse/metrics.log

@@ -100,7 +100,7 @@ Potential entry points (8)
 
 Global metrics
 ============== 
-Sloc = 3346
+Sloc = 3342
 Decision point = 418
 Global variables = 104
 If = 311

frama-c @ 5d71cbfe

-Subproject commit d933d7a3ed16c9b356320776ad4e0e16050651ae
+Subproject commit 5d71cbfe9b425c6775d305846edc91ea6933ce95

gzip124/.frama-c/gzip124.eva/warnings.log

 util.c:311:[eva] warning: calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
-FRAMAC_SHARE/libc/signal.h:134:[eva:assigns:missing-result] warning: no 'assigns \result \from ...' clause specified for function signal
 gzip.c:675:[eva:locals-escaping] warning: locals {attr} escaping the scope of zip through file_type
 gzip.c:817:[eva:locals-escaping] warning: locals {attr} escaping the scope of zip through file_type
 [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:

gzip124/.frama-c/gzip124.parse/warnings.log

 getopt.c:362:[kernel:typing:no-proto] warning: Calling function getenv that is declared without prototype.
-Its formals will be inferred from actual arguments
+Its formals will be inferred from actual arguments.
+Declare it as getenv(void) if the function does not take any parameters.
 gzip.c:448:[kernel:typing:incompatible-types-call] warning: implicit conversion between incompatible function types:
 void (*)(void)
 and

hiredis/.frama-c/hiredis-format.eva/metrics.log

@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
 ------------------------------------
 [metrics] Statements analyzed by Eva
 --------------------------
-1373 stmts in analyzed functions, 1279 stmts analyzed (93.2%)
+1372 stmts in analyzed functions, 1278 stmts analyzed (93.1%)
 bulklen: 5 stmts out of 5 (100.0%)
 countDigits: 21 stmts out of 21 (100.0%)
 eva_main: 13 stmts out of 13 (100.0%)
@@ -29,7 +29,7 @@ main: 74 stmts out of 75 (98.7%)
 redisvFormatCommand: 237 stmts out of 244 (97.1%)
 redisFormatSdsCommandArgv: 52 stmts out of 55 (94.5%)
 redisFormatCommandArgv: 50 stmts out of 53 (94.3%)
-sdscatvprintf: 26 stmts out of 31 (83.9%)
+sdscatvprintf: 25 stmts out of 30 (83.3%)
 sdsull2str: 18 stmts out of 24 (75.0%)
 sdsHdrSize: 13 stmts out of 18 (72.2%)
 sdscatfmt: 73 stmts out of 102 (71.6%)

hiredis/.frama-c/hiredis-format.parse/framac.ast

@@ -495,8 +495,7 @@ sds sdscpy(sds s, char const *t);
 
 sds sdscatvprintf(sds s, char const *fmt, va_list ap);
 
-sds ( /* format attribute */ sdscatprintf)(sds s, char const *fmt,
-                                           void * const *__va_params);
+sds sdscatprintf(sds s, char const *fmt, void * const *__va_params);
 
 sds sdscatfmt(sds s, char const *fmt, void * const *__va_params);
 
@@ -6437,8 +6436,7 @@ sds sdscatvprintf(sds s, char const *fmt, va_list ap)
   return_label: return __retres;
 }
 
-sds ( /* format attribute */ sdscatprintf)(sds s, char const *fmt,
-                                           void * const *__va_params)
+sds sdscatprintf(sds s, char const *fmt, void * const *__va_params)
 {
   va_list ap;
   char *t;

hiredis/.frama-c/hiredis-format.parse/metrics.log

@@ -154,7 +154,7 @@ Potential entry points (94)
 
 Global metrics
 ============== 
-Sloc = 6240
+Sloc = 6234
 Decision point = 1175
 Global variables = 8
 If = 919

hiredis/.frama-c/hiredis-misc.parse/framac.ast

@@ -495,8 +495,7 @@ sds sdscpy(sds s, char const *t);
 
 sds sdscatvprintf(sds s, char const *fmt, va_list ap);
 
-sds ( /* format attribute */ sdscatprintf)(sds s, char const *fmt,
-                                           void * const *__va_params);
+sds sdscatprintf(sds s, char const *fmt, void * const *__va_params);
 
 sds sdscatfmt(sds s, char const *fmt, void * const *__va_params);
 
@@ -6437,8 +6436,7 @@ sds sdscatvprintf(sds s, char const *fmt, va_list ap)
   return_label: return __retres;
 }
 
-sds ( /* format attribute */ sdscatprintf)(sds s, char const *fmt,
-                                           void * const *__va_params)
+sds sdscatprintf(sds s, char const *fmt, void * const *__va_params)
 {
   va_list ap;
   char *t;

hiredis/.frama-c/hiredis-misc.parse/metrics.log

@@ -154,7 +154,7 @@ Potential entry points (92)
 
 Global metrics
 ============== 
-Sloc = 6242
+Sloc = 6236
 Decision point = 1175
 Global variables = 8
 If = 919