Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/open-source-case-studies
  • contra-bit/open-source-case-studies
2 results
Show changes
Hide whitespace changes
Inline Side-by-side
Showing
with 152 additions and 71 deletions
basic-cwe-examples/.frama-c/cwe190.parse/framac.ast
View file @ bf5deb7b
/* Generated by Frama-C */
#include "errno.h"
#include "stdlib.h"
long volatile _rand;
long random_long(void)
size_t volatile _rand;
size_t random_size_t(void)
{
return _rand;
}
long packet_get_long_ok(void)
size_t packet_get_size_t_ok(void)
{
long __retres;
size_t __retres;
int tmp_0;
long tmp;
tmp = random_long();
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 0; else tmp_0 = 123456;
__retres = (long)tmp_0;
__retres = (size_t)tmp_0;
return __retres;
}
long packet_get_long_problem(void)
size_t packet_get_size_t_problem(void)
{
long tmp_0;
long tmp;
tmp = random_long();
if (tmp) tmp_0 = 9223372036854775807L / (long)2; else tmp_0 = (long)0;
unsigned long tmp_0;
size_t tmp;
tmp = random_size_t();
if (tmp) tmp_0 = 18446744073709551615UL / (unsigned long)2 + (unsigned long)1;
else tmp_0 = (unsigned long)0;
return tmp_0;
}
......@@ -37,12 +39,12 @@ 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 *));
size_t nresp = packet_get_size_t_ok();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i = (long)0;
size_t i = (size_t)0;
while (i < nresp) {
*(response + i) = packet_get_string((char const *)0);
i ++;
......@@ -50,12 +52,12 @@ int main(void)
}
free((void *)response);
}
nresp = packet_get_long_problem();
if (nresp > (long)0) {
response = (char **)malloc((unsigned long)nresp * sizeof(char *));
nresp = packet_get_size_t_problem();
if (nresp > (size_t)0) {
response = (char **)malloc(nresp * sizeof(char *));
if (! response) exit(1);
{
long i_0 = (long)0;
size_t i_0 = (size_t)0;
while (i_0 < nresp) {
*(response + i_0) = packet_get_string((char const *)0);
i_0 ++;
......
basic-cwe-examples/.frama-c/cwe190.parse/metrics.log
View file @ bf5deb7b
[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);
main (0 call); packet_get_size_t_ok (1 call);
packet_get_size_t_problem (1 call); packet_get_string (2 calls);
random_size_t (2 calls);
Specified-only functions (0)
============================
......
basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast
View file @ bf5deb7b
......@@ -17,10 +17,10 @@ int stack_top;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -34,7 +34,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -46,7 +46,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -58,7 +58,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -72,7 +72,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param1, param0;
*/
int printf_va_2(char const * __restrict format, int param0, int param1);
int printf_va_2(char const * restrict format, int param0, int param1);
int main(void)
{
......
basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast
View file @ bf5deb7b
......@@ -17,10 +17,10 @@ int stack_top;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -34,7 +34,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -46,7 +46,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -58,7 +58,7 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -72,7 +72,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param1, param0;
*/
int printf_va_2(char const * __restrict format, int param0, int param1);
int printf_va_2(char const * restrict format, int param0, int param1);
int main(void)
{
......
basic-cwe-examples/.frama-c/cwe20-precise.parse/framac.ast
View file @ bf5deb7b
......@@ -18,10 +18,10 @@ typedef struct _board_square_t board_square_t;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -35,7 +35,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -47,7 +47,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -59,10 +59,10 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * __restrict format);
int printf_va_2(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -76,7 +76,7 @@ int printf_va_2(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_2(char const * __restrict format, int *param0);
int scanf_va_2(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -88,7 +88,7 @@ int scanf_va_2(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -100,7 +100,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_3(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_3(FILE * restrict stream, char const * restrict format);
int main(void)
{
......
basic-cwe-examples/.frama-c/cwe20.parse/framac.ast
View file @ bf5deb7b
......@@ -18,10 +18,10 @@ typedef struct _board_square_t board_square_t;
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
int printf_va_1(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -35,7 +35,7 @@ int printf_va_1(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_1(char const * __restrict format, int *param0);
int scanf_va_1(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -47,7 +47,7 @@ int scanf_va_1(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_1(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
......@@ -59,10 +59,10 @@ int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * __restrict format);
int printf_va_2(char const * restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
/*@ requires \valid(param0);
requires valid_read_string(format);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
......@@ -76,7 +76,7 @@ int printf_va_2(char const * __restrict format);
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int scanf_va_2(char const * __restrict format, int *param0);
int scanf_va_2(char const * restrict format, int *param0);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -88,7 +88,7 @@ int scanf_va_2(char const * __restrict format, int *param0);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_2(FILE * restrict stream, char const * restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
......@@ -100,7 +100,7 @@ int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_3(FILE * __restrict stream, char const * __restrict format);
int fprintf_va_3(FILE * restrict stream, char const * restrict format);
int main(void)
{
......
basic-cwe-examples/.frama-c/cwe416-precise.eva/nonterm.log
View file @ bf5deb7b
cwe416.c:27:[nonterm] warning: non-terminating function call
cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
stack: main
basic-cwe-examples/.frama-c/cwe416-precise.parse/framac.ast
View file @ bf5deb7b
/* Generated by Frama-C */
#include "errno.h"
#include "fcntl.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
......@@ -14,16 +15,16 @@ int main(int argc, char **argv)
char *buf2R1;
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned long)512);
buf1R1 = (char *)malloc((size_t)512);
if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned long)512);
buf2R1 = (char *)malloc((size_t)512);
if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
buf2R2 = (char *)malloc((size_t)(512 / 2 - 8));
if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
buf3R2 = (char *)malloc((size_t)(512 / 2 - 8));
if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned long)(512 - 1));
strncpy(buf2R1,(char const *)*(argv + 1),(size_t)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
free((void *)buf3R2);
......
basic-cwe-examples/.frama-c/cwe416.eva/nonterm.log
View file @ bf5deb7b
cwe416.c:27:[nonterm] warning: non-terminating function call
cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
stack: main
basic-cwe-examples/.frama-c/cwe416.parse/framac.ast
View file @ bf5deb7b
/* Generated by Frama-C */
#include "errno.h"
#include "fcntl.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
......@@ -14,16 +15,16 @@ int main(int argc, char **argv)
char *buf2R1;
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned long)512);
buf1R1 = (char *)malloc((size_t)512);
if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned long)512);
buf2R1 = (char *)malloc((size_t)512);
if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
buf2R2 = (char *)malloc((size_t)(512 / 2 - 8));
if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
buf3R2 = (char *)malloc((size_t)(512 / 2 - 8));
if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned long)(512 - 1));
strncpy(buf2R1,(char const *)*(argv + 1),(size_t)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
free((void *)buf3R2);
......
basic-cwe-examples/.frama-c/cwe588-precise.eva/alarms.csv 0 → 100644
View file @ bf5deb7b
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
basic-cwe-examples/.frama-c/cwe588-precise.eva/metrics.log 0 → 100644
View file @ bf5deb7b
[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%)
basic-cwe-examples/.frama-c/cwe588-precise.eva/nonterm.log 0 → 100644
View file @ bf5deb7b
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main
basic-cwe-examples/.frama-c/cwe588-precise.eva/warnings.log 0 → 100644
View file @ bf5deb7b
cwe588.c:10:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
basic-cwe-examples/.frama-c/cwe588-precise.parse/framac.ast 0 → 100644
View file @ bf5deb7b
/* 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;
}
basic-cwe-examples/.frama-c/cwe588-precise.parse/metrics.log 0 → 100644
View file @ bf5deb7b
[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
basic-cwe-examples/.frama-c/cwe588-precise.parse/warnings.log 0 → 100644
View file @ bf5deb7b
cwe588.c:9:[kernel:typing:incompatible-pointer-types] warning: casting function to struct foo *
basic-cwe-examples/.frama-c/cwe588.eva/alarms.csv 0 → 100644
View file @ bf5deb7b
directory file line function property kind status property
. cwe588.c 10 main mem_access Invalid or unreachable \valid(&foo->i)
basic-cwe-examples/.frama-c/cwe588.eva/metrics.log 0 → 100644
View file @ bf5deb7b
[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%)
basic-cwe-examples/.frama-c/cwe588.eva/nonterm.log 0 → 100644
View file @ bf5deb7b
cwe588.c:10:[nonterm:stmt] warning: non-terminating statement
stack: main