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

 directory	file	line	function	property kind	status	property
-.	cwe190.c	32	main	mem_access	Unknown	\valid(response + i)
 .	cwe190.c	39	main	mem_access	Invalid or unreachable	\valid(response + i_0)

basic-cwe-examples/.frama-c/cwe190.eva/metrics.log

 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 4 (out of 4)
-Semantically reached functions = 4
+Syntactically reachable functions = 5 (out of 5)
+Semantically reached functions = 5
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-30 stmts in analyzed functions, 25 stmts analyzed (83.3%)
-packet_get_int_ok: 2 stmts out of 2 (100.0%)
-packet_get_int_problem: 2 stmts out of 2 (100.0%)
+42 stmts in analyzed functions, 39 stmts analyzed (92.9%)
+packet_get_size_t_ok: 6 stmts out of 6 (100.0%)
+packet_get_size_t_problem: 5 stmts out of 5 (100.0%)
 packet_get_string: 2 stmts out of 2 (100.0%)
-main: 19 stmts out of 24 (79.2%)
+random_size_t: 1 stmts out of 1 (100.0%)
+main: 25 stmts out of 28 (89.3%)

basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log

-cwe190.c:39:[nonterm] warning: non-terminating loop
+cwe190.c:39:[nonterm:stmt] warning: non-terminating loop
 stack: main

basic-cwe-examples/.frama-c/cwe190.parse/framac.ast

 /* Generated by Frama-C */
+#include "errno.h"
 #include "stdlib.h"
-int packet_get_int_ok(void)
+size_t volatile _rand;
+size_t random_size_t(void)
 {
-  int __retres;
-  __retres = 123456;
-  return __retres;
+  return _rand;
 }
 
-int packet_get_int_problem(void)
+size_t packet_get_size_t_ok(void)
 {
-  int __retres;
-  __retres = 1073741824;
+  size_t __retres;
+  int tmp_0;
+  size_t tmp;
+  tmp = random_size_t();
+  if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+  __retres = (size_t)tmp_0;
   return __retres;
 }
 
+size_t packet_get_size_t_problem(void)
+{
+  unsigned long tmp_0;
+  size_t tmp;
+  tmp = random_size_t();
+  if (tmp) tmp_0 = 18446744073709551615UL / (unsigned long)2 + (unsigned long)1;
+  else tmp_0 = (unsigned long)0;
+  return tmp_0;
+}
+
 char *packet_get_string(char const *s)
 {
   char *__retres;
@@ -25,30 +39,32 @@ int main(void)
 {
   int __retres;
   char **response;
-  int nresp = packet_get_int_ok();
-  if (nresp > 0) {
-    response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+  size_t nresp = packet_get_size_t_ok();
+  if (nresp > (size_t)0) {
+    response = (char **)malloc(nresp * sizeof(char *));
+    if (! response) exit(1);
     {
-      int i = 0;
+      size_t i = (size_t)0;
       while (i < nresp) {
         *(response + i) = packet_get_string((char const *)0);
         i ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
-  nresp = packet_get_int_problem();
-  if (nresp > 0) {
-    response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+  nresp = packet_get_size_t_problem();
+  if (nresp > (size_t)0) {
+    response = (char **)malloc(nresp * sizeof(char *));
+    if (! response) exit(1);
     {
-      int i_0 = 0;
+      size_t i_0 = (size_t)0;
       while (i_0 < nresp) {
         *(response + i_0) = packet_get_string((char const *)0);
         i_0 ++;
       }
     }
+    free((void *)response);
   }
-  free((void *)response);
   __retres = 0;
   return __retres;
 }

basic-cwe-examples/.frama-c/cwe190.parse/metrics.log

-[metrics] Defined functions (4)
+[metrics] Defined functions (5)
 =====================
- main (0 call); packet_get_int_ok (1 call); packet_get_int_problem (1 call);
- packet_get_string (2 calls); 
+ main (0 call); packet_get_size_t_ok (1 call);
+ packet_get_size_t_problem (1 call); packet_get_string (2 calls);
+ random_size_t (2 calls); 
 
 Specified-only functions (0)
 ============================
@@ -21,15 +22,15 @@ Potential entry points (1)
 
 Global metrics
 ============== 
-Sloc = 30
-Decision point = 4
-Global variables = 0
-If = 4
+Sloc = 42
+Decision point = 8
+Global variables = 1
+If = 8
 Loop = 2
 Goto = 0
-Assignment = 14
-Exit point = 4
-Function = 4
-Function call = 8
+Assignment = 19
+Exit point = 5
+Function = 5
+Function call = 12
 Pointer dereferencing = 2
-Cyclomatic complexity = 8
+Cyclomatic complexity = 13

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

+directory	file	line	function	property kind	status	property
+.	cwe20-2.c	32	main	index_bound	Unknown	0 ≤ stack_top
+.	cwe20-2.c	35	main	signed_overflow	Unknown	account_balance - (int)((int)(amount / 100) * 100) ≤ 2147483647

basic-cwe-examples/.frama-c/cwe20-2-precise.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] References to non-analyzed functions
+------------------------------------
+[metrics] Statements analyzed by Eva
+--------------------------
+30 stmts in analyzed functions, 30 stmts analyzed (100.0%)
+main: 30 stmts out of 30 (100.0%)

basic-cwe-examples/.frama-c/cwe20-2-precise.eva/warnings.log

+cwe20-2.c:32:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+stack: main

basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+int account_balance = 1000;
+int bill_stack[100];
+int stack_top;
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * restrict format);
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdin->__fc_FILE_data
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * restrict format, int *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_2(FILE * restrict stream, char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param1),
+            (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param1, param0;
+ */
+int printf_va_2(char const * restrict format, int param0, int param1);
+
+int main(void)
+{
+  int __retres;
+  int error;
+  int amount;
+  {
+    int i = 0;
+    while (i < 100) {
+      bill_stack[i] = 100;
+      i ++;
+    }
+  }
+  stack_top = 100;
+  printf("Please specify the amount to withdraw: \n"); /* printf_va_1 */
+  error = scanf("%d",& amount); /* scanf_va_1 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+    exit(1);
+  }
+  if (amount > account_balance) {
+    fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_2 */
+    exit(1);
+  }
+  int withdraw_bills = amount / 100;
+  while (withdraw_bills) {
+    stack_top --;
+    bill_stack[stack_top] = 0;
+    withdraw_bills --;
+  }
+  account_balance -= (amount / 100) * 100;
+  printf("Withdrew $%d, balance: $%d\n",amount,account_balance); /* printf_va_2 */
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe20-2-precise.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 30
+Decision point = 4
+Global variables = 3
+If = 4
+Loop = 2
+Goto = 0
+Assignment = 11
+Exit point = 1
+Function = 1
+Function call = 7
+Pointer dereferencing = 0
+Cyclomatic complexity = 5

basic-cwe-examples/.frama-c/cwe20-2.eva/alarms.csv

+directory	file	line	function	property kind	status	property
+.	cwe20-2.c	32	main	index_bound	Unknown	0 ≤ stack_top
+.	cwe20-2.c	33	main	signed_overflow	Unknown	-2147483648 ≤ withdraw_bills - 1
+.	cwe20-2.c	35	main	signed_overflow	Unknown	account_balance - (int)((int)(amount / 100) * 100) ≤ 2147483647

basic-cwe-examples/.frama-c/cwe20-2.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] References to non-analyzed functions
+------------------------------------
+[metrics] Statements analyzed by Eva
+--------------------------
+30 stmts in analyzed functions, 30 stmts analyzed (100.0%)
+main: 30 stmts out of 30 (100.0%)

basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+int account_balance = 1000;
+int bill_stack[100];
+int stack_top;
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * restrict format);
+
+/*@ requires \valid(param0);
+    requires valid_read_string(format);
+    ensures \initialized(param0);
+    assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+    assigns \result
+      \from (indirect: __fc_stdin->__fc_FILE_id),
+            (indirect: __fc_stdin->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns __fc_stdin->__fc_FILE_data
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+    assigns *param0
+      \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * restrict format, int *param0);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * restrict stream, char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, stream->__fc_FILE_data;
+    assigns \result
+      \from (indirect: stream->__fc_FILE_id),
+            (indirect: stream->__fc_FILE_data),
+            (indirect: *(format + (0 ..)));
+    assigns stream->__fc_FILE_data
+      \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+            (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_2(FILE * restrict stream, char const * restrict format);
+
+/*@ requires valid_read_string(format);
+    assigns \result, __fc_stdout->__fc_FILE_data;
+    assigns \result
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            (indirect: __fc_stdout->__fc_FILE_data),
+            (indirect: *(format + (0 ..))), (indirect: param1),
+            (indirect: param0);
+    assigns __fc_stdout->__fc_FILE_data
+      \from (indirect: __fc_stdout->__fc_FILE_id),
+            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+            param1, param0;
+ */
+int printf_va_2(char const * restrict format, int param0, int param1);
+
+int main(void)
+{
+  int __retres;
+  int error;
+  int amount;
+  {
+    int i = 0;
+    while (i < 100) {
+      bill_stack[i] = 100;
+      i ++;
+    }
+  }
+  stack_top = 100;
+  printf("Please specify the amount to withdraw: \n"); /* printf_va_1 */
+  error = scanf("%d",& amount); /* scanf_va_1 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+    exit(1);
+  }
+  if (amount > account_balance) {
+    fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_2 */
+    exit(1);
+  }
+  int withdraw_bills = amount / 100;
+  while (withdraw_bills) {
+    stack_top --;
+    bill_stack[stack_top] = 0;
+    withdraw_bills --;
+  }
+  account_balance -= (amount / 100) * 100;
+  printf("Withdrew $%d, balance: $%d\n",amount,account_balance); /* printf_va_2 */
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe20-2.parse/metrics.log

+[metrics] Defined functions (1)
+=====================
+ main (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 30
+Decision point = 4
+Global variables = 3
+If = 4
+Loop = 2
+Goto = 0
+Assignment = 11
+Exit point = 1
+Function = 1
+Function call = 7
+Pointer dereferencing = 0
+Cyclomatic complexity = 5

basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log

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