[c-testsuite] apply code fixes and analysis improvements

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

 directory	file	line	function	property kind	status	property
-.	00025.c	1	strlen	assigns clause	Unknown	assigns \nothing;
-.	00025.c	1	strlen	from clause	Unknown	assigns \result \from \nothing;

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

-00025.c:4:[kernel:annot:missing-spec] warning: Neither code nor specification for function strlen, generating default assigns from the prototype

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

 /* Generated by Frama-C */
-int strlen(char *);
+/*@ assigns \result;
+    assigns \result \from *(s + (0 ..)); */
+int strlen(char *s);
 
 int main(void)
 {

c-testsuite/.frama-c/00025.parse/metrics.log

@@ -2,13 +2,13 @@
 =====================
  main (0 call); 
 
-Specified-only functions (0)
+Specified-only functions (1)
 ============================
- 
+ strlen (1 call); 
 
-Undefined and unspecified functions (1)
+Undefined and unspecified functions (0)
 =======================================
- strlen (1 call); 
+ 
 
 'Extern' global variables (0)
 =============================

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

 directory	file	line	function	property kind	status	property
 .	00040.c	13	chk	mem_access	Unknown	\valid_read(t + (int)(x + (int)(8 * i)))
+.	00040.c	13	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)(x + (int)(8 * i)))
+.	00040.c	13	chk	signed_overflow	Unknown	r + *(t + (int)(x + (int)(8 * i))) ≤ 2147483647
+.	00040.c	14	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)(i + (int)(8 * y)))
+.	00040.c	14	chk	signed_overflow	Unknown	r + *(t + (int)(i + (int)(8 * y))) ≤ 2147483647
+.	00040.c	16	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)((int)(x + i) + (int)(8 * (int)(y + i))))
+.	00040.c	16	chk	signed_overflow	Unknown	r + *(t + (int)((int)(x + i) + (int)(8 * (int)(y + i)))) ≤ 2147483647
+.	00040.c	18	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)((int)(x + i) + (int)(8 * (int)(y - i))))
+.	00040.c	18	chk	signed_overflow	Unknown	r + *(t + (int)((int)(x + i) + (int)(8 * (int)(y - i)))) ≤ 2147483647
+.	00040.c	20	chk	signed_overflow	Unknown	-2147483648 ≤ r + *(t + (int)((int)(x - i) + (int)(8 * (int)(y + i))))
+.	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

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
 --------------------------
-49 stmts in analyzed functions, 44 stmts analyzed (89.8%)
-chk: 19 stmts out of 19 (100.0%)
+53 stmts in analyzed functions, 48 stmts analyzed (90.6%)
+chk: 23 stmts out of 23 (100.0%)
 main: 7 stmts out of 8 (87.5%)
 go: 18 stmts out of 22 (81.8%)

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

-00040.c:38:[eva] warning: recursive call during value analysis of go (go <- go :: 00040.c:50 <- main).
-Assuming the call has no effect. The analysis will be unsound.
+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

@@ -11,15 +11,23 @@ int chk(int x, int y)
   while (i < 8) {
     r += *(t + (x + 8 * i));
     r += *(t + (i + 8 * y));
-    if ((x + i < 8) & (y + i < 8)) r += *(t + ((x + i) + 8 * (y + i)));
-    if ((x + i < 8) & (y - i >= 0)) r += *(t + ((x + i) + 8 * (y - i)));
-    if ((x - i >= 0) & (y + i < 8)) r += *(t + ((x - i) + 8 * (y + i)));
-    if ((x - i >= 0) & (y - i >= 0)) r += *(t + ((x - i) + 8 * (y - i)));
+    if (x + i < 8) 
+      if (y + i < 8) r += *(t + ((x + i) + 8 * (y + i)));
+    if (x + i < 8) 
+      if (y - i >= 0) r += *(t + ((x + i) + 8 * (y - i)));
+    if (x - i >= 0) 
+      if (y + i < 8) r += *(t + ((x - i) + 8 * (y + i)));
+    if (x - i >= 0) 
+      if (y - i >= 0) r += *(t + ((x - i) + 8 * (y - i)));
     i ++;
   }
   return r;
 }
 
+/*@ assigns *(t + (0 .. 63));
+    assigns *(t + (0 .. 63))
+      \from *(t + (0 .. 63)), (indirect: n), (indirect: x), (indirect: y);
+ */
 int go(int n, int x, int y)
 {
   int __retres;

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

@@ -20,10 +20,10 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 49
-Decision point = 10
+Sloc = 53
+Decision point = 14
 Global variables = 2
-If = 10
+If = 14
 Loop = 3
 Goto = 2
 Assignment = 21
@@ -31,4 +31,4 @@ Exit point = 3
 Function = 3
 Function call = 4
 Pointer dereferencing = 10
-Cyclomatic complexity = 13
+Cyclomatic complexity = 17

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

-00040.c:15:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:15:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:17:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:17:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:19:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:19:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:21:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation
-00040.c:21:[kernel:CERT:EXP:46] warning: operand of bitwise operator is a logical relation

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

 directory	file	line	function	property kind	status	property
-.	00141.c	11	main	initialization	Invalid or unreachable	\initialized(&foo)

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

@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-4 stmts in analyzed functions, 1 stmts analyzed (25.0%)
-main: 1 stmts out of 4 (25.0%)
+4 stmts in analyzed functions, 4 stmts analyzed (100.0%)
+main: 4 stmts out of 4 (100.0%)

c-testsuite/.frama-c/00141.eva/nonterm.log

-00141.c:11:[nonterm] warning: non-terminating statement
-stack: main

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

+00141.c:17:[eva:signed-overflow] warning: 2's complement assumed for overflow
+00141.c:18:[eva:signed-overflow] warning: 2's complement assumed for overflow

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

 /* Generated by Frama-C */
+int volatile foo;
+int volatile bar;
+int volatile foobar;
 int main(void)
 {
   int __retres;
-  int foo;
-  int bar;
-  int foobar;
   foobar = foo + bar;
   foobar = foo + bar;
   __retres = 0;

c-testsuite/.frama-c/00141.parse/metrics.log

@@ -22,7 +22,7 @@ Global metrics
 ============== 
 Sloc = 4
 Decision point = 0
-Global variables = 0
+Global variables = 3
 If = 0
 Loop = 0
 Goto = 0

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

 directory	file	line	function	property kind	status	property
-.	00144.c	7	main	initialization	Invalid or unreachable	\initialized(&i)

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

@@ -5,5 +5,5 @@ Semantically reached functions = 1
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-26 stmts in analyzed functions, 1 stmts analyzed (3.8%)
-main: 1 stmts out of 26 (3.8%)
+26 stmts in analyzed functions, 26 stmts analyzed (100.0%)
+main: 26 stmts out of 26 (100.0%)

c-testsuite/.frama-c/00144.eva/nonterm.log

-00144.c:7:[nonterm] warning: non-terminating statement
-stack: main

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

 /* Generated by Frama-C */
+int volatile i;
 int main(void)
 {
   int __retres;
-  int i;
   int *q;
   void *p;
   if (i) i = 0; else i = (int)0l;