From aa2a71da35ffe4dfbef85cbf0cd7c23a9c243339 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Dec 2020 15:48:21 +0100
Subject: [PATCH] [basic-cwe-examples] add Makefile and improvements
---
basic-cwe-examples/.frama-c/GNUmakefile | 8 ++---
.../.frama-c/cwe119-precise.eva/alarms.csv | 6 ++--
.../.frama-c/cwe119-precise.eva/metrics.log | 13 ++++----
.../.frama-c/cwe119-precise.eva/nonterm.log | 6 ++--
.../.frama-c/cwe119-precise.parse/framac.ast | 31 +++++++++++++------
.../.frama-c/cwe119-precise.parse/metrics.log | 23 +++++++-------
.../.frama-c/cwe119.eva/alarms.csv | 8 ++---
.../.frama-c/cwe119.eva/metrics.log | 13 ++++----
.../.frama-c/cwe119.eva/nonterm.log | 3 ++
.../.frama-c/cwe119.parse/framac.ast | 31 +++++++++++++------
.../.frama-c/cwe119.parse/metrics.log | 23 +++++++-------
.../.frama-c/cwe190-precise.eva/alarms.csv | 2 +-
.../.frama-c/cwe190-precise.eva/metrics.log | 13 ++++----
.../.frama-c/cwe190-precise.eva/nonterm.log | 2 +-
.../.frama-c/cwe190-precise.parse/framac.ast | 28 ++++++++++++-----
.../.frama-c/cwe190-precise.parse/metrics.log | 22 ++++++-------
.../.frama-c/cwe190.eva/alarms.csv | 3 +-
.../.frama-c/cwe190.eva/metrics.log | 13 ++++----
.../.frama-c/cwe190.eva/nonterm.log | 2 +-
.../.frama-c/cwe190.eva/warnings.log | 2 +-
.../.frama-c/cwe190.parse/framac.ast | 28 ++++++++++++-----
.../.frama-c/cwe190.parse/metrics.log | 22 ++++++-------
.../.frama-c/cwe20-precise.eva/metrics.log | 4 +--
.../.frama-c/cwe20-precise.parse/framac.ast | 1 +
.../.frama-c/cwe20-precise.parse/metrics.log | 4 +--
.../.frama-c/cwe20.eva/metrics.log | 4 +--
.../.frama-c/cwe20.parse/framac.ast | 1 +
.../.frama-c/cwe20.parse/metrics.log | 4 +--
.../.frama-c/cwe416-precise.eva/alarms.csv | 8 ++---
.../.frama-c/cwe416-precise.eva/metrics.log | 4 +--
.../.frama-c/cwe416-precise.eva/nonterm.log | 2 +-
.../.frama-c/cwe416-precise.parse/framac.ast | 4 +++
.../.frama-c/cwe416-precise.parse/metrics.log | 10 +++---
.../.frama-c/cwe416.eva/alarms.csv | 8 ++---
.../.frama-c/cwe416.eva/metrics.log | 4 +--
.../.frama-c/cwe416.eva/nonterm.log | 2 ++
.../.frama-c/cwe416.parse/framac.ast | 4 +++
.../.frama-c/cwe416.parse/metrics.log | 10 +++---
.../.frama-c/cwe787-precise.eva/alarms.csv | 2 +-
.../.frama-c/cwe787-precise.eva/metrics.log | 6 ++--
.../.frama-c/cwe787-precise.eva/nonterm.log | 6 ++--
.../.frama-c/cwe787-precise.eva/warnings.log | 4 +--
.../.frama-c/cwe787-precise.parse/framac.ast | 9 ++++--
.../.frama-c/cwe787-precise.parse/metrics.log | 12 +++----
.../.frama-c/cwe787.eva/alarms.csv | 28 ++++++++---------
.../.frama-c/cwe787.eva/metrics.log | 6 ++--
.../.frama-c/cwe787.parse/framac.ast | 9 ++++--
.../.frama-c/cwe787.parse/metrics.log | 12 +++----
basic-cwe-examples/Makefile | 11 +++++++
basic-cwe-examples/cwe119.c | 17 +++++-----
basic-cwe-examples/cwe190.c | 19 +++++++-----
basic-cwe-examples/cwe20.c | 1 +
basic-cwe-examples/cwe416.c | 4 +++
basic-cwe-examples/cwe787.c | 9 ++----
54 files changed, 313 insertions(+), 218 deletions(-)
create mode 100644 basic-cwe-examples/Makefile
diff --git a/basic-cwe-examples/.frama-c/GNUmakefile b/basic-cwe-examples/.frama-c/GNUmakefile
index b6b51aef2..787ebe0b5 100644
--- a/basic-cwe-examples/.frama-c/GNUmakefile
+++ b/basic-cwe-examples/.frama-c/GNUmakefile
@@ -45,10 +45,10 @@ cwe416-precise.parse: ../cwe416.c
cwe787-precise.parse: ../cwe787.c
cwe20-precise.eva: EVAFLAGS +=
-cwe119-precise.eva: EVAFLAGS += -eva-precision 1
-cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow -eva-no-alloc-returns-null
-cwe416-precise.eva: EVAFLAGS += -eva-precision 1
-cwe787-precise.eva: EVAFLAGS += -eva-precision 2 -eva-no-alloc-returns-null
+cwe119-precise.eva: EVAFLAGS +=
+cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow
+cwe416-precise.eva: EVAFLAGS +=
+cwe787-precise.eva: EVAFLAGS += -eva-precision 2
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
index 8fb375b87..2d595fe02 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/alarms.csv
@@ -1,3 +1,5 @@
directory file line function property kind status property
-. cwe119.c 62 host_lookup precondition of strcpy Unknown room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc string.h 352 strcpy precondition Unknown room_string: \valid(dest + (0 .. strlen(src)))
+. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
+. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
+. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc string.h 352 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
index 8d097e6b8..8883390a7 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/metrics.log
@@ -1,14 +1,15 @@
[metrics] Eva coverage statistics
=======================
-Syntactically reachable functions = 6 (out of 6)
-Semantically reached functions = 6
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-47 stmts in analyzed functions, 45 stmts analyzed (95.7%)
-host_lookup: 7 stmts out of 7 (100.0%)
-my_gethostbyaddr: 5 stmts out of 5 (100.0%)
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
my_inet_addr: 10 stmts out of 10 (100.0%)
my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
validate_addr_form: 7 stmts out of 7 (100.0%)
-main: 4 stmts out of 6 (66.7%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
index 1f3822301..a6681f265 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.eva/nonterm.log
@@ -1,3 +1,3 @@
-cwe119.c:62:[nonterm] warning: non-terminating function call
-stack: host_lookup :: cwe119.c:69 <- main
-cwe119.c:70:[nonterm] warning: unreachable return
+cwe119.c:65:[nonterm] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
index a9cac3fad..9df9879f0 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.parse/framac.ast
@@ -1,5 +1,4 @@
/* Generated by Frama-C */
-#include "__fc_builtin.h"
#include "errno.h"
#include "inttypes.h"
#include "netdb.h"
@@ -14,6 +13,22 @@
#include "strings.h"
#include "sys/socket.h"
#include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+ uint32_t __retres;
+ uint32_t r = _rand;
+ if (! r) {
+ __retres = 1U;
+ goto return_label;
+ }
+ else {
+ __retres = r;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
@@ -66,9 +81,9 @@ static in_addr_t my_inet_addr(char const *cp)
goto return_label;
}
else {
- int tmp;
- tmp = Frama_C_nondet(1,(int)4294967295U);
- __retres = (unsigned int)tmp;
+ in_addr_t tmp;
+ tmp = nonzero_uint32_t();
+ __retres = tmp;
goto return_label;
}
return_label: return __retres;
@@ -88,13 +103,11 @@ static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
void host_lookup(char *user_supplied_addr)
{
struct hostent *hp;
- in_addr_t *addr;
+ in_addr_t addr;
char hostname[64];
- in_addr_t tmp;
validate_addr_form(user_supplied_addr);
- tmp = my_inet_addr((char const *)user_supplied_addr);
- addr = (in_addr_t *)tmp;
- hp = my_gethostbyaddr((void const *)addr,sizeof(struct in_addr),2);
+ addr = my_inet_addr((char const *)user_supplied_addr);
+ hp = my_gethostbyaddr((void const *)(& addr),sizeof(struct in_addr),2);
strcpy(hostname,(char const *)hp->h_name);
return;
}
diff --git a/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
index d20479d45..06e1d8be4 100644
--- a/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119-precise.parse/metrics.log
@@ -1,7 +1,8 @@
-[metrics] Defined functions (6)
+[metrics] Defined functions (7)
=====================
host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
- my_inet_addr (1 call); my_strcmp (1 call); validate_addr_form (1 call);
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call);
Specified-only functions (0)
============================
@@ -21,15 +22,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 47
-Decision point = 5
-Global variables = 1
-If = 5
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
Loop = 1
-Goto = 3
-Assignment = 19
-Exit point = 6
-Function = 6
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
Function call = 12
Pointer dereferencing = 6
-Cyclomatic complexity = 11
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
index 692590ced..2d595fe02 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/alarms.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-. cwe119.c 25 my_strcmp mem_access Unknown \valid_read(s1 + i)
-. cwe119.c 25 my_strcmp mem_access Unknown \valid_read(s2 + i)
-. cwe119.c 62 host_lookup precondition of strcpy Unknown room_string: \valid(dest + (0 .. strlen(src)))
-FRAMAC_SHARE/libc string.h 352 strcpy precondition Unknown room_string: \valid(dest + (0 .. strlen(src)))
+. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s1 + i)
+. cwe119.c 28 my_strcmp mem_access Unknown \valid_read(s2 + i)
+. cwe119.c 65 host_lookup precondition of strcpy Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
+FRAMAC_SHARE/libc string.h 352 strcpy precondition Invalid or unreachable room_string: \valid(dest + (0 .. strlen(src)))
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
index a66ce1aca..8883390a7 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/metrics.log
@@ -1,14 +1,15 @@
[metrics] Eva coverage statistics
=======================
-Syntactically reachable functions = 6 (out of 6)
-Semantically reached functions = 6
+Syntactically reachable functions = 7 (out of 7)
+Semantically reached functions = 7
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-47 stmts in analyzed functions, 47 stmts analyzed (100.0%)
-host_lookup: 7 stmts out of 7 (100.0%)
-main: 6 stmts out of 6 (100.0%)
-my_gethostbyaddr: 5 stmts out of 5 (100.0%)
+54 stmts in analyzed functions, 48 stmts analyzed (88.9%)
my_inet_addr: 10 stmts out of 10 (100.0%)
my_strcmp: 12 stmts out of 12 (100.0%)
+nonzero_uint32_t: 9 stmts out of 9 (100.0%)
validate_addr_form: 7 stmts out of 7 (100.0%)
+host_lookup: 4 stmts out of 5 (80.0%)
+my_gethostbyaddr: 4 stmts out of 5 (80.0%)
+main: 2 stmts out of 6 (33.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
index e69de29bb..a6681f265 100644
--- a/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe119.eva/nonterm.log
@@ -0,0 +1,3 @@
+cwe119.c:65:[nonterm] warning: non-terminating function call
+stack: host_lookup :: cwe119.c:70 <- main
+cwe119.c:73:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
index a9cac3fad..9df9879f0 100644
--- a/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe119.parse/framac.ast
@@ -1,5 +1,4 @@
/* Generated by Frama-C */
-#include "__fc_builtin.h"
#include "errno.h"
#include "inttypes.h"
#include "netdb.h"
@@ -14,6 +13,22 @@
#include "strings.h"
#include "sys/socket.h"
#include "sys/uio.h"
+uint32_t volatile _rand;
+uint32_t nonzero_uint32_t(void)
+{
+ uint32_t __retres;
+ uint32_t r = _rand;
+ if (! r) {
+ __retres = 1U;
+ goto return_label;
+ }
+ else {
+ __retres = r;
+ goto return_label;
+ }
+ return_label: return __retres;
+}
+
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
@@ -66,9 +81,9 @@ static in_addr_t my_inet_addr(char const *cp)
goto return_label;
}
else {
- int tmp;
- tmp = Frama_C_nondet(1,(int)4294967295U);
- __retres = (unsigned int)tmp;
+ in_addr_t tmp;
+ tmp = nonzero_uint32_t();
+ __retres = tmp;
goto return_label;
}
return_label: return __retres;
@@ -88,13 +103,11 @@ static struct hostent *my_gethostbyaddr(void const *addr, socklen_t len,
void host_lookup(char *user_supplied_addr)
{
struct hostent *hp;
- in_addr_t *addr;
+ in_addr_t addr;
char hostname[64];
- in_addr_t tmp;
validate_addr_form(user_supplied_addr);
- tmp = my_inet_addr((char const *)user_supplied_addr);
- addr = (in_addr_t *)tmp;
- hp = my_gethostbyaddr((void const *)addr,sizeof(struct in_addr),2);
+ addr = my_inet_addr((char const *)user_supplied_addr);
+ hp = my_gethostbyaddr((void const *)(& addr),sizeof(struct in_addr),2);
strcpy(hostname,(char const *)hp->h_name);
return;
}
diff --git a/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
index d20479d45..06e1d8be4 100644
--- a/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe119.parse/metrics.log
@@ -1,7 +1,8 @@
-[metrics] Defined functions (6)
+[metrics] Defined functions (7)
=====================
host_lookup (2 calls); main (0 call); my_gethostbyaddr (1 call);
- my_inet_addr (1 call); my_strcmp (1 call); validate_addr_form (1 call);
+ my_inet_addr (1 call); my_strcmp (1 call); nonzero_uint32_t (1 call);
+ validate_addr_form (1 call);
Specified-only functions (0)
============================
@@ -21,15 +22,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 47
-Decision point = 5
-Global variables = 1
-If = 5
+Sloc = 54
+Decision point = 6
+Global variables = 2
+If = 6
Loop = 1
-Goto = 3
-Assignment = 19
-Exit point = 6
-Function = 6
+Goto = 5
+Assignment = 21
+Exit point = 7
+Function = 7
Function call = 12
Pointer dereferencing = 6
-Cyclomatic complexity = 11
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
index d7352a280..7ef8d232e 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/alarms.csv
@@ -1,2 +1,2 @@
directory file line function property kind status property
-. cwe190.c 38 main unsigned_overflow Invalid or unreachable (unsigned int)nresp * sizeof(char *) ≤ 4294967295
+. cwe190.c 42 main unsigned_overflow Invalid or unreachable (unsigned int)nresp * sizeof(char *) ≤ 4294967295
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
index 869047fdc..4da1ec297 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/metrics.log
@@ -1,12 +1,13 @@
[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, 20 stmts analyzed (66.7%)
-packet_get_int_ok: 2 stmts out of 2 (100.0%)
-packet_get_int_problem: 2 stmts out of 2 (100.0%)
+41 stmts in analyzed functions, 31 stmts analyzed (75.6%)
+packet_get_int_ok: 5 stmts out of 5 (100.0%)
+packet_get_int_problem: 5 stmts out of 5 (100.0%)
packet_get_string: 2 stmts out of 2 (100.0%)
-main: 14 stmts out of 24 (58.3%)
+random_int: 1 stmts out of 1 (100.0%)
+main: 18 stmts out of 28 (64.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
index a2c084e5d..e238d5be4 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe190.c:38:[nonterm] warning: non-terminating function call
+cwe190.c:42:[nonterm] warning: non-terminating function call
stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
index c04239089..9ed5602e8 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.parse/framac.ast
@@ -1,17 +1,27 @@
/* Generated by Frama-C */
#include "stdlib.h"
+int volatile _rand;
+int random_int(void)
+{
+ return _rand;
+}
+
int packet_get_int_ok(void)
{
- int __retres;
- __retres = 123456;
- return __retres;
+ int tmp_0;
+ int tmp;
+ tmp = random_int();
+ if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+ return tmp_0;
}
int packet_get_int_problem(void)
{
- int __retres;
- __retres = 1073741824;
- return __retres;
+ int tmp_0;
+ int tmp;
+ tmp = random_int();
+ if (tmp) tmp_0 = 1073741824; else tmp_0 = 0;
+ return tmp_0;
}
char *packet_get_string(char const *s)
@@ -28,6 +38,7 @@ int main(void)
int nresp = packet_get_int_ok();
if (nresp > 0) {
response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+ if (! response) exit(1);
{
int i = 0;
while (i < nresp) {
@@ -35,11 +46,12 @@ int main(void)
i ++;
}
}
+ free((void *)response);
}
- free((void *)response);
nresp = packet_get_int_problem();
if (nresp > 0) {
response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+ if (! response) exit(1);
{
int i_0 = 0;
while (i_0 < nresp) {
@@ -47,8 +59,8 @@ int main(void)
i_0 ++;
}
}
+ free((void *)response);
}
- free((void *)response);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
index 209600bca..94c58dcd1 100644
--- a/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190-precise.parse/metrics.log
@@ -1,7 +1,7 @@
-[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);
+ packet_get_string (2 calls); random_int (2 calls);
Specified-only functions (0)
============================
@@ -21,15 +21,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 30
-Decision point = 4
-Global variables = 0
-If = 4
+Sloc = 41
+Decision point = 8
+Global variables = 1
+If = 8
Loop = 2
Goto = 0
-Assignment = 14
-Exit point = 4
-Function = 4
-Function call = 8
+Assignment = 18
+Exit point = 5
+Function = 5
+Function call = 12
Pointer dereferencing = 2
-Cyclomatic complexity = 8
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
index 05f9878d1..95905c5a1 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/alarms.csv
@@ -1,3 +1,2 @@
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)
+. cwe190.c 44 main mem_access Invalid or unreachable \valid(response + i_0)
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
index 29e31d521..1a73b1cf9 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/metrics.log
@@ -1,12 +1,13 @@
[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%)
+41 stmts in analyzed functions, 38 stmts analyzed (92.7%)
+packet_get_int_ok: 5 stmts out of 5 (100.0%)
+packet_get_int_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_int: 1 stmts out of 1 (100.0%)
+main: 25 stmts out of 28 (89.3%)
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
index 90a44fdbc..02c4a2c51 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe190.c:39:[nonterm] warning: non-terminating loop
+cwe190.c:44:[nonterm] warning: non-terminating loop
stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
index da00dd538..8286bf2be 100644
--- a/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
+++ b/basic-cwe-examples/.frama-c/cwe190.eva/warnings.log
@@ -1,2 +1,2 @@
-cwe190.c:39:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+cwe190.c:44:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
index c04239089..9ed5602e8 100644
--- a/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
@@ -1,17 +1,27 @@
/* Generated by Frama-C */
#include "stdlib.h"
+int volatile _rand;
+int random_int(void)
+{
+ return _rand;
+}
+
int packet_get_int_ok(void)
{
- int __retres;
- __retres = 123456;
- return __retres;
+ int tmp_0;
+ int tmp;
+ tmp = random_int();
+ if (tmp) tmp_0 = 0; else tmp_0 = 123456;
+ return tmp_0;
}
int packet_get_int_problem(void)
{
- int __retres;
- __retres = 1073741824;
- return __retres;
+ int tmp_0;
+ int tmp;
+ tmp = random_int();
+ if (tmp) tmp_0 = 1073741824; else tmp_0 = 0;
+ return tmp_0;
}
char *packet_get_string(char const *s)
@@ -28,6 +38,7 @@ int main(void)
int nresp = packet_get_int_ok();
if (nresp > 0) {
response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+ if (! response) exit(1);
{
int i = 0;
while (i < nresp) {
@@ -35,11 +46,12 @@ int main(void)
i ++;
}
}
+ free((void *)response);
}
- free((void *)response);
nresp = packet_get_int_problem();
if (nresp > 0) {
response = (char **)malloc((unsigned int)nresp * sizeof(char *));
+ if (! response) exit(1);
{
int i_0 = 0;
while (i_0 < nresp) {
@@ -47,8 +59,8 @@ int main(void)
i_0 ++;
}
}
+ free((void *)response);
}
- free((void *)response);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
index 209600bca..94c58dcd1 100644
--- a/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
@@ -1,7 +1,7 @@
-[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);
+ packet_get_string (2 calls); random_int (2 calls);
Specified-only functions (0)
============================
@@ -21,15 +21,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 30
-Decision point = 4
-Global variables = 0
-If = 4
+Sloc = 41
+Decision point = 8
+Global variables = 1
+If = 8
Loop = 2
Goto = 0
-Assignment = 14
-Exit point = 4
-Function = 4
-Function call = 8
+Assignment = 18
+Exit point = 5
+Function = 5
+Function call = 12
Pointer dereferencing = 2
-Cyclomatic complexity = 8
+Cyclomatic complexity = 13
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log
index e69261104..55cf71eb1 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.eva/metrics.log
+++ b/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%)
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
index 9b111bb64..832c51ac3 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
@@ -131,6 +131,7 @@ int main(void)
}
}
board = (board_square_t *)malloc((unsigned int)(m * n) * sizeof(board_square_t));
+ free((void *)board);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
index 84c0bb1bc..aea9a9303 100644
--- a/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20-precise.parse/metrics.log
@@ -20,7 +20,7 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 19
+Sloc = 20
Decision point = 4
Global variables = 0
If = 4
@@ -29,6 +29,6 @@ Goto = 1
Assignment = 4
Exit point = 1
Function = 1
-Function call = 11
+Function call = 12
Pointer dereferencing = 0
Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log
index e69261104..55cf71eb1 100644
--- a/basic-cwe-examples/.frama-c/cwe20.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20.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%)
diff --git a/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
index 9b111bb64..832c51ac3 100644
--- a/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
@@ -131,6 +131,7 @@ int main(void)
}
}
board = (board_square_t *)malloc((unsigned int)(m * n) * sizeof(board_square_t));
+ free((void *)board);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
index 84c0bb1bc..aea9a9303 100644
--- a/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe20.parse/metrics.log
@@ -20,7 +20,7 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 19
+Sloc = 20
Decision point = 4
Global variables = 0
If = 4
@@ -29,6 +29,6 @@ Goto = 1
Assignment = 4
Exit point = 1
Function = 1
-Function call = 11
+Function call = 12
Pointer dereferencing = 0
Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
index e851cf8ed..8b44be02a 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/alarms.csv
@@ -1,7 +1,3 @@
directory file line function property kind status property
-. cwe416.c 23 main dangling_pointer Unknown ¬\dangling(&buf2R1)
-. cwe416.c 23 main mem_access Unknown \valid_read(argv + 1)
-. cwe416.c 23 main precondition of strncpy Invalid or unreachable room_nstring: \valid(dest + (0 .. n - 1))
-. cwe416.c 23 main precondition of strncpy Unknown valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc string.h 363 strncpy precondition Unknown valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc string.h 364 strncpy precondition Invalid or unreachable room_nstring: \valid(dest + (0 .. n - 1))
+. cwe416.c 27 main dangling_pointer Invalid or unreachable ¬\dangling(&buf2R1)
+. cwe416.c 27 main mem_access Unknown \valid_read(argv + 1)
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
index 0e6e5e33c..e1d3abc93 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-11 stmts in analyzed functions, 6 stmts analyzed (54.5%)
-main: 6 stmts out of 11 (54.5%)
+19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
+main: 14 stmts out of 19 (73.7%)
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
index d090b734e..8f94f04c8 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
@@ -1,2 +1,2 @@
-cwe416.c:23:[nonterm] warning: non-terminating function call
+cwe416.c:27:[nonterm] warning: non-terminating function call
stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
index 9dd04d553..f036f7c09 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
@@ -15,10 +15,14 @@ int main(int argc, char **argv)
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned int)512);
+ if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned int)512);
+ if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+ if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+ if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned int)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
diff --git a/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
index d284d8218..b69d6dc03 100644
--- a/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416-precise.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 11
-Decision point = 0
+Sloc = 19
+Decision point = 4
Global variables = 0
-If = 0
+If = 4
Loop = 0
Goto = 0
Assignment = 5
Exit point = 1
Function = 1
-Function call = 9
+Function call = 13
Pointer dereferencing = 1
-Cyclomatic complexity = 1
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
index 1a2df76a5..8b44be02a 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/alarms.csv
@@ -1,7 +1,3 @@
directory file line function property kind status property
-. cwe416.c 23 main dangling_pointer Unknown ¬\dangling(&buf2R1)
-. cwe416.c 23 main mem_access Unknown \valid_read(argv + 1)
-. cwe416.c 23 main precondition of strncpy Unknown room_nstring: \valid(dest + (0 .. n - 1))
-. cwe416.c 23 main precondition of strncpy Unknown valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc string.h 363 strncpy precondition Unknown valid_nstring_src: valid_read_nstring(src, n)
-FRAMAC_SHARE/libc string.h 364 strncpy precondition Unknown room_nstring: \valid(dest + (0 .. n - 1))
+. cwe416.c 27 main dangling_pointer Invalid or unreachable ¬\dangling(&buf2R1)
+. cwe416.c 27 main mem_access Unknown \valid_read(argv + 1)
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
index cb1beb046..e1d3abc93 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/metrics.log
@@ -5,5 +5,5 @@ Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-11 stmts in analyzed functions, 11 stmts analyzed (100.0%)
-main: 11 stmts out of 11 (100.0%)
+19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
+main: 14 stmts out of 19 (73.7%)
diff --git a/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
index e69de29bb..8f94f04c8 100644
--- a/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
@@ -0,0 +1,2 @@
+cwe416.c:27:[nonterm] warning: non-terminating function call
+stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
index 9dd04d553..f036f7c09 100644
--- a/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
@@ -15,10 +15,14 @@ int main(int argc, char **argv)
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned int)512);
+ if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned int)512);
+ if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+ if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned int)(512 / 2 - 8));
+ if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned int)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
diff --git a/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
index d284d8218..b69d6dc03 100644
--- a/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe416.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 11
-Decision point = 0
+Sloc = 19
+Decision point = 4
Global variables = 0
-If = 0
+If = 4
Loop = 0
Goto = 0
Assignment = 5
Exit point = 1
Function = 1
-Function call = 9
+Function call = 13
Pointer dereferencing = 1
-Cyclomatic complexity = 1
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
index 9d7be6d0b..452f2812f 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/alarms.csv
@@ -1,2 +1,2 @@
directory file line function property kind status property
-. cwe787.c 29 copy_input mem_access Unknown \valid(dst_buf + tmp_5)
+. cwe787.c 26 copy_input mem_access Unknown \valid(dst_buf + tmp_5)
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
index f6a2b08b8..80b221b25 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/metrics.log
@@ -5,6 +5,6 @@ Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-59 stmts in analyzed functions, 56 stmts analyzed (94.9%)
-copy_input: 52 stmts out of 53 (98.1%)
-main: 4 stmts out of 6 (66.7%)
+63 stmts in analyzed functions, 59 stmts analyzed (93.7%)
+copy_input: 54 stmts out of 55 (98.2%)
+main: 5 stmts out of 8 (62.5%)
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
index 93f8bef44..b16304bfa 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/nonterm.log
@@ -1,3 +1,3 @@
-cwe787.c:23:[nonterm] warning: non-terminating loop
-stack: copy_input :: cwe787.c:45 <- main
-cwe787.c:46:[nonterm] warning: unreachable return
+cwe787.c:20:[nonterm] warning: non-terminating loop
+stack: copy_input :: cwe787.c:42 <- main
+cwe787.c:43:[nonterm] warning: unreachable return
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
index 8abb70980..bd08b209d 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.eva/warnings.log
@@ -1,2 +1,2 @@
-cwe787.c:29:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
-stack: copy_input :: cwe787.c:45 <- main
+cwe787.c:26:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+stack: copy_input :: cwe787.c:42 <- main
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
index f583df233..3a9b0588f 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.parse/framac.ast
@@ -9,6 +9,7 @@ char *copy_input(char *user_supplied_string)
size_t tmp_0;
char *dst_buf =
malloc(((unsigned int)4 * sizeof(char)) * (unsigned int)16);
+ if (! dst_buf) exit(1);
tmp_0 = strlen((char const *)user_supplied_string);
if ((size_t)16 <= tmp_0) exit(1);
dst_index = 0;
@@ -69,10 +70,14 @@ char *copy_input(char *user_supplied_string)
int main(void)
{
int __retres;
+ char *tmp;
+ char *tmp_0;
char *benevolent_string = (char *)"<a href=\'ab&c\'>";
- copy_input(benevolent_string);
+ tmp = copy_input(benevolent_string);
+ free((void *)tmp);
char *malicious_string = (char *)"&&&&&&&&&&&&&&&";
- copy_input(malicious_string);
+ tmp_0 = copy_input(malicious_string);
+ free((void *)tmp_0);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
index 5993c9e94..c31eb0dae 100644
--- a/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787-precise.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 59
-Decision point = 4
+Sloc = 63
+Decision point = 5
Global variables = 0
-If = 4
+If = 5
Loop = 1
Goto = 0
-Assignment = 36
+Assignment = 38
Exit point = 2
Function = 2
-Function call = 6
+Function call = 9
Pointer dereferencing = 12
-Cyclomatic complexity = 6
+Cyclomatic complexity = 7
diff --git a/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
index 0d5866ed7..7c25eae88 100644
--- a/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
+++ b/basic-cwe-examples/.frama-c/cwe787.eva/alarms.csv
@@ -1,19 +1,19 @@
directory file line function property kind status property
+. cwe787.c 22 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
+. cwe787.c 22 copy_input mem_access Unknown \valid(dst_buf + tmp_1)
+. cwe787.c 23 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
+. cwe787.c 23 copy_input mem_access Unknown \valid(dst_buf + tmp_2)
+. cwe787.c 24 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
+. cwe787.c 24 copy_input mem_access Unknown \valid(dst_buf + tmp_3)
. cwe787.c 25 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 25 copy_input mem_access Unknown \valid(dst_buf + tmp_1)
+. cwe787.c 25 copy_input mem_access Unknown \valid(dst_buf + tmp_4)
. cwe787.c 26 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 26 copy_input mem_access Unknown \valid(dst_buf + tmp_2)
-. cwe787.c 27 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 27 copy_input mem_access Unknown \valid(dst_buf + tmp_3)
-. cwe787.c 28 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 28 copy_input mem_access Unknown \valid(dst_buf + tmp_4)
+. cwe787.c 26 copy_input mem_access Unknown \valid(dst_buf + tmp_5)
. cwe787.c 29 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 29 copy_input mem_access Unknown \valid(dst_buf + tmp_5)
-. cwe787.c 32 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 32 copy_input mem_access Unknown \valid(dst_buf + tmp_6)
+. cwe787.c 29 copy_input mem_access Unknown \valid(dst_buf + tmp_6)
+. cwe787.c 30 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
+. cwe787.c 30 copy_input mem_access Unknown \valid(dst_buf + tmp_7)
+. cwe787.c 31 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
+. cwe787.c 31 copy_input mem_access Unknown \valid(dst_buf + tmp_8)
. cwe787.c 33 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 33 copy_input mem_access Unknown \valid(dst_buf + tmp_7)
-. cwe787.c 34 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 34 copy_input mem_access Unknown \valid(dst_buf + tmp_8)
-. cwe787.c 36 copy_input signed_overflow Unknown dst_index + 1 ≤ 2147483647
-. cwe787.c 36 copy_input mem_access Unknown \valid(dst_buf + tmp_9)
+. cwe787.c 33 copy_input mem_access Unknown \valid(dst_buf + tmp_9)
diff --git a/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
index 0c237d4f0..b21ec892c 100644
--- a/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787.eva/metrics.log
@@ -5,6 +5,6 @@ Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
-59 stmts in analyzed functions, 58 stmts analyzed (98.3%)
-main: 6 stmts out of 6 (100.0%)
-copy_input: 52 stmts out of 53 (98.1%)
+63 stmts in analyzed functions, 62 stmts analyzed (98.4%)
+main: 8 stmts out of 8 (100.0%)
+copy_input: 54 stmts out of 55 (98.2%)
diff --git a/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
index f583df233..3a9b0588f 100644
--- a/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
+++ b/basic-cwe-examples/.frama-c/cwe787.parse/framac.ast
@@ -9,6 +9,7 @@ char *copy_input(char *user_supplied_string)
size_t tmp_0;
char *dst_buf =
malloc(((unsigned int)4 * sizeof(char)) * (unsigned int)16);
+ if (! dst_buf) exit(1);
tmp_0 = strlen((char const *)user_supplied_string);
if ((size_t)16 <= tmp_0) exit(1);
dst_index = 0;
@@ -69,10 +70,14 @@ char *copy_input(char *user_supplied_string)
int main(void)
{
int __retres;
+ char *tmp;
+ char *tmp_0;
char *benevolent_string = (char *)"<a href=\'ab&c\'>";
- copy_input(benevolent_string);
+ tmp = copy_input(benevolent_string);
+ free((void *)tmp);
char *malicious_string = (char *)"&&&&&&&&&&&&&&&";
- copy_input(malicious_string);
+ tmp_0 = copy_input(malicious_string);
+ free((void *)tmp_0);
__retres = 0;
return __retres;
}
diff --git a/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
index 5993c9e94..c31eb0dae 100644
--- a/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
+++ b/basic-cwe-examples/.frama-c/cwe787.parse/metrics.log
@@ -20,15 +20,15 @@ Potential entry points (1)
Global metrics
==============
-Sloc = 59
-Decision point = 4
+Sloc = 63
+Decision point = 5
Global variables = 0
-If = 4
+If = 5
Loop = 1
Goto = 0
-Assignment = 36
+Assignment = 38
Exit point = 2
Function = 2
-Function call = 6
+Function call = 9
Pointer dereferencing = 12
-Cyclomatic complexity = 6
+Cyclomatic complexity = 7
diff --git a/basic-cwe-examples/Makefile b/basic-cwe-examples/Makefile
new file mode 100644
index 000000000..824e4eb4e
--- /dev/null
+++ b/basic-cwe-examples/Makefile
@@ -0,0 +1,11 @@
+TARGETS=cwe20 cwe119 cwe190 cwe416 cwe787
+
+all: $(TARGETS)
+
+clean:
+ rm -f $(TARGETS)
+
+CFLAGS ?= -Wall
+
+%: %.c
+ $(CC) $(CFLAGS) -o $@ $^
diff --git a/basic-cwe-examples/cwe119.c b/basic-cwe-examples/cwe119.c
index cfbaa1a82..dcb451760 100644
--- a/basic-cwe-examples/cwe119.c
+++ b/basic-cwe-examples/cwe119.c
@@ -1,15 +1,18 @@
// Based on MITRE's CWE-119, demonstrative example 1
// https://cwe.mitre.org/data/definitions/119.html
-// Run with "-eva-precision 1" to obtain a "Red Alarm".
-
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <netdb.h>
-// To use Frama-C's "Frama_C_interval" to generate a nondeterministic value
-#include "__fc_builtin.h"
+volatile uint32_t _rand;
+// returns a random non-zero uint32_t
+uint32_t nonzero_uint32_t(void) {
+ uint32_t r = _rand;
+ if (!r) return 1U;
+ else return r;
+}
static void validate_addr_form(char *v) {
// naive, simplistic validation
@@ -33,7 +36,7 @@ static in_addr_t my_inet_addr(const char *cp) {
if (my_strcmp(cp, "127.0.0.1") == 0) {
return 0;
} else {
- return Frama_C_nondet(1,UINT_MAX);
+ return nonzero_uint32_t();
}
}
@@ -52,13 +55,13 @@ static struct hostent *my_gethostbyaddr(const void *addr,
void host_lookup(char *user_supplied_addr){
struct hostent *hp;
- in_addr_t *addr;
+ in_addr_t addr;
char hostname[64];
/* routine that ensures user_supplied_addr is in the right format for conversion */
validate_addr_form(user_supplied_addr);
addr = my_inet_addr(user_supplied_addr);
- hp = my_gethostbyaddr(addr, sizeof(struct in_addr), AF_INET);
+ hp = my_gethostbyaddr(&addr, sizeof(struct in_addr), AF_INET);
strcpy(hostname, hp->h_name);
}
diff --git a/basic-cwe-examples/cwe190.c b/basic-cwe-examples/cwe190.c
index ff56da6bd..e303db701 100644
--- a/basic-cwe-examples/cwe190.c
+++ b/basic-cwe-examples/cwe190.c
@@ -6,18 +6,21 @@
// write to the (under-allocated) buffer.
// Adding option "-warn-unsigned-overflow" ensures Eva reports the
// overflow as soon as it happens.
-// Also, adding option "-eva-no-alloc-returns-null" allows focusing on this
-// issue while ignoring the the fact that malloc() may fail (which would
-// require an extra check).
#include <stdlib.h>
+volatile int _rand;
+// returns a random int
+int random_int(void) {
+ return _rand;
+}
+
int packet_get_int_ok() {
- return 123456;
+ return random_int() ? 0 : 123456; // ok size
}
int packet_get_int_problem() {
- return 1073741824;
+ return random_int() ? 1073741824 : 0; // too large (>= INT_MAX/4)
}
char *packet_get_string(const char *s) {
@@ -29,15 +32,17 @@ int main() {
int nresp = packet_get_int_ok();
if (nresp > 0) {
response = malloc(nresp*sizeof(char*));
+ if (!response) exit(1);
for (int i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+ free(response);
}
- free(response);
nresp = packet_get_int_problem();
if (nresp > 0) {
response = malloc(nresp*sizeof(char*));
+ if (!response) exit(1);
for (int i = 0; i < nresp; i++) response[i] = packet_get_string(NULL);
+ free(response);
}
- free(response);
return 0;
}
diff --git a/basic-cwe-examples/cwe20.c b/basic-cwe-examples/cwe20.c
index 4a991fd2b..e10512d78 100644
--- a/basic-cwe-examples/cwe20.c
+++ b/basic-cwe-examples/cwe20.c
@@ -33,5 +33,6 @@ int main() {
}
board = (board_square_t*) malloc( m * n * sizeof(board_square_t));
+ free(board);
return 0;
}
diff --git a/basic-cwe-examples/cwe416.c b/basic-cwe-examples/cwe416.c
index 69ab349a3..255731555 100644
--- a/basic-cwe-examples/cwe416.c
+++ b/basic-cwe-examples/cwe416.c
@@ -16,10 +16,14 @@ int main(int argc, char **argv) {
char *buf2R2;
char *buf3R2;
buf1R1 = (char *) malloc(BUFSIZER1);
+ if (!buf1R1) exit(1);
buf2R1 = (char *) malloc(BUFSIZER1);
+ if (!buf2R1) exit(1);
free(buf2R1);
buf2R2 = (char *) malloc(BUFSIZER2);
+ if (!buf2R2) exit(1);
buf3R2 = (char *) malloc(BUFSIZER2);
+ if (!buf3R2) exit(1);
strncpy(buf2R1, argv[1], BUFSIZER1-1);
free(buf1R1);
free(buf2R2);
diff --git a/basic-cwe-examples/cwe787.c b/basic-cwe-examples/cwe787.c
index 7086b0b37..e31f5a0e2 100644
--- a/basic-cwe-examples/cwe787.c
+++ b/basic-cwe-examples/cwe787.c
@@ -4,10 +4,6 @@
// Option "-eva-precision 1" reduces the number of "Unknown" alarms.
// Run with "-eva-precision 2" to obtain a "Red Alarm".
-// Also, adding option "-eva-no-alloc-returns-null" allows focusing on this
-// issue while ignoring the the fact that malloc() may fail (which would
-// require an extra check).
-
#include <stdlib.h>
#include <string.h>
@@ -16,6 +12,7 @@
char * copy_input(char *user_supplied_string) {
int i, dst_index;
char *dst_buf = (char*)malloc(4*sizeof(char) * MAX_SIZE);
+ if (!dst_buf) exit(1);
if ( MAX_SIZE <= strlen(user_supplied_string) ){
exit(1);
}
@@ -40,8 +37,8 @@ char * copy_input(char *user_supplied_string) {
int main() {
char *benevolent_string = "<a href='ab&c'>";
- copy_input(benevolent_string);
+ free(copy_input(benevolent_string));
char *malicious_string = "&&&&&&&&&&&&&&&";
- copy_input(malicious_string);
+ free(copy_input(malicious_string));
return 0;
}
--
GitLab