sync with frama-c master

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

@@ -330,7 +330,9 @@ struct __anonstruct_Record_80 {
    NTP_int64 ntp_tx_ts ;
 };
 typedef struct __anonstruct_Record_80 Record;
+struct SST_Stats_Record;
 typedef struct SST_Stats_Record *SST_Stats;
+struct SRC_Instance_Record;
 typedef struct SRC_Instance_Record *SRC_Instance;
 enum __anonenum_SRC_Type_23 {
     SRC_NTP = 0,

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

@@ -292,7 +292,9 @@ struct __anonstruct_Record_80 {
    NTP_int64 ntp_tx_ts ;
 };
 typedef struct __anonstruct_Record_80 Record;
+struct SST_Stats_Record;
 typedef struct SST_Stats_Record *SST_Stats;
+struct SRC_Instance_Record;
 typedef struct SRC_Instance_Record *SRC_Instance;
 enum __anonenum_SRC_Type_23 {
     SRC_NTP = 0,

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

@@ -2,4 +2,5 @@ directory	file	line	function	property kind	status	property
 code	tc_hand.c	1037	UpdateTarget	initialization	Unknown	\initialized(&SU_setting.execution_result)
 code	telem.c	133	TM_InterruptService	ptr_comparison	Unknown	\pointer_comparable((void *)telemetry_pointer, (void *)(&telemetry_data.time))
 code	telem.c	313	IncrementCounters	index_bound	Unknown	sensor_unit < 4
+code/harness	harness.c	1020	Start_Conversion	index_bound	Unknown	channel < 0x28
 code/harness	harness.c	3338	Acquisition_Tests	signed_overflow	Unknown	octets + 2 ≤ 2147483647

frama-c @ 086dbf67

-Subproject commit 350350ce23b5d1276490b9b6dcb8c6093a3fb4c4
+Subproject commit 086dbf6774409ce5457bbc1ddb232e1f97714b23

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

@@ -2,20 +2,10 @@ directory	file	line	function	property kind	status	property
 .	bits.c	133	send_bits	shift	Unknown	0 ≤ value
 .	bits.c	133	send_bits	signed_overflow	Unknown	value << bi_valid ≤ 2147483647
 .	bits.c	133	send_bits	shift	Unknown	0 ≤ bi_valid < 32
-.	bits.c	134	send_bits	index_bound	Unknown	tmp_1 < (int)(16384 + 2048)
-.	bits.c	134	send_bits	index_bound	Unknown	tmp_2 < (int)(16384 + 2048)
 .	bits.c	135	send_bits	shift	Unknown	0 ≤ (unsigned int)((unsigned int)((unsigned int)((int)(8 * 2)) * sizeof(char)) - (unsigned int)bi_valid) < 32
 .	bits.c	138	send_bits	shift	Unknown	0 ≤ value
 .	bits.c	138	send_bits	signed_overflow	Unknown	value << bi_valid ≤ 2147483647
 .	bits.c	138	send_bits	shift	Unknown	0 ≤ bi_valid < 32
-.	bits.c	166	bi_windup	index_bound	Unknown	tmp_1 < (int)(16384 + 2048)
-.	bits.c	166	bi_windup	index_bound	Unknown	tmp_2 < (int)(16384 + 2048)
-.	bits.c	168	bi_windup	index_bound	Unknown	tmp_3 < (int)(16384 + 2048)
-.	bits.c	189	copy_block	index_bound	Unknown	tmp_1 < (int)(16384 + 2048)
-.	bits.c	189	copy_block	index_bound	Unknown	tmp_2 < (int)(16384 + 2048)
-.	bits.c	190	copy_block	index_bound	Unknown	tmp_5 < (int)(16384 + 2048)
-.	bits.c	190	copy_block	index_bound	Unknown	tmp_6 < (int)(16384 + 2048)
-.	bits.c	203	copy_block	index_bound	Unknown	tmp_7 < (int)(16384 + 2048)
 .	bits.c	203	copy_block	mem_access	Unknown	\valid_read(tmp_8)
 .	deflate.c	324	lm_init	function_pointer	Unknown	\valid_function(read_buf)
 .	deflate.c	386	longest_match	mem_access	Unknown	\valid_read(scan + (int)(best_len - 1))
@@ -447,11 +437,8 @@ directory	file	line	function	property kind	status	property
 .	trees.c	376	ct_init	signed_overflow	Unknown	dist + 1 ≤ 2147483647
 .	trees.c	459	pqdownheap	mem_access	Unknown	\valid_read(&(tree + heap[(int)(j_0 + 1)])->fc.freq)
 .	trees.c	459	pqdownheap	mem_access	Unknown	\valid_read(&(tree + heap[j_0])->fc.freq)
-.	trees.c	459	pqdownheap	index_bound	Unknown	heap[(int)(j_0 + 1)] < (int)((int)(2 * (int)((int)(256 + 1) + 29)) + 1)
-.	trees.c	459	pqdownheap	index_bound	Unknown	heap[j_0] < (int)((int)(2 * (int)((int)(256 + 1) + 29)) + 1)
 .	trees.c	462	pqdownheap	mem_access	Unknown	\valid_read(&(tree + heap[j_0])->fc.freq)
 .	trees.c	462	pqdownheap	mem_access	Unknown	\valid_read(&(tree + v)->fc.freq)
-.	trees.c	462	pqdownheap	index_bound	Unknown	heap[j_0] < (int)((int)(2 * (int)((int)(256 + 1) + 29)) + 1)
 .	trees.c	504	gen_bitlen	mem_access	Unknown	\valid(&(tree + heap[heap_max])->dl.len)
 .	trees.c	508	gen_bitlen	mem_access	Unknown	\valid_read(&(tree + (tree + n)->dl.dad)->dl.len)
 .	trees.c	508	gen_bitlen	mem_access	Unknown	\valid_read(&(tree + n)->dl.dad)
@@ -657,14 +644,6 @@ directory	file	line	function	property kind	status	property
 .	util.c	385	display_ratio	precondition of putc	Unknown	valid_stream: \valid(stream)
 .	util.c	388	display_ratio	precondition of putc	Unknown	valid_stream: \valid(stream)
 .	zip.c	70	zip	mem_access	Unknown	\valid_read(p)
-.	zip.c	89	zip	index_bound	Unknown	tmp_18 < (int)(16384 + 2048)
-.	zip.c	89	zip	index_bound	Unknown	tmp_19 < (int)(16384 + 2048)
-.	zip.c	89	zip	index_bound	Unknown	tmp_22 < (int)(16384 + 2048)
-.	zip.c	89	zip	index_bound	Unknown	tmp_23 < (int)(16384 + 2048)
-.	zip.c	90	zip	index_bound	Unknown	tmp_26 < (int)(16384 + 2048)
-.	zip.c	90	zip	index_bound	Unknown	tmp_27 < (int)(16384 + 2048)
-.	zip.c	90	zip	index_bound	Unknown	tmp_30 < (int)(16384 + 2048)
-.	zip.c	90	zip	index_bound	Unknown	tmp_31 < (int)(16384 + 2048)
 .	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

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

@@ -184,6 +184,7 @@ struct __anonstruct_ev_6 {
    void (*cleanup)(void *privdata) ;
    void (*scheduleTimer)(void *privdata, struct timeval tv) ;
 };
+struct sockaddr;
 struct __anonstruct_sub_7 {
    redisCallbackList invalid ;
    struct dict *channels ;

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

@@ -184,6 +184,7 @@ struct __anonstruct_ev_6 {
    void (*cleanup)(void *privdata) ;
    void (*scheduleTimer)(void *privdata, struct timeval tv) ;
 };
+struct sockaddr;
 struct __anonstruct_sub_7 {
    redisCallbackList invalid ;
    struct dict *channels ;

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

@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
 ------------------------------------
 [metrics] Statements analyzed by Eva
 --------------------------
-3715 stmts in analyzed functions, 3682 stmts analyzed (99.1%)
+3715 stmts in analyzed functions, 3668 stmts analyzed (98.7%)
 adc_buf_channel: 2 stmts out of 2 (100.0%)
 adc_init: 12 stmts out of 12 (100.0%)
 altitude_control_task: 7 stmts out of 7 (100.0%)
@@ -68,7 +68,7 @@ timer_init_0: 4 stmts out of 4 (100.0%)
 timer_periodic_0: 7 stmts out of 7 (100.0%)
 uart1_init: 7 stmts out of 7 (100.0%)
 periodic_task: 51 stmts out of 52 (98.1%)
-auto_nav: 679 stmts out of 694 (97.8%)
+auto_nav: 665 stmts out of 694 (95.8%)
 roll_pitch_pid_run: 22 stmts out of 23 (95.7%)
 nav_home: 38 stmts out of 40 (95.0%)
 main: 30 stmts out of 32 (93.8%)