[c-testsuite] Unroll recursive calls to avoid relying on specifications.

Also avoids a failure on a recursive function without specification
(function factorial in file 00168.c).

Adds annotations to disable partitioning in file 00040.c to avoid combinatorial
explosion.

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]++;