synchronize with frama-c master

frama-c @ 9b464ff0

-Subproject commit d518abcc12ec3caa149c728aea351e509205b1c8
+Subproject commit 9b464ff0d452e265e51da668aa2daee3de212280

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

@@ -63,7 +63,6 @@ src	modbus.c	732	modbus_reply	initialization	Unknown	\initialized(req + (int)(of
 src	modbus.c	732	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 4))
 src	modbus.c	763	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 3))
 src	modbus.c	763	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 4))
-src	modbus.c	784	modbus_reply	mem_access	Unknown	\valid_read(tab_registers + i)
 src	modbus.c	799	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 3))
 src	modbus.c	799	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 4))
 src	modbus.c	803	modbus_reply	precondition of memcpy	Unknown	valid_dest: valid_or_empty(dest, n)
@@ -78,7 +77,6 @@ src	modbus.c	865	modbus_reply	initialization	Unknown	\initialized(req + (int)(of
 src	modbus.c	865	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 4))
 src	modbus.c	884	modbus_reply	initialization	Unknown	\initialized(req + (int)((int)(offset + j) + 1))
 src	modbus.c	884	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + j))
-src	modbus.c	884	modbus_reply	mem_access	Unknown	\valid(mb_mapping->tab_registers + i_0)
 src	modbus.c	928	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 3))
 src	modbus.c	928	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 4))
 src	modbus.c	929	modbus_reply	initialization	Unknown	\initialized(req + (int)(offset + 5))
@@ -97,7 +95,6 @@ src	modbus.c	972	modbus_reply	initialization	Unknown	\initialized(req + (int)(of
 src	modbus.c	972	modbus_reply	mem_access	Unknown	\valid(mb_mapping->tab_registers + i_1)
 src	modbus.c	972	modbus_reply	mem_access	Unknown	\valid_read(req + (int)((int)(offset + j_0) + 1))
 src	modbus.c	972	modbus_reply	mem_access	Unknown	\valid_read(req + (int)(offset + j_0))
-src	modbus.c	977	modbus_reply	mem_access	Unknown	\valid_read(mb_mapping->tab_registers + i_1)
 src	modbus.c	1012	modbus_reply_exception	initialization	Unknown	\initialized(req + (int)(offset - 1))
 src	modbus.c	1013	modbus_reply_exception	initialization	Unknown	\initialized(req + offset)
 tests	unit-test-server.c	44	main	mem_access	Unknown	\valid_read(argv + 1)

libmodbus/.frama-c/libmodbus-unit-server.eva/warnings.log

@@ -16,11 +16,7 @@ stack: modbus_set_bits_from_bytes :: src/modbus.c:854 <-
        main
 src/modbus.c:869:[eva:locals-escaping] warning: locals {__va_args_132} escaping the scope of a block of modbus_reply through S___fc_stderr
 src/modbus.c:875:[eva:locals-escaping] warning: locals {__va_args_136} escaping the scope of a block of modbus_reply through S___fc_stderr
-src/modbus.c:884:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
-stack: modbus_reply :: tests/unit-test-server.c:183 <- main
 src/modbus.c:922:[eva:locals-escaping] warning: locals {__va_args_140} escaping the scope of a block of modbus_reply through S___fc_stderr
 src/modbus.c:949:[eva:locals-escaping] warning: locals {__va_args_149} escaping the scope of a block of modbus_reply through S___fc_stderr
 src/modbus.c:957:[eva:locals-escaping] warning: locals {__va_args_155} escaping the scope of a block of modbus_reply through S___fc_stderr
 src/modbus.c:985:[eva:locals-escaping] warning: locals {__va_args_159} escaping the scope of a block of modbus_reply through S___fc_stderr
-src/modbus.c:972:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
-stack: modbus_reply :: tests/unit-test-server.c:183 <- main