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

[basic-cwe-examples] add more CWE examples based on MITRE

parent 2a502eab
Pipeline #33127 canceled with stage
in 59 seconds
......@@ -4,7 +4,8 @@
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
FRAMAC_SHARE=$(shell $(FRAMAC)-config -print-share-path)
include $(FRAMAC_SHARE)/analysis-scripts/prologue.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
......@@ -25,7 +26,7 @@ EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## Analysis targets (suffixed with .eva)
IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe588.eva cwe761.eva cwe787.eva
PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
......@@ -39,6 +40,8 @@ cwe20-2.parse: ../cwe20-2.c
cwe119.parse: ../cwe119.c
cwe190.parse: ../cwe190.c
cwe416.parse: ../cwe416.c
cwe588.parse: ../cwe588.c
cwe761.parse: ../cwe761.c
cwe787.parse: ../cwe787.c
cwe20-precise.parse: ../cwe20.c
......@@ -46,8 +49,12 @@ cwe20-2-precise.parse: ../cwe20-2.c
cwe119-precise.parse: ../cwe119.c
cwe190-precise.parse: ../cwe190.c
cwe416-precise.parse: ../cwe416.c
cwe588-precise.parse: ../cwe588.c
cwe761-precise.parse: ../cwe761.c
cwe787-precise.parse: ../cwe787.c
cwe761-precise.parse: CPPFLAGS+=-DFC_EVA_PRECISE
cwe190-unsigned.parse: ../cwe190-unsigned.c
cwe20-precise.eva: EVAFLAGS +=
......@@ -55,11 +62,13 @@ cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
cwe119-precise.eva: EVAFLAGS +=
cwe190-precise.eva: EVAFLAGS +=
cwe416-precise.eva: EVAFLAGS +=
cwe588-precise.eva: EVAFLAGS +=
cwe761-precise.eva: EVAFLAGS += -eva-precision 1
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
include $(FRAMAC_SHARE)/analysis-scripts/epilogue.mk
###############################################################################
# optional, for OSCS
......
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
4 stmts in analyzed functions, 2 stmts analyzed (50.0%)
main: 2 stmts out of 4 (50.0%)
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main
cwe588.c:10:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* Generated by Frama-C */
struct foo {
int i ;
};
int main(void)
{
int __retres;
struct foo *foo = (struct foo *)(& main);
foo->i = 2;
__retres = foo->i;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (address taken) (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (0)
==========================
Global metrics
==============
Sloc = 4
Decision point = 0
Global variables = 0
If = 0
Loop = 0
Goto = 0
Assignment = 3
Exit point = 1
Function = 1
Function call = 0
Pointer dereferencing = 2
Cyclomatic complexity = 1
cwe588.c:9:[kernel:typing:incompatible-pointer-types] warning: casting function to struct foo *
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
4 stmts in analyzed functions, 2 stmts analyzed (50.0%)
main: 2 stmts out of 4 (50.0%)
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main
cwe588.c:10:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* Generated by Frama-C */
struct foo {
int i ;
};
int main(void)
{
int __retres;
struct foo *foo = (struct foo *)(& main);
foo->i = 2;
__retres = foo->i;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (address taken) (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (0)
==========================
Global metrics
==============
Sloc = 4
Decision point = 0
Global variables = 0
If = 0
Loop = 0
Goto = 0
Assignment = 3
Exit point = 1
Function = 1
Function call = 0
Pointer dereferencing = 2
Cyclomatic complexity = 1
cwe588.c:9:[kernel:typing:incompatible-pointer-types] warning: casting function to struct foo *
directory file line function property kind status property
. cwe761.c 21 contains_char precondition of free Invalid or unreachable freeable: p ≡ \null ∨ \freeable(p)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Invalid or unreachable freeable: p ≡ \null ∨ \freeable(p)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 2 (out of 2)
Semantically reached functions = 2
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
21 stmts in analyzed functions, 15 stmts analyzed (71.4%)
main: 2 stmts out of 2 (100.0%)
contains_char: 13 stmts out of 19 (68.4%)
cwe761.c:21:[nonterm:stmt] warning: non-terminating function call
stack: contains_char :: cwe761.c:34 <- main
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "errno.h"
#include "stdint.h"
#include "stdlib.h"
#include "string.c"
#include "string.h"
#include "strings.h"
int contains_char(char c)
{
int __retres;
char *str;
str = (char *)malloc((unsigned long)20 * sizeof(char));
if (! str) {
__retres = 0;
goto return_label;
}
strcpy(str,"Search Me!");
while ((int)*str != '\000') {
if ((int)*str == (int)c) {
free((void *)str);
__retres = 1;
goto return_label;
}
str ++;
}
free((void *)str);
__retres = 0;
return_label: return __retres;
}
int main(void)
{
int tmp;
tmp = contains_char((char)'e');
return tmp;
}
Markdown is supported
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