diff --git a/c-testsuite/.frama-c/00040.eva/alarms.csv b/c-testsuite/.frama-c/00040.eva/alarms.csv
index 06537ae9e4bf75662e9b0b00aea8caf936b31b09..6ca1784575622a646d7b2a87ca8ec79c25541b33 100644
--- a/c-testsuite/.frama-c/00040.eva/alarms.csv
+++ b/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
diff --git a/c-testsuite/.frama-c/00040.eva/metrics.log b/c-testsuite/.frama-c/00040.eva/metrics.log
index 5331e378a9a2e6c51c8464be45c4d0d57d60c068..4205ee5b5e1bc89701808801c6bf77396c8b4320 100644
--- a/c-testsuite/.frama-c/00040.eva/metrics.log
+++ b/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%)
diff --git a/c-testsuite/.frama-c/00040.eva/warnings.log b/c-testsuite/.frama-c/00040.eva/warnings.log
index 8dffc4168f55707e473e38b38edc5445aab51ec1..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/c-testsuite/.frama-c/00040.eva/warnings.log
+++ b/c-testsuite/.frama-c/00040.eva/warnings.log
@@ -1,3 +0,0 @@
-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.
diff --git a/c-testsuite/.frama-c/00040.parse/framac.ast b/c-testsuite/.frama-c/00040.parse/framac.ast
index 2af128c840a2801d8e854814fdaf4319e1768928..a7adfc502c049dd3483f2d33796cd5d22601c6dc 100644
--- a/c-testsuite/.frama-c/00040.parse/framac.ast
+++ b/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);
diff --git a/c-testsuite/.frama-c/00176.eva/metrics.log b/c-testsuite/.frama-c/00176.eva/metrics.log
index 901dd086ff09d44fdf004ba254c2c6f5388e7395..137be239fef8e2a2217503523ae594e25f372ecd 100644
--- a/c-testsuite/.frama-c/00176.eva/metrics.log
+++ b/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%)
diff --git a/c-testsuite/.frama-c/00176.eva/warnings.log b/c-testsuite/.frama-c/00176.eva/warnings.log
index a28f68c4548cb9ae99929ba64a0c98b50fe87c7d..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/c-testsuite/.frama-c/00176.eva/warnings.log
+++ b/c-testsuite/.frama-c/00176.eva/warnings.log
@@ -1,6 +0,0 @@
-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.
diff --git a/c-testsuite/.frama-c/00181.eva/alarms.csv b/c-testsuite/.frama-c/00181.eva/alarms.csv
index b0ae993dc90939ba440720a896a9fcd0561533ed..c94b6c7be8fa81480abad1e18655eca44518e096 100644
--- a/c-testsuite/.frama-c/00181.eva/alarms.csv
+++ b/c-testsuite/.frama-c/00181.eva/alarms.csv
@@ -1,3 +1 @@
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
diff --git a/c-testsuite/.frama-c/00181.eva/metrics.log b/c-testsuite/.frama-c/00181.eva/metrics.log
index 8c0443501394c0381b0766ad16c12112de9061cf..a9075a90dc46b610994b277bfef84f4e5e6adf09 100644
--- a/c-testsuite/.frama-c/00181.eva/metrics.log
+++ b/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%)
diff --git a/c-testsuite/.frama-c/00181.eva/warnings.log b/c-testsuite/.frama-c/00181.eva/warnings.log
index d39353ab3bd18e7ffae0059999d34e7d34dc8789..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/c-testsuite/.frama-c/00181.eva/warnings.log
+++ b/c-testsuite/.frama-c/00181.eva/warnings.log
@@ -1,6 +0,0 @@
-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.
diff --git a/c-testsuite/.frama-c/GNUmakefile b/c-testsuite/.frama-c/GNUmakefile
index 4392686f70744251a1aea05ed19e6891b1e153fd..3c97835abc818bd9f402af915871c0852e738f0b 100644
--- a/c-testsuite/.frama-c/GNUmakefile
+++ b/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
diff --git a/c-testsuite/00040.c b/c-testsuite/00040.c
index cc7e96d9b3a3dbed11601bc3f74369a5a115ac29..cff731322e0677b8c11845d42933ac1ea2b20db0 100644
--- a/c-testsuite/00040.c
+++ b/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]++;
diff --git a/cerberus/.frama-c/besson_blazy_wilkie_Fig_1.eva/nonterm.log b/cerberus/.frama-c/besson_blazy_wilkie_Fig_1.eva/nonterm.log
index 73e1881ae33ed8684f3b5a32ae75da72f6ed1d70..c21adaea10d09601a6632908e3ffde5d11fd71de 100644
--- a/cerberus/.frama-c/besson_blazy_wilkie_Fig_1.eva/nonterm.log
+++ b/cerberus/.frama-c/besson_blazy_wilkie_Fig_1.eva/nonterm.log
@@ -1 +1,2 @@
-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
diff --git a/chrony/.frama-c/chrony-ntp-core.eva/alarms.csv b/chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
index 1caf0c0df676cf04186fedc55e5ec426135df428..fc6d2d49f17fc428a00611dbda9fba26c752d5c0 100644
--- a/chrony/.frama-c/chrony-ntp-core.eva/alarms.csv
+++ b/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)
diff --git a/frama-c b/frama-c
index 5e23a5351095acb2199a8b985ed6b8a61592483e..b7ce41a110ea5bec28f8559fc1adc3a2b8766c01 160000
--- a/frama-c
+++ b/frama-c
@@ -1 +1 @@
-Subproject commit 5e23a5351095acb2199a8b985ed6b8a61592483e
+Subproject commit b7ce41a110ea5bec28f8559fc1adc3a2b8766c01
diff --git a/gzip124/.frama-c/gzip124.eva/alarms.csv b/gzip124/.frama-c/gzip124.eva/alarms.csv
index 1502f216534fe3d1e38776ece54ef7726f19c201..f58e7db19fbbe2e4cba2c7a0234a77b896775eae 100644
--- a/gzip124/.frama-c/gzip124.eva/alarms.csv
+++ b/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;
diff --git a/ioccc/.frama-c/2019_endoh_prog.eva/warnings.log b/ioccc/.frama-c/2019_endoh_prog.eva/warnings.log
index a674f24d718cfd58a4343491908a863829efe079..e85d6acfa31ee20afd61b40eb178ee45d0a93e71 100644
--- a/ioccc/.frama-c/2019_endoh_prog.eva/warnings.log
+++ b/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.
diff --git a/itc-benchmarks/.frama-c/01_w_Defects.eva/nonterm.log b/itc-benchmarks/.frama-c/01_w_Defects.eva/nonterm.log
index 0b81834e0fce96e7fcba751f6233a65db4e4b6b7..7b19e222e442b73c869a91a9ebd12a97abbdf2e7 100644
--- a/itc-benchmarks/.frama-c/01_w_Defects.eva/nonterm.log
+++ b/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 <-
diff --git a/kilo/.frama-c/kilo.eva/alarms.csv b/kilo/.frama-c/kilo.eva/alarms.csv
index 54e0ef9b99daf7f2f2913b1e532e5288b6274ec5..b6cc009ecf0358727615ce35cd41fa7fd7c772d8 100644
--- a/kilo/.frama-c/kilo.eva/alarms.csv
+++ b/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))
diff --git a/libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv b/libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv
index d2c3856b6d114a388f9bd811a2122b96545f2033..79cc69006da1d001b433a160ee282428af6355e4 100644
--- a/libmodbus/.frama-c/libmodbus-unit-server.eva/alarms.csv
+++ b/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))
diff --git a/microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv b/microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv
index c36a7231e74aeff6fc6dd97ed9fa727ea3a7cfa3..07a87b85759e28c8c93f1b5160132289d89c7813 100644
--- a/microstrain/.frama-c/microstrain_gx4_45_test.eva/alarms.csv
+++ b/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)
diff --git a/polarssl/.frama-c/polarssl-server.eva/alarms.csv b/polarssl/.frama-c/polarssl-server.eva/alarms.csv
index 8fa54a0eb8a1568fe7701bf15f56b7cfdf0ab044..d07f7f0b731c553478f0945df89307269f86b445 100644
--- a/polarssl/.frama-c/polarssl-server.eva/alarms.csv
+++ b/polarssl/.frama-c/polarssl-server.eva/alarms.csv
@@ -42,8 +42,8 @@ FRAMAC_SHARE/libc string.h 121 memmove precondition Unknown valid_src: valid_rea
FRAMAC_SHARE/libc string.h 131 memset precondition Unknown valid_s: valid_or_empty(s, n)
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))
FRAMAC_SHARE/libc/sys socket.h 301 accept precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
FRAMAC_SHARE/libc/sys socket.h 551 shutdown precondition Unknown valid_sockfd: 0 ≤ sockfd < 1024
library ctr_drbg.c 154 block_cipher_df mem_access Unknown \valid_read(p + i)