Commit cf4a1fc1 authored by Thibault Martin's avatar Thibault Martin
Browse files

Bit of cleaning (files not needed for ltest)

parent 587c4b4d
Pipeline #36751 failed with stage
in 14 seconds
......@@ -43,7 +43,7 @@ include ../../Makefile.ltest
$(eval $(call generate-rules,cwe787,../cwe787.c))
### Epilogue. Do not modify this block. #######################################
include $(FRAMAC_SHARE)/analysis-scripts/epilogue.mk
include $(shell $(FRAMAC)-config -print-share-path)/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 24 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:24:[nonterm:stmt] warning: non-terminating function call
stack: contains_char :: cwe761.c:37 <- 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