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

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+struct _board_square_t {
+   char color ;
+};
+typedef struct _board_square_t board_square_t;
+/*@ 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, __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_2(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_2(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_2(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_3(FILE * restrict stream, char const * restrict format);
+
+int main(void)
+{
+  int __retres;
+  int m;
+  int n;
+  int error;
+  board_square_t *board;
+  printf("Please specify the board height: \n"); /* printf_va_1 */
+  error = scanf("%d",& m); /* scanf_va_1 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+    exit(1);
+  }
+  printf("Please specify the board width: \n"); /* printf_va_2 */
+  error = scanf("%d",& n); /* scanf_va_2 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_2 */
+    exit(1);
+  }
+  if (m > 100) goto _LOR;
+  else 
+    if (n > 100) {
+      _LOR:
+      {
+        fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_3 */
+        exit(1);
+      }
+    }
+  board = (board_square_t *)malloc((unsigned long)(m * n) * sizeof(board_square_t));
+  free((void *)board);
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe20-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 = 20
+Decision point = 4
+Global variables = 0
+If = 4
+Loop = 0
+Goto = 1
+Assignment = 4
+Exit point = 1
+Function = 1
+Function call = 12
+Pointer dereferencing = 0
+Cyclomatic complexity = 5

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

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

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

+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+struct _board_square_t {
+   char color ;
+};
+typedef struct _board_square_t board_square_t;
+/*@ 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, __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_2(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_2(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_2(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_3(FILE * restrict stream, char const * restrict format);
+
+int main(void)
+{
+  int __retres;
+  int m;
+  int n;
+  int error;
+  board_square_t *board;
+  printf("Please specify the board height: \n"); /* printf_va_1 */
+  error = scanf("%d",& m); /* scanf_va_1 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+    exit(1);
+  }
+  printf("Please specify the board width: \n"); /* printf_va_2 */
+  error = scanf("%d",& n); /* scanf_va_2 */
+  if (-1 == error) {
+    fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_2 */
+    exit(1);
+  }
+  if (m > 100) goto _LOR;
+  else 
+    if (n > 100) {
+      _LOR:
+      {
+        fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_3 */
+        exit(1);
+      }
+    }
+  board = (board_square_t *)malloc((unsigned long)(m * n) * sizeof(board_square_t));
+  free((void *)board);
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe20.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 = 20
+Decision point = 4
+Global variables = 0
+If = 4
+Loop = 0
+Goto = 1
+Assignment = 4
+Exit point = 1
+Function = 1
+Function call = 12
+Pointer dereferencing = 0
+Cyclomatic complexity = 5

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

+directory	file	line	function	property kind	status	property
+.	cwe416.c	27	main	dangling_pointer	Invalid or unreachable	¬\dangling(&buf2R1)
+.	cwe416.c	27	main	mem_access	Unknown	\valid_read(argv + 1)

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

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

basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log

+cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
+stack: main

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

+/* Generated by Frama-C */
+#include "errno.h"
+#include "fcntl.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+#include "string.h"
+#include "strings.h"
+#include "unistd.h"
+int main(int argc, char **argv)
+{
+  int __retres;
+  char *buf1R1;
+  char *buf2R1;
+  char *buf2R2;
+  char *buf3R2;
+  buf1R1 = (char *)malloc((size_t)512);
+  if (! buf1R1) exit(1);
+  buf2R1 = (char *)malloc((size_t)512);
+  if (! buf2R1) exit(1);
+  free((void *)buf2R1);
+  buf2R2 = (char *)malloc((size_t)(512 / 2 - 8));
+  if (! buf2R2) exit(1);
+  buf3R2 = (char *)malloc((size_t)(512 / 2 - 8));
+  if (! buf3R2) exit(1);
+  strncpy(buf2R1,(char const *)*(argv + 1),(size_t)(512 - 1));
+  free((void *)buf1R1);
+  free((void *)buf2R2);
+  free((void *)buf3R2);
+  __retres = 0;
+  return __retres;
+}
+
+

basic-cwe-examples/.frama-c/cwe416-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 = 19
+Decision point = 4
+Global variables = 0
+If = 4
+Loop = 0
+Goto = 0
+Assignment = 5
+Exit point = 1
+Function = 1
+Function call = 13
+Pointer dereferencing = 1
+Cyclomatic complexity = 5

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

+directory	file	line	function	property kind	status	property
+.	cwe416.c	27	main	dangling_pointer	Invalid or unreachable	¬\dangling(&buf2R1)
+.	cwe416.c	27	main	mem_access	Unknown	\valid_read(argv + 1)

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

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

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

+cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
+stack: main