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

Remove files with make clean

parent 804646b3
Pipeline #33140 failed with stage
in 19 seconds
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
20 stmts in analyzed functions, 20 stmts analyzed (100.0%)
main: 20 stmts out of 20 (100.0%)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
struct _board_square_t {
char color ;
};
typedef struct _board_square_t board_square_t;
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_1(char const * __restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
\from (indirect: __fc_stdin->__fc_FILE_id),
(indirect: __fc_stdin->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdin->__fc_FILE_data
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
assigns *param0
\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);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
assigns \result
\from (indirect: __fc_stdout->__fc_FILE_id),
(indirect: __fc_stdout->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdout->__fc_FILE_data
\from (indirect: __fc_stdout->__fc_FILE_id),
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
*/
int printf_va_2(char const * __restrict format);
/*@ requires valid_read_string(format);
requires \valid(param0);
ensures \initialized(param0);
assigns \result, __fc_stdin->__fc_FILE_data, *param0;
assigns \result
\from (indirect: __fc_stdin->__fc_FILE_id),
(indirect: __fc_stdin->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns __fc_stdin->__fc_FILE_data
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
assigns *param0
\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);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
/*@ requires valid_read_string(format);
assigns \result, stream->__fc_FILE_data;
assigns \result
\from (indirect: stream->__fc_FILE_id),
(indirect: stream->__fc_FILE_data),
(indirect: *(format + (0 ..)));
assigns stream->__fc_FILE_data
\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 main(void)
{
int __retres;
int m;
int n;
int error;
board_square_t *board;
printf("Please specify the board height: \n"); /* printf_va_1 */
error = scanf("%d",& m); /* scanf_va_1 */
if (-1 == error) {
fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
exit(1);
}
printf("Please specify the board width: \n"); /* printf_va_2 */
error = scanf("%d",& n); /* scanf_va_2 */
if (-1 == error) {
fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_2 */
exit(1);
}
if (m > 100) goto _LOR;
else
if (n > 100) {
_LOR:
{
fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_3 */
exit(1);
}
}
board = (board_square_t *)malloc((unsigned long)(m * n) * sizeof(board_square_t));
free((void *)board);
__retres = 0;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 20
Decision point = 4
Global variables = 0
If = 4
Loop = 0
Goto = 1
Assignment = 4
Exit point = 1
Function = 1
Function call = 12
Pointer dereferencing = 0
Cyclomatic complexity = 5
directory file line function property kind status property
. cwe416.c 27 main dangling_pointer Invalid or unreachable ¬\dangling(&buf2R1)
. cwe416.c 27 main mem_access Unknown \valid_read(argv + 1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
main: 14 stmts out of 19 (73.7%)
cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
stack: main
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
#include "unistd.h"
int main(int argc, char **argv)
{
int __retres;
char *buf1R1;
char *buf2R1;
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned long)512);
if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned long)512);
if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned long)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
free((void *)buf3R2);
__retres = 0;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 19
Decision point = 4
Global variables = 0
If = 4
Loop = 0
Goto = 0
Assignment = 5
Exit point = 1
Function = 1
Function call = 13
Pointer dereferencing = 1
Cyclomatic complexity = 5
directory file line function property kind status property
. cwe416.c 27 main dangling_pointer Invalid or unreachable ¬\dangling(&buf2R1)
. cwe416.c 27 main mem_access Unknown \valid_read(argv + 1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 1 (out of 1)
Semantically reached functions = 1
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
19 stmts in analyzed functions, 14 stmts analyzed (73.7%)
main: 14 stmts out of 19 (73.7%)
cwe416.c:27:[nonterm:stmt] warning: non-terminating function call
stack: main
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
#include "stdlib.h"
#include "string.h"
#include "strings.h"
#include "unistd.h"
int main(int argc, char **argv)
{
int __retres;
char *buf1R1;
char *buf2R1;
char *buf2R2;
char *buf3R2;
buf1R1 = (char *)malloc((unsigned long)512);
if (! buf1R1) exit(1);
buf2R1 = (char *)malloc((unsigned long)512);
if (! buf2R1) exit(1);
free((void *)buf2R1);
buf2R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
if (! buf2R2) exit(1);
buf3R2 = (char *)malloc((unsigned long)(512 / 2 - 8));
if (! buf3R2) exit(1);
strncpy(buf2R1,(char const *)*(argv + 1),(unsigned long)(512 - 1));
free((void *)buf1R1);
free((void *)buf2R2);
free((void *)buf3R2);
__retres = 0;
return __retres;
}
[metrics] Defined functions (1)
=====================
main (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 19
Decision point = 4
Global variables = 0
If = 4
Loop = 0
Goto = 0
Assignment = 5
Exit point = 1
Function = 1
Function call = 13
Pointer dereferencing = 1
Cyclomatic complexity = 5
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