Merge branch 'fix/recursion' into 'master'

Sync with frama-c master after MR !3660 and !3698

See merge request !25

c-testsuite/.frama-c/00040.eva/alarms.csv

@@ -12,5 +12,6 @@ directory	file	line	function	property kind	status	property
 .	00040.c	20	chk	signed_overflow	Unknown	r + *(t + (int)((int)(x - i) + (int)(8 * (int)(y + i)))) ≤ 2147483647
 .	00040.c	22	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)((int)(x - i) + (int)(8 * (int)(y - i))))
 .	00040.c	22	chk	signed_overflow	Unknown	r + *(t + (int)((int)(x - i) + (int)(8 * (int)(y - i)))) ≤ 2147483647
-.	00040.c	40	go	signed_overflow	Unknown	*(t + (int)(x + (int)(8 * y))) + 1 ≤ 2147483647
-.	00040.c	42	go	signed_overflow	Unknown	-2147483648 ≤ *(t + (int)(x + (int)(8 * y))) - 1
+.	00040.c	34	go	signed_overflow	Unknown	N + 1 ≤ 2147483647
+.	00040.c	43	go	signed_overflow	Unknown	*(t + (int)(x + (int)(8 * y))) + 1 ≤ 2147483647
+.	00040.c	45	go	signed_overflow	Unknown	-2147483648 ≤ *(t + (int)(x + (int)(8 * y))) - 1

c-testsuite/.frama-c/00040.eva/metrics.log

@@ -5,7 +5,7 @@ Semantically reached functions = 3
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-53 stmts in analyzed functions, 48 stmts analyzed (90.6%)
+53 stmts in analyzed functions, 53 stmts analyzed (100.0%)
 chk: 23 stmts out of 23 (100.0%)
-main: 7 stmts out of 8 (87.5%)
-go: 18 stmts out of 22 (81.8%)
+go: 22 stmts out of 22 (100.0%)
+main: 8 stmts out of 8 (100.0%)

c-testsuite/.frama-c/00040.eva/warnings.log

-00040.c:41:[eva] warning: Using specification of function go for recursive calls.
-Analysis of function go is thus incomplete and its soundness
-relies on the written specification.

c-testsuite/.frama-c/00040.parse/framac.ast

@@ -36,7 +36,10 @@ int go(int n, int x, int y)
     __retres = 0;
     goto return_label;
   }
+  /*@ slevel 0; */
+  /*@ loop unroll 0; */
   while (y < 8) {
+    /*@ loop unroll 0; */
     while (x < 8) {
       int tmp;
       tmp = chk(x,y);

c-testsuite/.frama-c/00176.eva/metrics.log

@@ -5,8 +5,8 @@ Semantically reached functions = 4
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-59 stmts in analyzed functions, 57 stmts analyzed (96.6%)
+59 stmts in analyzed functions, 59 stmts analyzed (100.0%)
 main: 33 stmts out of 33 (100.0%)
 partition: 15 stmts out of 15 (100.0%)
+quicksort: 7 stmts out of 7 (100.0%)
 swap: 4 stmts out of 4 (100.0%)
-quicksort: 5 stmts out of 7 (71.4%)

c-testsuite/.frama-c/00176.eva/warnings.log

-00176.c:46:[eva] warning: Using specification of function quicksort for recursive calls.
-Analysis of function quicksort is thus incomplete and its soundness
-relies on the written specification.
-00176.c:47:[eva] warning: Using specification of function quicksort for recursive calls.
-Analysis of function quicksort is thus incomplete and its soundness
-relies on the written specification.

c-testsuite/.frama-c/00181.eva/alarms.csv

 directory	file	line	function	property kind	status	property
-.	00181.c	77	Move	user assertion	Unknown	j > 0
-.	00181.c	78	Move	user assertion	Unknown	i < 4

c-testsuite/.frama-c/00181.eva/metrics.log

@@ -5,8 +5,8 @@ Semantically reached functions = 4
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-80 stmts in analyzed functions, 77 stmts analyzed (96.2%)
-Move: 21 stmts out of 21 (100.0%)
+80 stmts in analyzed functions, 79 stmts analyzed (98.8%)
+Hanoi: 8 stmts out of 8 (100.0%)
 PrintAll: 26 stmts out of 26 (100.0%)
 main: 25 stmts out of 25 (100.0%)
-Hanoi: 5 stmts out of 8 (62.5%)
+Move: 20 stmts out of 21 (95.2%)

c-testsuite/.frama-c/00181.eva/warnings.log

-00181.c:101:[eva] warning: Using specification of function Hanoi for recursive calls.
-Analysis of function Hanoi is thus incomplete and its soundness
-relies on the written specification.
-00181.c:103:[eva] warning: Using specification of function Hanoi for recursive calls.
-Analysis of function Hanoi is thus incomplete and its soundness
-relies on the written specification.

c-testsuite/.frama-c/GNUmakefile

@@ -23,6 +23,7 @@ FCFLAGS     += \
 ## Eva-specific flags
 EVAFLAGS    += \
   -eva-precision 3 \
+  -eva-unroll-recursive-calls 10 \
 
 # Note: -eva-precision >3 (including 11) does not change anything
 

c-testsuite/00040.c

@@ -34,7 +34,10 @@ go(int n, int x, int y)
                 N++;
                 return 0;
         }
+        //@ slevel 0;
+        //@ loop unroll 0;
         for (; y<8; y++) {
+                //@ loop unroll 0;
                 for (; x<8; x++)
                         if (chk(x, y) == 0) {
                                 t[x + 8*y]++;

cerberus/.frama-c/besson_blazy_wilkie_Fig_1.eva/nonterm.log

-besson_blazy_wilkie_Fig_1.c:7:[nonterm:unreachable] warning: unreachable return
+besson_blazy_wilkie_Fig_1.c:6:[nonterm:stmt] warning: non-terminating function call (initializer)
+stack: main

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

@@ -855,7 +855,7 @@ FRAMAC_SHARE/libc	string.h	131	memset	precondition	Unknown	valid_s: valid_or_emp
 FRAMAC_SHARE/libc	string.h	141	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	string.h	173	strchr	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	761	chown	precondition	Unknown	valid_string_path: valid_read_string(path)
-FRAMAC_SHARE/libc	unistd.h	1124	unlink	precondition	Unknown	valid_string_path: valid_read_string(path)
+FRAMAC_SHARE/libc	unistd.h	1136	unlink	precondition	Unknown	valid_string_path: valid_read_string(path)
 FRAMAC_SHARE/libc/sys	stat.h	32	chmod	assigns clause	Unknown	assigns \nothing;
 FRAMAC_SHARE/libc/sys	stat.h	32	chmod	from clause	Unknown	assigns \result \from *(__x0 + (0 ..)), __x1;
 FRAMAC_SHARE/libc/sys	stat.h	87	stat	precondition	Unknown	valid_pathname: valid_read_string(pathname)

frama-c @ b7ce41a1

-Subproject commit 5e23a5351095acb2199a8b985ed6b8a61592483e
+Subproject commit b7ce41a110ea5bec28f8559fc1adc3a2b8766c01

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

@@ -243,14 +243,6 @@ directory	file	line	function	property kind	status	property
 .	gzip.c	1353	do_list	signed_overflow	Unknown	total_in - header_bytes ≤ 2147483647
 .	gzip.c	1372	do_list	precondition of lseek	Unknown	valid_fd: 0 ≤ fd < 1024
 .	gzip.c	1375	do_list	signed_overflow	Unknown	bytes_in + 8L ≤ 2147483647
-.	gzip.c	1379	do_list	initialization	Unknown	\initialized(&buf[1])
-.	gzip.c	1379	do_list	initialization	Unknown	\initialized(&buf[2] + 0)
-.	gzip.c	1379	do_list	initialization	Unknown	\initialized(&buf[2] + 1)
-.	gzip.c	1379	do_list	initialization	Unknown	\initialized((uch *)buf)
-.	gzip.c	1380	do_list	initialization	Unknown	\initialized(&buf[4] + 0)
-.	gzip.c	1380	do_list	initialization	Unknown	\initialized(&buf[4] + 1)
-.	gzip.c	1380	do_list	initialization	Unknown	\initialized((&buf[4] + 2) + 0)
-.	gzip.c	1380	do_list	initialization	Unknown	\initialized((&buf[4] + 2) + 1)
 .	gzip.c	1387	do_list	index_bound	Unknown	method_0 < 9
 .	gzip.c	1394	do_list	signed_overflow	Unknown	total_in + bytes_in ≤ 2147483647
 .	gzip.c	1400	do_list	signed_overflow	Unknown	total_out + bytes_out ≤ 2147483647
@@ -679,9 +671,9 @@ FRAMAC_SHARE/libc	unistd.h	769	close	precondition	Unknown	valid_fd: 0 ≤ fd < 1
 FRAMAC_SHARE/libc	unistd.h	968	lseek	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1007	read	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1008	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
-FRAMAC_SHARE/libc	unistd.h	1124	unlink	precondition	Unknown	valid_string_path: valid_read_string(path)
-FRAMAC_SHARE/libc	unistd.h	1140	write	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
-FRAMAC_SHARE/libc	unistd.h	1141	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
+FRAMAC_SHARE/libc	unistd.h	1136	unlink	precondition	Unknown	valid_string_path: valid_read_string(path)
+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	stat.h	32	chmod	assigns clause	Unknown	assigns \nothing;
 FRAMAC_SHARE/libc/sys	stat.h	32	chmod	from clause	Unknown	assigns \result \from *(__x0 + (0 ..)), __x1;
 FRAMAC_SHARE/libc/sys	stat.h	35	fstat	assigns clause	Unknown	assigns \result, *__x1;

ioccc/.frama-c/2019_endoh_prog.eva/warnings.log

@@ -3460,72 +3460,207 @@ relies on the written specification.
 2019/endoh/prog.c:34:[eva] warning: Using specification of function x0a for recursive calls.
 Analysis of function x0a is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:36:[eva] warning: Using specification of function x20 for recursive calls.
+Analysis of function x20 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:38:[eva] warning: Using specification of function x21 for recursive calls.
+Analysis of function x21 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:40:[eva] warning: Using specification of function x22 for recursive calls.
+Analysis of function x22 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:43:[eva] warning: Using specification of function x23 for recursive calls.
+Analysis of function x23 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:47:[eva] warning: Using specification of function x25 for recursive calls.
+Analysis of function x25 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:49:[eva] warning: Using specification of function x28 for recursive calls.
+Analysis of function x28 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:51:[eva] warning: Using specification of function x29 for recursive calls.
+Analysis of function x29 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:53:[eva] warning: Using specification of function x2a for recursive calls.
+Analysis of function x2a is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:55:[eva] warning: Using specification of function x2b for recursive calls.
+Analysis of function x2b is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:57:[eva] warning: Using specification of function x2c for recursive calls.
+Analysis of function x2c is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:60:[eva] warning: Using specification of function x2d for recursive calls.
+Analysis of function x2d is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:62:[eva] warning: Using specification of function x2f for recursive calls.
+Analysis of function x2f is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:64:[eva] warning: Using specification of function x30 for recursive calls.
+Analysis of function x30 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:66:[eva] warning: Using specification of function x31 for recursive calls.
+Analysis of function x31 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:68:[eva] warning: Using specification of function x32 for recursive calls.
+Analysis of function x32 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:70:[eva] warning: Using specification of function x33 for recursive calls.
+Analysis of function x33 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:72:[eva] warning: Using specification of function x34 for recursive calls.
+Analysis of function x34 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:74:[eva] warning: Using specification of function x35 for recursive calls.
+Analysis of function x35 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:76:[eva] warning: Using specification of function x36 for recursive calls.
+Analysis of function x36 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:78:[eva] warning: Using specification of function x37 for recursive calls.
+Analysis of function x37 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:80:[eva] warning: Using specification of function x38 for recursive calls.
+Analysis of function x38 is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:82:[eva] warning: Using specification of function x39 for recursive calls.
+Analysis of function x39 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:90:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:87:[eva] warning: Using specification of function x3a for recursive calls.
+Analysis of function x3a is thus incomplete and its soundness
+relies on the written specification.
+2019/endoh/prog.c:90:[eva] warning: Using specification of function x3d for recursive calls.
+Analysis of function x3d is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:119:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:119:[eva] warning: Using specification of function x3f for recursive calls.
+Analysis of function x3f is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:121:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:121:[eva] warning: Using specification of function x5b for recursive calls.
+Analysis of function x5b is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:123:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:123:[eva] warning: Using specification of function x5c for recursive calls.
+Analysis of function x5c is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:128:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:128:[eva] warning: Using specification of function x5d for recursive calls.
+Analysis of function x5d is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:130:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:130:[eva] warning: Using specification of function x61 for recursive calls.
+Analysis of function x61 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:132:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:132:[eva] warning: Using specification of function x62 for recursive calls.
+Analysis of function x62 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:134:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:134:[eva] warning: Using specification of function x63 for recursive calls.
+Analysis of function x63 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:136:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:136:[eva] warning: Using specification of function x64 for recursive calls.
+Analysis of function x64 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:138:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:138:[eva] warning: Using specification of function x65 for recursive calls.
+Analysis of function x65 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:141:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:141:[eva] warning: Using specification of function x66 for recursive calls.
+Analysis of function x66 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:143:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:143:[eva] warning: Using specification of function x68 for recursive calls.
+Analysis of function x68 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:148:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:148:[eva] warning: Using specification of function x69 for recursive calls.
+Analysis of function x69 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:150:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:150:[eva] warning: Using specification of function x6d for recursive calls.
+Analysis of function x6d is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:152:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:152:[eva] warning: Using specification of function x6e for recursive calls.
+Analysis of function x6e is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:155:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:155:[eva] warning: Using specification of function x6f for recursive calls.
+Analysis of function x6f is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:157:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:157:[eva] warning: Using specification of function x71 for recursive calls.
+Analysis of function x71 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:160:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:160:[eva] warning: Using specification of function x72 for recursive calls.
+Analysis of function x72 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:163:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:163:[eva] warning: Using specification of function x74 for recursive calls.
+Analysis of function x74 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:166:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:166:[eva] warning: Using specification of function x76 for recursive calls.
+Analysis of function x76 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:169:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:169:[eva] warning: Using specification of function x78 for recursive calls.
+Analysis of function x78 is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:172:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.
+2019/endoh/prog.c:172:[eva] warning: Using specification of function x7b for recursive calls.
+Analysis of function x7b is thus incomplete and its soundness
+relies on the written specification.
 2019/endoh/prog.c:84:[eva] warning: Using specification of function x3b for recursive calls.
 Analysis of function x3b is thus incomplete and its soundness
 relies on the written specification.

itc-benchmarks/.frama-c/01_w_Defects.eva/nonterm.log

@@ -2072,7 +2072,11 @@ stack: uninit_memory_access_005 :: 01_w_Defects/uninit_memory_access.c:556 <-
        uninit_memory_access_main :: 01_w_Defects/main.c:452 <-
        main :: fc_stubs.c:21 <-
        eva_main
-01_w_Defects/uninit_memory_access.c:147:[nonterm:unreachable] warning: unreachable return
+01_w_Defects/uninit_memory_access.c:145:[nonterm:stmt] warning: non-terminating function call
+stack: uninit_memory_access_006 :: 01_w_Defects/uninit_memory_access.c:561 <-
+       uninit_memory_access_main :: 01_w_Defects/main.c:452 <-
+       main :: fc_stubs.c:21 <-
+       eva_main
 01_w_Defects/uninit_memory_access.c:171:[nonterm:stmt] warning: non-terminating loop
 stack: uninit_memory_access_007_func_002 :: 01_w_Defects/uninit_memory_access.c:194 <-
        uninit_memory_access_007 :: 01_w_Defects/uninit_memory_access.c:566 <-
@@ -2111,7 +2115,11 @@ stack: uninit_memory_access_010 :: 01_w_Defects/uninit_memory_access.c:581 <-
        uninit_memory_access_main :: 01_w_Defects/main.c:452 <-
        main :: fc_stubs.c:21 <-
        eva_main
-01_w_Defects/uninit_memory_access.c:338:[nonterm:unreachable] warning: unreachable return
+01_w_Defects/uninit_memory_access.c:337:[nonterm:stmt] warning: non-terminating function call
+stack: uninit_memory_access_011 :: 01_w_Defects/uninit_memory_access.c:586 <-
+       uninit_memory_access_main :: 01_w_Defects/main.c:452 <-
+       main :: fc_stubs.c:21 <-
+       eva_main
 01_w_Defects/uninit_memory_access.c:370:[nonterm:stmt] warning: non-terminating statement
 stack: uninit_memory_access_012 :: 01_w_Defects/uninit_memory_access.c:591 <-
        uninit_memory_access_main :: 01_w_Defects/main.c:452 <-
@@ -2161,7 +2169,11 @@ stack: uninit_pointer_003 :: 01_w_Defects/uninit_pointer.c:466 <-
        uninit_pointer_main :: 01_w_Defects/main.c:458 <-
        main :: fc_stubs.c:21 <-
        eva_main
-01_w_Defects/uninit_pointer.c:71:[nonterm:unreachable] warning: unreachable return
+01_w_Defects/uninit_pointer.c:70:[nonterm:stmt] warning: non-terminating function call
+stack: uninit_pointer_004 :: 01_w_Defects/uninit_pointer.c:471 <-
+       uninit_pointer_main :: 01_w_Defects/main.c:458 <-
+       main :: fc_stubs.c:21 <-
+       eva_main
 01_w_Defects/uninit_pointer.c:92:[nonterm:stmt] warning: non-terminating statement
 stack: uninit_pointer_005_func_001 :: 01_w_Defects/uninit_pointer.c:97 <-
        uninit_pointer_005 :: 01_w_Defects/uninit_pointer.c:476 <-
@@ -2226,7 +2238,11 @@ stack: uninit_pointer_014 :: 01_w_Defects/uninit_pointer.c:521 <-
        uninit_pointer_main :: 01_w_Defects/main.c:458 <-
        main :: fc_stubs.c:21 <-
        eva_main
-01_w_Defects/uninit_pointer.c:392:[nonterm:unreachable] warning: unreachable return
+01_w_Defects/uninit_pointer.c:391:[nonterm:stmt] warning: non-terminating function call
+stack: uninit_pointer_015 :: 01_w_Defects/uninit_pointer.c:526 <-
+       uninit_pointer_main :: 01_w_Defects/main.c:458 <-
+       main :: fc_stubs.c:21 <-
+       eva_main
 01_w_Defects/uninit_pointer.c:434:[nonterm:stmt] warning: non-terminating loop
 stack: uninit_pointer_016 :: 01_w_Defects/uninit_pointer.c:531 <-
        uninit_pointer_main :: 01_w_Defects/main.c:458 <-

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

@@ -582,4 +582,4 @@ FRAMAC_SHARE/libc	string.h	131	memset	precondition	Unknown	valid_s: valid_or_emp
 FRAMAC_SHARE/libc	string.h	141	strlen	precondition	Unknown	valid_string_s: valid_read_string(s)
 FRAMAC_SHARE/libc	unistd.h	853	ftruncate	assigns clause	Unknown	assigns \nothing;
 FRAMAC_SHARE/libc	unistd.h	853	ftruncate	from clause	Unknown	assigns \result \from __x0, __x1;
-FRAMAC_SHARE/libc	unistd.h	1141	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
+FRAMAC_SHARE/libc	unistd.h	1153	write	precondition	Unknown	buf_has_room: \valid_read((char *)buf + (0 .. count - 1))

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

@@ -6,7 +6,7 @@ FRAMAC_SHARE/libc	string.h	95	memcpy	precondition	Unknown	valid_dest: valid_or_e
 FRAMAC_SHARE/libc	string.h	96	memcpy	precondition	Unknown	valid_src: valid_read_or_empty(src, n)
 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	1141	write	precondition	Unknown	buf_has_room: \valid_read((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))

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

@@ -18,8 +18,8 @@ FRAMAC_SHARE/libc	string.h	96	memcpy	precondition	Unknown	valid_src: valid_read_
 FRAMAC_SHARE/libc	string.h	426	strcat	precondition	Unknown	room_string: \valid(dest + (0 .. strlen(dest) + strlen(src)))
 FRAMAC_SHARE/libc	unistd.h	1007	read	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
 FRAMAC_SHARE/libc	unistd.h	1008	read	precondition	Unknown	buf_has_room: \valid((char *)buf + (0 .. count - 1))
-FRAMAC_SHARE/libc	unistd.h	1140	write	precondition	Unknown	valid_fd: 0 ≤ fd < 1024
-FRAMAC_SHARE/libc	unistd.h	1141	write	precondition	Unknown	buf_has_room: \valid_read((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))
 MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test	GX4-45_Test.c	258	main	precondition of printf_va_25	Unknown	valid_read_string(param0)
 MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test	GX4-45_Test.c	261	main	precondition of printf_va_26	Unknown	valid_read_string(param0)
 MIPSDK/C/Examples/Linux/GX4-45/GX4_45_Test	GX4-45_Test.c	264	main	precondition of printf_va_27	Unknown	valid_read_string(param0)