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

@@ -15,4 +15,4 @@ FRAMAC_SHARE/libc	stdio.h	253	printf_va_12	precondition	Unknown	valid_read_strin
 FRAMAC_SHARE/libc	stdio.h	253	printf_va_3	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	253	printf_va_7	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	stdio.h	253	printf_va_8	precondition	Unknown	valid_read_string(param2)
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)

basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv

@@ -2,4 +2,4 @@ directory	file	line	function	property kind	status	property
 .	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
 .	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
 .	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	436	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))

basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv

@@ -2,4 +2,4 @@ directory	file	line	function	property kind	status	property
 .	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s1 + i)
 .	cwe119.c	28	my_strcmp	mem_access	Unknown	\valid_read(s2 + i)
 .	cwe119.c	65	host_lookup	precondition of strcpy	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	436	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Invalid or unreachable	room_string: \valid(dest + (0 .. strlen(src)))

cerberus/.frama-c/null_pointer_3.eva/alarms.csv

 directory	file	line	function	property kind	status	property
 .	null_pointer_3.c	6	main	precondition of memcmp	Unknown	valid_s2: valid_read_or_empty(s2, n)
-FRAMAC_SHARE/libc	string.h	56	memcmp	precondition	Unknown	valid_s2: valid_read_or_empty(s2, n)
+FRAMAC_SHARE/libc	string.h	50	memcmp	precondition	Unknown	valid_s2: valid_read_or_empty(s2, n)

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

@@ -743,14 +743,14 @@ FRAMAC_SHARE/libc	string.c	246	strncpy	mem_access	Unknown	\valid_read(src + i)
 FRAMAC_SHARE/libc	string.c	332	strdup	precondition of strlen	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	string.c	338	strdup	precondition of memcpy	Unknown	valid_dest: valid_or_empty(dest, n)
 FRAMAC_SHARE/libc	string.c	338	strdup	precondition of memcpy	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	153	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	154	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	164	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	209	strchr	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	147	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	148	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	158	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	203	strchr	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	804	chown	precondition	Unknown	valid_string_path: valid_read_string(path)
 FRAMAC_SHARE/libc	unistd.h	1307	unlink	precondition	Unknown	valid_string_path: valid_read_string(path)
 FRAMAC_SHARE/libc/sys	stat.h	38	chmod	precondition	Unknown	valid_path: valid_read_string(path)

chrony/.frama-c/chrony-regress.eva/alarms.csv

@@ -77,7 +77,7 @@ directory	file	line	function	property kind	status	property
 .	regress.c	679	RGR_MultipleRegress	initialization	Unknown	\initialized(x2 + i)
 .	regress.c	683	RGR_MultipleRegress	initialization	Unknown	\initialized(y + i)
 FRAMAC_SHARE/libc	assert.h	31	__FC_assert	precondition	Invalid or unreachable	nonnull_c: c ≢ 0
-FRAMAC_SHARE/libc	string.h	164	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
+FRAMAC_SHARE/libc	string.h	158	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	66	test_unit	initialization	Unknown	\initialized(&b2)
 test/unit	regress.c	70	test_unit	initialization	Unknown	\initialized(&y[(long)(tmp_11 % (long)n)])

frama-c @ cfbc5b13

-Subproject commit b587ccf098032a894300b4aa6206803173d26932
+Subproject commit cfbc5b132e788fad0ba0c7cb066bc074e262d88f

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

@@ -966,21 +966,21 @@ FRAMAC_SHARE/libc	stdlib.c	60	atoi	signed_overflow	Unknown	-2147483648 ≤ n + (
 FRAMAC_SHARE/libc	stdlib.c	60	atoi	signed_overflow	Unknown	n + (int)((int)'0' - c) ≤ 2147483647
 FRAMAC_SHARE/libc	stdlib.c	62	atoi	signed_overflow	Unknown	-n ≤ 2147483647
 FRAMAC_SHARE/libc	stdlib.h	438	free	precondition	Unknown	freeable: p ≡ \null ∨ \freeable(p)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	186	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
-FRAMAC_SHARE/libc	string.h	187	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
-FRAMAC_SHARE/libc	string.h	195	strncmp	precondition	Unknown	valid_string_s2: valid_read_nstring(s2, n)
-FRAMAC_SHARE/libc	string.h	236	strrchr	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	245	strcspn	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	254	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	435	strcpy	precondition	Unknown	valid_string_src: valid_read_string(src)
-FRAMAC_SHARE/libc	string.h	436	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc	string.h	492	strcat	precondition	Unknown	valid_string_src: valid_read_string(src)
-FRAMAC_SHARE/libc	string.h	493	strcat	precondition	Unknown	valid_string_dest: valid_string(dest)
-FRAMAC_SHARE/libc	string.h	494	strcat	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	180	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
+FRAMAC_SHARE/libc	string.h	181	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
+FRAMAC_SHARE/libc	string.h	189	strncmp	precondition	Unknown	valid_string_s2: valid_read_nstring(s2, n)
+FRAMAC_SHARE/libc	string.h	230	strrchr	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	239	strcspn	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	248	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	429	strcpy	precondition	Unknown	valid_string_src: valid_read_string(src)
+FRAMAC_SHARE/libc	string.h	430	strcpy	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc	string.h	486	strcat	precondition	Unknown	valid_string_src: valid_read_string(src)
+FRAMAC_SHARE/libc	string.h	487	strcat	precondition	Unknown	valid_string_dest: valid_string(dest)
+FRAMAC_SHARE/libc	string.h	488	strcat	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
 FRAMAC_SHARE/libc	unistd.h	804	chown	precondition	Unknown	valid_string_path: valid_read_string(path)
 FRAMAC_SHARE/libc	unistd.h	812	close	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1093	lseek	precondition	Unknown	valid_fd: 0 ≤ fd < 1024

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

@@ -241,8 +241,8 @@ FRAMAC_SHARE/libc	string.c	156	strncmp	initialization	Unknown	\initialized((unsi
 FRAMAC_SHARE/libc	string.c	156	strncmp	mem_access	Unknown	\valid_read((unsigned char *)s1 + i)
 FRAMAC_SHARE/libc	string.c	156	strncmp	signed_overflow	Unknown	(int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i) ≤ 2147483647
 FRAMAC_SHARE/libc	string.c	156	strncmp	signed_overflow	Unknown	-2147483648 ≤ (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	733	access	precondition	Unknown	valid_string_path: valid_read_string(path)

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

@@ -325,15 +325,15 @@ FRAMAC_SHARE/libc	string.c	189	strcasecmp	mem_access	Unknown	\valid_read(s2 + i)
 FRAMAC_SHARE/libc	string.c	193	strcasecmp	mem_access	Unknown	\valid_read(s2 + i)
 FRAMAC_SHARE/libc	string.c	226	strcpy	mem_access	Unknown	\valid_read(src + i)
 FRAMAC_SHARE/libc	string.c	246	strncpy	mem_access	Unknown	\valid_read(src + i)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	153	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	154	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	652	strerror_r	assigns clause	Unknown	assigns \result, *(strerrbuf + (0 ..));
-FRAMAC_SHARE/libc	string.h	652	strerror_r	from clause	Unknown	assigns *(strerrbuf + (0 ..)) \from *(strerrbuf + (0 ..)), errnum, buflen;
-FRAMAC_SHARE/libc	string.h	652	strerror_r	from clause	Unknown	assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	147	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	148	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	646	strerror_r	assigns clause	Unknown	assigns \result, *(strerrbuf + (0 ..));
+FRAMAC_SHARE/libc	string.h	646	strerror_r	from clause	Unknown	assigns *(strerrbuf + (0 ..)) \from *(strerrbuf + (0 ..)), errnum, buflen;
+FRAMAC_SHARE/libc	string.h	646	strerror_r	from clause	Unknown	assigns \result \from *(strerrbuf + (0 ..)), errnum, buflen;
 FRAMAC_SHARE/libc	strings.h	77	strncasecmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
 FRAMAC_SHARE/libc	unistd.h	733	access	precondition	Unknown	valid_string_path: valid_read_string(path)
 FRAMAC_SHARE/libc/sys	socket.h	346	connect	precondition	Unknown	valid_sockfd: 0 ≤ sockfd < 1024

ioccc/.frama-c/2019_adamovsky_iocccsize_2018.eva/alarms.csv

@@ -61,5 +61,5 @@ FRAMAC_SHARE/libc	ctype.h	161	isspace	precondition	Unknown	c_uchar_or_eof: (0
 FRAMAC_SHARE/libc	stdio.h	302	fgetc	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	325	fputc	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	387	ungetc	precondition	Unknown	valid_stream: \valid(stream)
-FRAMAC_SHARE/libc	string.h	194	strncmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
-FRAMAC_SHARE/libc	string.h	254	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	188	strncmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
+FRAMAC_SHARE/libc	string.h	248	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)

ioccc/.frama-c/2019_burton_prog_clean.eva/alarms.csv

 directory	file	line	function	property kind	status	property
 2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	-((int)(~tmp_0)) ≤ 2147483647
-2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	e + (int)(11 ≡ n? 1: 0) ≤ 2147483647
+2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	e + (int)(11 ≡ n ? 1 : 0) ≤ 2147483647
 2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	y + 1 ≤ 2147483647
 2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	j + 1 ≤ 2147483647
 2019/burton	prog.clean.c	1	main	signed_overflow	Unknown	j + tmp_1 ≤ 2147483647

ioccc/.frama-c/2019_iocccsize.eva/alarms.csv

@@ -61,5 +61,5 @@ FRAMAC_SHARE/libc	ctype.h	161	isspace	precondition	Unknown	c_uchar_or_eof: (0
 FRAMAC_SHARE/libc	stdio.h	302	fgetc	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	325	fputc	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	387	ungetc	precondition	Unknown	valid_stream: \valid(stream)
-FRAMAC_SHARE/libc	string.h	194	strncmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
-FRAMAC_SHARE/libc	string.h	254	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	188	strncmp	precondition	Unknown	valid_string_s1: valid_read_nstring(s1, n)
+FRAMAC_SHARE/libc	string.h	248	strspn	precondition	Unknown	valid_string_s: valid_read_string(s)

ioccc/.frama-c/2020_giles_prog.eva/alarms.csv

@@ -214,7 +214,7 @@ directory	file	line	function	property kind	status	property
 2020/giles	prog.c	70	main	initialization	Unknown	\initialized(&k[(uint32_t)(z + 1)])
 FRAMAC_SHARE/libc	stdio.h	396	fread	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	409	fwrite	precondition	Unknown	valid_stream: \valid(stream)
-FRAMAC_SHARE/libc	string.h	57	memcmp	precondition	Unknown	initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	58	memcmp	precondition	Unknown	initialization: s2: \initialized((char *)s2 + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	209	strchr	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	51	memcmp	precondition	Unknown	initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	52	memcmp	precondition	Unknown	initialization: s2: \initialized((char *)s2 + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	203	strchr	precondition	Unknown	valid_string_s: valid_read_string(s)

ioccc/.frama-c/2020_otterness_prog.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-2020/otterness	prog.c	12	A	initialization	Unknown	\initialized(c + (int)(!(c ≢ \null)? 0: 1))
+2020/otterness	prog.c	12	A	initialization	Unknown	\initialized(c + (int)(!(c ≢ \null) ? 0 : 1))
 2020/otterness	prog.c	12	A	initialization	Unknown	\initialized(c)
-2020/otterness	prog.c	12	A	mem_access	Unknown	\valid_read(c + (int)(!(c ≢ \null)? 0: 1))
+2020/otterness	prog.c	12	A	mem_access	Unknown	\valid_read(c + (int)(!(c ≢ \null) ? 0 : 1))
 2020/otterness	prog.c	12	A	mem_access	Unknown	\valid_read(c)
 2020/otterness	prog.c	12	A	ptr_comparison	Unknown	\pointer_comparable((void *)0, (void *)c)
 2020/otterness	prog.c	12	A	signed_overflow	Unknown	(int)((u2)*c) << l ≤ 2147483647
@@ -45,7 +45,7 @@ directory	file	line	function	property kind	status	property
 2020/otterness	prog.c	166	K	shift	Unknown	0 ≤ (int)tmp_3 < 32
 2020/otterness	prog.c	167	K	division_by_zero	Unknown	(u4)e ≢ 0
 2020/otterness	prog.c	175	K	mem_access	Unknown	\valid(b)
-2020/otterness	prog.c	176	K	mem_access	Unknown	\valid(b + (int)(k ≢ 0? 0: 1))
+2020/otterness	prog.c	176	K	mem_access	Unknown	\valid(b + (int)(k ≢ 0 ? 0 : 1))
 2020/otterness	prog.c	176	K	mem_access	Unknown	\valid_read(b)
 2020/otterness	prog.c	177	K	mem_access	Unknown	\valid(b + n)
 2020/otterness	prog.c	178	K	initialization	Unknown	\initialized(b + n)
@@ -82,5 +82,5 @@ FRAMAC_SHARE/libc	stdio.h	395	fread	precondition	Unknown	valid_ptr_block: \valid
 FRAMAC_SHARE/libc	stdio.h	396	fread	precondition	Unknown	valid_stream: \valid(stream)
 FRAMAC_SHARE/libc	stdio.h	408	fwrite	precondition	Unknown	valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1))
 FRAMAC_SHARE/libc	stdio.h	409	fwrite	precondition	Unknown	valid_stream: \valid(stream)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)

itc-benchmarks/.frama-c/01_w_Defects.eva/alarms.csv

@@ -426,7 +426,7 @@ directory	file	line	function	property kind	status	property
 FRAMAC_SHARE/libc	stdlib.h	438	free	precondition	Invalid or unreachable	freeable: p ≡ \null ∨ \freeable(p)
 FRAMAC_SHARE/libc	string.c	226	strcpy	initialization	Unknown	\initialized(src + i)
 FRAMAC_SHARE/libc	string.c	227	strcpy	mem_access	Unknown	\valid(dest + i)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	164	memset	precondition	Invalid or unreachable	valid_s: valid_or_empty(s_0, n)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	158	memset	precondition	Invalid or unreachable	valid_s: valid_or_empty(s_0, n)

kgflags/.frama-c/kgflags-full_api.eva/alarms.csv

@@ -75,8 +75,8 @@ FRAMAC_SHARE/libc	stdio.h	253	printf_va_11	precondition	Unknown	valid_read_strin
 FRAMAC_SHARE/libc	stdio.h	253	printf_va_6	precondition	Unknown	valid_read_string(param1)
 FRAMAC_SHARE/libc	stdlib.h	99	strtod	precondition	Unknown	valid_string_nptr: valid_read_string(nptr)
 FRAMAC_SHARE/libc	stdlib.h	171	strtol	precondition	Unknown	valid_string_nptr: valid_read_string(nptr)
-FRAMAC_SHARE/libc	string.h	186	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
-FRAMAC_SHARE/libc	string.h	187	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
+FRAMAC_SHARE/libc	string.h	180	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
+FRAMAC_SHARE/libc	string.h	181	strcmp	precondition	Unknown	valid_string_s2: valid_read_string(s2)
 examples	full_api.c	34	main	precondition of printf_va_1	Unknown	valid_read_string(param0)
 examples	full_api.c	37	main	is_nan_or_infinite	Unknown	\is_finite(double_val)
 examples	full_api.c	41	main	precondition of printf_va_6	Unknown	valid_read_string(param1)

kgflags/.frama-c/kgflags-simple.eva/alarms.csv

@@ -32,5 +32,5 @@ FRAMAC_SHARE/libc	stdio.h	249	fprintf_va_5	precondition	Unknown	valid_read_strin
 FRAMAC_SHARE/libc	stdio.h	249	fprintf_va_8	precondition	Unknown	valid_read_string(param1)
 FRAMAC_SHARE/libc	stdio.h	249	fprintf_va_9	precondition	Unknown	valid_read_string(param1)
 FRAMAC_SHARE/libc	stdio.h	380	puts	precondition	Unknown	valid_string_s: valid_read_string(s)
-FRAMAC_SHARE/libc	string.h	186	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
+FRAMAC_SHARE/libc	string.h	180	strcmp	precondition	Unknown	valid_string_s1: valid_read_string(s1)
 examples	simple.c	12	main	precondition of puts	Unknown	valid_string_s: valid_read_string(s)

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

@@ -574,11 +574,11 @@ FRAMAC_SHARE/libc	string.c	306	strstr	mem_access	Unknown	\valid_read(haystack +
 FRAMAC_SHARE/libc	string.c	307	strstr	mem_access	Unknown	\valid_read(needle + j)
 FRAMAC_SHARE/libc	string.c	309	strstr	mem_access	Unknown	\valid_read(needle + j)
 FRAMAC_SHARE/libc	string.c	338	strdup	precondition of memcpy	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	131	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
-FRAMAC_SHARE/libc	string.h	153	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	154	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
-FRAMAC_SHARE/libc	string.h	164	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
-FRAMAC_SHARE/libc	string.h	174	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	125	memcpy	precondition	Unknown	separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1))
+FRAMAC_SHARE/libc	string.h	147	memmove	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	148	memmove	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	158	memset	precondition	Unknown	valid_s: valid_or_empty(s, n)
+FRAMAC_SHARE/libc	string.h	168	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	1327	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))

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

@@ -2,8 +2,8 @@ directory	file	line	function	property kind	status	property
 FRAMAC_SHARE/libc	stdio.h	253	printf_va_15	precondition	Unknown	valid_read_string(param0)
 FRAMAC_SHARE/libc	string.c	146	strcmp	mem_access	Unknown	\valid_read(s1 + i)
 FRAMAC_SHARE/libc	string.c	149	strcmp	mem_access	Unknown	\valid_read((unsigned char *)s1 + i)
-FRAMAC_SHARE/libc	string.h	128	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
-FRAMAC_SHARE/libc	string.h	129	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
+FRAMAC_SHARE/libc	string.h	122	memcpy	precondition	Unknown	valid_dest: valid_or_empty(dest, n)
+FRAMAC_SHARE/libc	string.h	123	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
 FRAMAC_SHARE/libc	time.h	356	nanosleep	precondition	Unknown	valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000
 FRAMAC_SHARE/libc	unistd.h	1144	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
 FRAMAC_SHARE/libc	unistd.h	1327	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))