Commit aa2a71da authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

[basic-cwe-examples] add Makefile and improvements

parent 708bcd58
......@@ -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
......
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)))
[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%)
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
/* 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;
}
......
[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
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)))
[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%)
cwe119.c:65:[nonterm] warning: non-terminating function call
stack: host_lookup :: cwe119.c:70 <- main
cwe119.c:73:[nonterm] warning: unreachable return
/* 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;
}
......
[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
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
[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%)
cwe190.c:38:[nonterm] warning: non-terminating function call
cwe190.c:42:[nonterm] warning: non-terminating function call
stack: main
/* 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;
}
......
[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
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)
[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%)
cwe190.c:39:[nonterm] warning: non-terminating loop
cwe190.c:44:[nonterm] warning: non-terminating loop
stack: main
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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment