synchronize with frama-c master

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

@@ -8889,9 +8889,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
       if (cmsg->cmsg_type == 29) {
         struct timeval tv;
         struct timespec ts;
-        unsigned char *tmp_0;
-        tmp_0 = CMSG_DATA(cmsg);
-        memcpy((void *)(& tv),(void const *)tmp_0,sizeof(tv));
+        memcpy((void *)(& tv),(void const *)(cmsg + 1),sizeof(tv));
         UTI_TimevalToTimespec(& tv,& ts);
         LCL_CookTime(& ts,& local_ts.ts,& local_ts.err);
         local_ts.source = NTP_TS_KERNEL;
@@ -8899,9 +8897,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
     if (cmsg->cmsg_level == 1) 
       if (cmsg->cmsg_type == 35) {
         struct timespec ts_0;
-        unsigned char *tmp_1;
-        tmp_1 = CMSG_DATA(cmsg);
-        memcpy((void *)(& ts_0),(void const *)tmp_1,sizeof(ts_0));
+        memcpy((void *)(& ts_0),(void const *)(cmsg + 1),sizeof(ts_0));
         LCL_CookTime(& ts_0,& local_ts.ts,& local_ts.err);
         local_ts.source = NTP_TS_KERNEL;
       }

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

@@ -313,15 +313,15 @@ Potential entry points (114)
 
 Global metrics
 ============== 
-Sloc = 10451
+Sloc = 10449
 Decision point = 1910
 Global variables = 254
 If = 1794
 Loop = 169
 Goto = 485
-Assignment = 4646
+Assignment = 4644
 Exit point = 521
 Function = 542
-Function call = 2132
+Function call = 2130
 Pointer dereferencing = 2774
 Cyclomatic complexity = 2431

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

@@ -8703,9 +8703,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
       if (cmsg->cmsg_type == 29) {
         struct timeval tv;
         struct timespec ts;
-        unsigned char *tmp_0;
-        tmp_0 = CMSG_DATA(cmsg);
-        memcpy((void *)(& tv),(void const *)tmp_0,sizeof(tv));
+        memcpy((void *)(& tv),(void const *)(cmsg + 1),sizeof(tv));
         UTI_TimevalToTimespec(& tv,& ts);
         LCL_CookTime(& ts,& local_ts.ts,& local_ts.err);
         local_ts.source = NTP_TS_KERNEL;
@@ -8713,9 +8711,7 @@ static void process_message(struct msghdr *hdr, int length, int sock_fd)
     if (cmsg->cmsg_level == 1) 
       if (cmsg->cmsg_type == 35) {
         struct timespec ts_0;
-        unsigned char *tmp_1;
-        tmp_1 = CMSG_DATA(cmsg);
-        memcpy((void *)(& ts_0),(void const *)tmp_1,sizeof(ts_0));
+        memcpy((void *)(& ts_0),(void const *)(cmsg + 1),sizeof(ts_0));
         LCL_CookTime(& ts_0,& local_ts.ts,& local_ts.err);
         local_ts.source = NTP_TS_KERNEL;
       }

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

@@ -292,15 +292,15 @@ Potential entry points (161)
 
 Global metrics
 ============== 
-Sloc = 8290
+Sloc = 8288
 Decision point = 1426
 Global variables = 241
 If = 1367
 Loop = 162
 Goto = 410
-Assignment = 3758
+Assignment = 3756
 Exit point = 458
 Function = 474
-Function call = 1680
+Function call = 1678
 Pointer dereferencing = 2054
 Cyclomatic complexity = 1884

frama-c @ a3e88edb

-Subproject commit 7af05e7691d839abb8673a8be4ae9921753e8941
+Subproject commit a3e88edb939d0ded0a02bba53e441bcedd61f1fe

gzip124/.frama-c/gzip124.eva/alarms.csv

@@ -552,7 +552,7 @@ directory	file	line	function	property kind	status	property
 .	zip.c	111	file_read	precondition of read	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
 .	zip.c	111	file_read	precondition of read	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	ctype.h	174	isupper	precondition	Unknown	c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
-FRAMAC_SHARE/libc	fcntl.h	168	__va_open_mode_t	precondition	Unknown	valid_filename: valid_read_string(filename)
+FRAMAC_SHARE/libc	fcntl.h	175	__va_open_mode_t	precondition	Unknown	valid_filename: valid_read_string(filename)
 FRAMAC_SHARE/libc	stdio.h	207	fprintf_va_1	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	207	fprintf_va_11	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	207	fprintf_va_12	precondition	Unknown	valid_read_string(param0)

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

 util.c:186:[eva:garbled-mix] warning: The specification of function strrchr has generated a garbled mix for assigns clause \result.
 util.c:400:[eva] warning: ignoring unsupported allocates clause
-FRAMAC_SHARE/libc/signal.h:122:[eva] warning: no 'assigns \result \from ...' clause specified for function signal
+FRAMAC_SHARE/libc/signal.h:123:[eva] warning: no 'assigns \result \from ...' clause specified for function signal
 inflate.c:403:[eva] warning: ignoring unsupported allocates clause
 inflate.c:412:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: huft_build :: inflate.c:763 <-

hiredis/.frama-c/hiredis-misc.eva/alarms.csv

@@ -335,5 +335,5 @@ FRAMAC_SHARE/libc	string.h	528	strerror_r	from clause	Unknown	assigns *(strerrbu
 FRAMAC_SHARE/libc	string.h	528	strerror_r	from clause	Unknown	assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
 FRAMAC_SHARE/libc	strings.h	53	strncasecmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
 FRAMAC_SHARE/libc	unistd.h	725	access	precondition	Unknown	valid_string_path: valid_read_string(path)
-FRAMAC_SHARE/libc/sys	socket.h	334	connect	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
-FRAMAC_SHARE/libc/sys	socket.h	540	setsockopt	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	335	connect	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	541	setsockopt	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024

kilo/.frama-c/kilo.eva/alarms.csv

@@ -556,7 +556,7 @@ directory	file	line	function	property kind	status	property
 FRAMAC_SHARE/libc	ctype.h	94	isdigit	precondition	Unknown	c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
 FRAMAC_SHARE/libc	ctype.h	134	isprint	precondition	Unknown	c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
 FRAMAC_SHARE/libc	ctype.h	161	isspace	precondition	Unknown	c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
-FRAMAC_SHARE/libc	fcntl.h	168	__va_open_mode_t	precondition	Unknown	valid_filename: valid_read_string(filename)
+FRAMAC_SHARE/libc	fcntl.h	175	__va_open_mode_t	precondition	Unknown	valid_filename: valid_read_string(filename)
 FRAMAC_SHARE/libc	stdio.c	90	getline	mem_access	Unknown	\valid(*lineptr + tmp_2)
 FRAMAC_SHARE/libc	stdio.c	93	getline	mem_access	Unknown	\valid(*lineptr + cur)
 FRAMAC_SHARE/libc	stdio.h	213	snprintf_va_4	precondition	Unknown	valid_read_nstring(param0, 20)

libmodbus/.frama-c/libmodbus-random-client.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc/sys	socket.h	437	recv	precondition	Unknown	valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
+FRAMAC_SHARE/libc/sys	socket.h	438	recv	precondition	Unknown	valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
 src	modbus-tcp.c	180	_modbus_tcp_recv	precondition of recv	Unknown	valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
 src	modbus-tcp.c	202	_modbus_tcp_pre_check_confirmation	initialization	Unknown	\initialized(rsp + 2)
 src	modbus-tcp.c	202	_modbus_tcp_pre_check_confirmation	initialization	Unknown	\initialized(rsp + 3)

libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv

@@ -7,10 +7,10 @@ FRAMAC_SHARE/libc	string.h	96	memcpy	precondition	Unknown	valid_src: valid_read_
 FRAMAC_SHARE/libc	time.h	298	nanosleep	precondition	Unknown	valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
 FRAMAC_SHARE/libc	unistd.h	1008	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
 FRAMAC_SHARE/libc	unistd.h	1153	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
-FRAMAC_SHARE/libc/sys	socket.h	301	accept	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
-FRAMAC_SHARE/libc/sys	socket.h	436	recv	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
-FRAMAC_SHARE/libc/sys	socket.h	437	recv	precondition	Unknown	valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
-FRAMAC_SHARE/libc/sys	socket.h	493	send	precondition	Unknown	buf_len_ok: \valid_read((char *)buf + (0 .. len - 1))
+FRAMAC_SHARE/libc/sys	socket.h	302	accept	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	437	recv	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	438	recv	precondition	Unknown	valid_buffer_length: \valid((char *)buf + (0 .. len - 1))
+FRAMAC_SHARE/libc/sys	socket.h	494	send	precondition	Unknown	buf_len_ok: \valid_read((char *)buf + (0 .. len - 1))
 src	modbus-data.c	89	modbus_set_bits_from_bytes	initialization	Unknown	\initialized(tab_byte + (unsigned int)((unsigned int)(i - (unsigned int)idx) / 8))
 src	modbus-data.c	89	modbus_set_bits_from_bytes	mem_access	Unknown	\valid(dest + i)
 src	modbus-data.c	89	modbus_set_bits_from_bytes	mem_access	Unknown	\valid_read(tab_byte + (unsigned int)((unsigned int)(i - (unsigned int)idx) / 8))

microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	fcntl.h	160	__va_open_void	precondition	Unknown	valid_filename: valid_read_string(filename)
+FRAMAC_SHARE/libc	fcntl.h	167	__va_open_void	precondition	Unknown	valid_filename: valid_read_string(filename)
 FRAMAC_SHARE/libc	stdio.h	211	printf_va_154	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	211	printf_va_155	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	211	printf_va_156	precondition	Unknown	valid_read_string(param0)

polarssl/.frama-c/polarssl-server.eva/alarms.csv

@@ -44,8 +44,8 @@ FRAMAC_SHARE/libc	unistd.h	1007	read	precondition	Unknown	valid_fd: 0 ≤ fd < 1
 FRAMAC_SHARE/libc	unistd.h	1008	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
 FRAMAC_SHARE/libc	unistd.h	1152	write	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1153	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
-FRAMAC_SHARE/libc/sys	socket.h	301	accept	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
-FRAMAC_SHARE/libc/sys	socket.h	551	shutdown	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	302	accept	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
+FRAMAC_SHARE/libc/sys	socket.h	552	shutdown	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024
 library	ctr_drbg.c	154	block_cipher_df	mem_access	Unknown	\valid_read(p + i)
 library	des.c	384	des_setkey	postcondition	Unknown	\initialized(\old(SK) + (0 .. 31))
 library	dhm.c	210	dhm_read_public	signed_overflow	Unknown	-2147483648 ≤ (int)(-0x3200) + ret