sync with frama-c master

chrony/chrony-ntp-core.eva/alarms.csv

@@ -840,12 +840,12 @@ directory	file	line	function	property kind	status	property
 .	util.c	1213	UTI_GetRandomBytesUrandom	precondition of fread	Unknown	valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1))
 FRAMAC_SHARE/libc	__fc_inet.h	358	inet_addr	precondition	Unknown	valid_arg: valid_read_string(arg)
 FRAMAC_SHARE/libc	assert.h	31	__FC_assert	precondition	Invalid or unreachable	nonnull_c: c ≢ 0
-FRAMAC_SHARE/libc	math.h	372	exp	precondition	Unknown	finite_domain: x ≤ 0x1.62e42fefa39efp+9
-FRAMAC_SHARE/libc	math.h	409	log	precondition	Unknown	finite_arg: \is_finite(x)
-FRAMAC_SHARE/libc	math.h	410	log	precondition	Unknown	arg_positive: x > 0
-FRAMAC_SHARE/libc	math.h	496	fabs	precondition	Unknown	finite_arg: \is_finite(x)
-FRAMAC_SHARE/libc	math.h	540	sqrt	precondition	Unknown	finite_arg: \is_finite(x)
-FRAMAC_SHARE/libc	math.h	541	sqrt	precondition	Unknown	arg_positive: x ≥ -0.
+FRAMAC_SHARE/libc	math.h	325	exp	precondition	Unknown	finite_domain: x ≤ 0x1.62e42fefa39efp+9
+FRAMAC_SHARE/libc	math.h	362	log	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	363	log	precondition	Unknown	arg_positive: x > 0
+FRAMAC_SHARE/libc	math.h	449	fabs	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	493	sqrt	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	494	sqrt	precondition	Unknown	arg_positive: x ≥ -0.
 FRAMAC_SHARE/libc	netdb.c	113	gethostbyname	mem_access	Unknown	\valid_read(cp)
 FRAMAC_SHARE/libc	netdb.c	116	gethostbyname	mem_access	Unknown	\valid_read(cp)
 FRAMAC_SHARE/libc	netdb.c	119	gethostbyname	precondition of inet_addr	Unknown	valid_arg: valid_read_string(arg)

chrony/chrony-regress.eva/alarms.csv

@@ -94,9 +94,9 @@ directory	file	line	function	property kind	status	property
 .	regress.c	698	RGR_MultipleRegress	precondition of fabs	Unknown	finite_arg: \is_finite(x)
 .	regress.c	698	RGR_MultipleRegress	precondition of fabs	Unknown	finite_arg: \is_finite(x)
 FRAMAC_SHARE/libc	assert.h	31	__FC_assert	precondition	Invalid or unreachable	nonnull_c: c ≢ 0
-FRAMAC_SHARE/libc	math.h	496	fabs	precondition	Unknown	finite_arg: \is_finite(x)
-FRAMAC_SHARE/libc	math.h	540	sqrt	precondition	Unknown	finite_arg: \is_finite(x)
-FRAMAC_SHARE/libc	math.h	541	sqrt	precondition	Unknown	arg_positive: x ≥ -0.
+FRAMAC_SHARE/libc	math.h	449	fabs	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	493	sqrt	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	494	sqrt	precondition	Unknown	arg_positive: x ≥ -0.
 FRAMAC_SHARE/libc	string.h	115	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
 test/unit	regress.c	45	test_unit	initialization	Unknown	\initialized(&x[j])
 test/unit	regress.c	52	test_unit	precondition of fabs	Unknown	finite_arg: \is_finite(x)

frama-c @ 5e840bb7

-Subproject commit c32afcc4038b1234219137cae196f3f776533d2f
+Subproject commit 5e840bb7060585b81d8fc0d76b3627ca2b8d004d

icpc/icpc.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	math.h	372	exp	precondition	Unknown	finite_domain: x ≤ 0x1.62e42fefa39efp+9
-FRAMAC_SHARE/libc	math.h	496	fabs	precondition	Unknown	finite_arg: \is_finite(x)
+FRAMAC_SHARE/libc	math.h	325	exp	precondition	Unknown	finite_domain: x ≤ 0x1.62e42fefa39efp+9
+FRAMAC_SHARE/libc	math.h	449	fabs	precondition	Unknown	finite_arg: \is_finite(x)
 FRAMAC_SHARE/libc	stdio.h	207	fprintf	assigns clause	Unknown	assigns \result, *stream;
 FRAMAC_SHARE/libc	stdio.h	207	fprintf	from clause	Unknown	assigns *stream \from *stream, *(format + (0 ..));
 FRAMAC_SHARE/libc	stdio.h	207	fprintf	from clause	Unknown	assigns \result \from *stream, *(format + (0 ..));

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

@@ -4,7 +4,7 @@ FRAMAC_SHARE/libc	string.c	130	strcmp	mem_access	Unknown	\valid_read(s1 + i)
 FRAMAC_SHARE/libc	string.c	133	strcmp	mem_access	Unknown	\valid_read((unsigned char *)s1 + i)
 FRAMAC_SHARE/libc	string.h	92	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
 FRAMAC_SHARE/libc	string.h	93	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	time.h	270	nanosleep	precondition	Unknown	valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
+FRAMAC_SHARE/libc	time.h	280	nanosleep	precondition	Unknown	valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
 FRAMAC_SHARE/libc	unistd.h	782	close	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1004	read	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1005	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))

papabench/papabench.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-FRAMAC_SHARE/libc	math.h	398	frexpf	assigns clause	Unknown	assigns \result, *exp;
-FRAMAC_SHARE/libc	math.h	398	frexpf	from clause	Unknown	assigns *exp \from *exp, value;
-FRAMAC_SHARE/libc	math.h	398	frexpf	from clause	Unknown	assigns \result \from *exp, value;
-FRAMAC_SHARE/libc	math.h	405	ldexp	assigns clause	Unknown	assigns \nothing;
-FRAMAC_SHARE/libc	math.h	405	ldexp	from clause	Unknown	assigns \result \from x, exp;
+FRAMAC_SHARE/libc	math.h	351	frexpf	assigns clause	Unknown	assigns \result, *exp;
+FRAMAC_SHARE/libc	math.h	351	frexpf	from clause	Unknown	assigns *exp \from *exp, value;
+FRAMAC_SHARE/libc	math.h	351	frexpf	from clause	Unknown	assigns \result \from *exp, value;
+FRAMAC_SHARE/libc	math.h	358	ldexp	assigns clause	Unknown	assigns \nothing;
+FRAMAC_SHARE/libc	math.h	358	ldexp	from clause	Unknown	assigns \result \from x, exp;
 sw/airborne/autopilot	estimator.c	116	estimator_update_state_infrared	is_nan	Unknown	¬\is_NaN(\mul_float(rad_of_ir, (float)ir_roll))
 sw/airborne/autopilot	estimator.c	118	estimator_update_state_infrared	is_nan	Unknown	¬\is_NaN(\mul_float(rad_of_ir, (float)ir_pitch))
 sw/airborne/autopilot	estimator.c	158	estimator_update_ir_estim	is_nan	Unknown	¬\is_NaN(\div_float(estimator_update_ir_estim_sum_xy, estimator_update_ir_estim_sum_xx))