[basic-cwe-examples] split CWE190 in two different cases

basic-cwe-examples/.frama-c/GNUmakefile

@@ -29,7 +29,9 @@ IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe78
 
 PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
 
-TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS)
+OTHER_TARGETS = cwe190-unsigned.parse
+
+TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS) $(OTHER_TARGETS)
 
 ### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
 cwe20.parse:  ../cwe20.c
@@ -46,12 +48,15 @@ cwe190-precise.parse: ../cwe190.c
 cwe416-precise.parse: ../cwe416.c
 cwe787-precise.parse: ../cwe787.c
 
+cwe190-unsigned.parse: ../cwe190-unsigned.c
+
 cwe20-precise.eva:   EVAFLAGS +=
 cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
 cwe119-precise.eva:  EVAFLAGS +=
-cwe190-precise.eva:  EVAFLAGS += -warn-unsigned-overflow
+cwe190-precise.eva:  EVAFLAGS +=
 cwe416-precise.eva:  EVAFLAGS +=
 cwe787-precise.eva:  EVAFLAGS += -eva-precision 2
+cwe190-unsigned.eva:  EVAFLAGS += -warn-unsigned-overflow
 
 ### Epilogue. Do not modify this block. #######################################
 include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk

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

 directory	file	line	function	property kind	status	property
-.	cwe190.c	43	main	unsigned_overflow	Invalid or unreachable	nresp * sizeof(char *) ≤ 18446744073709551615
+.	cwe190.c	39	main	mem_access	Invalid or unreachable	\valid(response + i_0)

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

@@ -5,9 +5,9 @@ Semantically reached functions = 5
 Coverage estimation = 100.0%
 [metrics] Statements analyzed by Eva
 --------------------------
-42 stmts in analyzed functions, 32 stmts analyzed (76.2%)
+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%)
 random_size_t: 1 stmts out of 1 (100.0%)
-main: 18 stmts out of 28 (64.3%)
+main: 25 stmts out of 28 (89.3%)

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

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

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

+cwe190.c:39:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+stack: main

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

+/* Generated by Frama-C */
+#include "stdlib.h"
+long volatile _rand;
+long random_long(void)
+{
+  return _rand;
+}
+
+long packet_get_long_ok(void)
+{
+  long __retres;
+  int tmp_0;
+  long tmp;
+  tmp = random_long();
+  if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+  __retres = (long)tmp_0;
+  return __retres;
+}
+
+long packet_get_long_problem(void)
+{
+  long tmp_0;
+  long tmp;
+  tmp = random_long();
+  if (tmp) tmp_0 = 9223372036854775807L / (long)2; else tmp_0 = (long)0;
+  return tmp_0;
+}
+
+char *packet_get_string(char const *s)
+{
+  char *__retres;
+  __retres = (char *)"string";
+  return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  char **response;
+  long nresp = packet_get_long_ok();
+  if (nresp > (long)0) {
+    response = (char **)malloc((unsigned long)nresp * sizeof(char *));
+    if (! response) exit(1);
+    {
+      long i = (long)0;
+      while (i < nresp) {
+        *(response + i) = packet_get_string((char const *)0);
+        i ++;
+      }
+    }
+    free((void *)response);
+  }
+  nresp = packet_get_long_problem();
+  if (nresp > (long)0) {
+    response = (char **)malloc((unsigned long)nresp * sizeof(char *));
+    if (! response) exit(1);
+    {
+      long i_0 = (long)0;
+      while (i_0 < nresp) {
+        *(response + i_0) = packet_get_string((char const *)0);
+        i_0 ++;
+      }
+    }
+    free((void *)response);
+  }
+  __retres = 0;
+  return __retres;
+}
+
+

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

+[metrics] Defined functions (5)
+=====================
+ main (0 call); packet_get_long_ok (1 call);
+ packet_get_long_problem (1 call); packet_get_string (2 calls);
+ random_long (2 calls); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (1)
+==========================
+ main; 
+
+Global metrics
+============== 
+Sloc = 42
+Decision point = 8
+Global variables = 1
+If = 8
+Loop = 2
+Goto = 0
+Assignment = 19
+Exit point = 5
+Function = 5
+Function call = 12
+Pointer dereferencing = 2
+Cyclomatic complexity = 13

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

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

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

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

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

-cwe190.c:45:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+cwe190.c:39:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
 stack: main

basic-cwe-examples/cwe190-unsigned.c

+// Based on MITRE's CWE-190, demonstrative example 2
+// https://cwe.mitre.org/data/definitions/190.html
+
+// By default, Frama-C/Eva does not report unsigned overflows as alarms;
+// nevertheless, in the code below, Eva reports an alarm when trying to
+// write to the (under-allocated) buffer.
+// Adding option "-warn-unsigned-overflow" ensures Eva reports the
+// overflow as soon as it happens.
+
+#include <limits.h>
+#include <stdlib.h>
+
+volatile long _rand;
+// returns a random long
+long random_long(void) {
+  return _rand;
+}
+
+long packet_get_long_ok() {
+  return random_long() ? 0 : 123456; // ok size
+}
+
+long packet_get_long_problem() {
+  return random_long() ? LONG_MAX/2 : 0; // too large
+}
+
+char *packet_get_string(const char *s) {
+  return "string";
+}
+
+int main() {
+  char **response;
+  long nresp = packet_get_long_ok();
+  if (nresp > 0) {
+    response = malloc(nresp*sizeof(char*));
+    if (!response) exit(1);
+    for (long i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+    free(response);
+  }
+
+  nresp = packet_get_long_problem();
+  if (nresp > 0) {
+    response = malloc(nresp*sizeof(char*));
+    if (!response) exit(1);
+    for (long i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+    free(response);
+  }
+  return 0;
+}

basic-cwe-examples/cwe190.c

 // Based on MITRE's CWE-190, demonstrative example 2
 // https://cwe.mitre.org/data/definitions/190.html
 
-// By default, Frama-C/Eva does not report unsigned overflows as alarms;
-// nevertheless, in the code below, Eva reports an alarm when trying to
-// write to the (under-allocated) buffer.
-// Adding option "-warn-unsigned-overflow" ensures Eva reports the
-// overflow as soon as it happens.
-
 #include <stdint.h>
 #include <stdlib.h>