Skip to content
Snippets Groups Projects
Commit 665d5d74 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

fix symbolic paths and update oracles

parent 26509386
No related branches found
No related tags found
1 merge request!6Feature/new cgc
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 389 additions and 461 deletions
cgc-challenges/3D_Image_Toolkit/.frama-c/3D_Image_Toolkit.eva/alarms.csv
+ 1
− 1
View file @ 665d5d74
......@@ -110,7 +110,7 @@ directory file line function property kind status property
. main.c 200 cgc_menu mem_access Unknown \valid_read(px_list_0 + val)
. main.c 200 cgc_menu precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. main.c 200 cgc_menu precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
/home/andr/git/oscs-pub3/cgc-challenges/lib libcgc.c 42 cgc_receive precondition of read Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
CGC_LIB libcgc.c 42 cgc_receive precondition of read Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc string.h 92 memcpy precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 93 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 115 memset precondition Unknown valid_s: valid_or_empty(s, n)
......
cgc-challenges/3D_Image_Toolkit/.frama-c/3D_Image_Toolkit.parse/framac.ast
+ 14
− 13
View file @ 665d5d74
/* Generated by Frama-C */
#include "ctype.h"
#include "errno.h"
#include "fcntl.h"
#include "math.h"
......@@ -62,19 +63,6 @@ enum __anonenum_coords_3 {
Y = 1,
Z = 2
};
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
__attribute__((__noreturn__)) void cgc__terminate(unsigned int status);
int cgc_transmit(int fd, void const *buf, size_t count, size_t *tx_bytes);
......@@ -90,6 +78,19 @@ int cgc_deallocate(void *addr, size_t length);
int cgc_random(void *buf, size_t count, size_t *rnd_bytes);
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
int receive_bytes_iPcz(char *buffer, size_t count)
{
int __retres;
......
cgc-challenges/3D_Image_Toolkit/.frama-c/GNUmakefile
+ 2
− 1
View file @ 665d5d74
......@@ -19,7 +19,7 @@ CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
......@@ -30,6 +30,7 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = 3D_Image_Toolkit.eva
......
cgc-challenges/Accel/.frama-c/Accel.eva/alarms.csv
+ 190
− 190
View file @ 665d5d74
This diff is collapsed.
cgc-challenges/Accel/.frama-c/Accel.eva/metrics.log
+ 41
− 44
View file @ 665d5d74
......@@ -5,57 +5,54 @@ Semantically reached functions = 19
Coverage estimation = 37.3%
Unreached functions (32) =
</home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c>: cgc_eval_function;
cgc_infixtorpn; cgc_is_arg_arithmetic;
</home/andr/git/oscs-pub3/cgc-challenges/Accel/accelfunc.c>:
cgc_handle_op_abs; cgc_handle_op_add; cgc_handle_op_avg;
<accel.c>: cgc_eval_function; cgc_infixtorpn; cgc_is_arg_arithmetic;
<accelfunc.c>: cgc_handle_op_abs; cgc_handle_op_add; cgc_handle_op_avg;
cgc_handle_op_cos; cgc_handle_op_count; cgc_handle_op_ln;
cgc_handle_op_log10; cgc_handle_op_max; cgc_handle_op_median;
cgc_handle_op_min; cgc_handle_op_power; cgc_handle_op_product;
cgc_handle_op_quotient; cgc_handle_op_sin; cgc_handle_op_sqrt;
cgc_handle_op_stddev; cgc_handle_op_subtract; cgc_handle_op_sum;
</home/andr/git/oscs-pub3/cgc-challenges/Accel/accelio.c>:
cgc_sanitize_formula;
</home/andr/git/oscs-pub3/cgc-challenges/Accel/atof.c>: cgc_atof;
</home/andr/git/oscs-pub3/cgc-challenges/Accel/queue.c>: cgc_clear_queue;
cgc_dequeue_copy; cgc_enqueue; cgc_enqueue_copy;
</home/andr/git/oscs-pub3/cgc-challenges/Accel/stack.c>: cgc_clear_stack;
cgc_peek_top; cgc_pop_copy; cgc_push; cgc_push_copy;
<accelio.c>: cgc_sanitize_formula;
<atof.c>: cgc_atof;
<queue.c>: cgc_clear_queue; cgc_dequeue_copy; cgc_enqueue;
cgc_enqueue_copy;
<stack.c>: cgc_clear_stack; cgc_peek_top; cgc_pop_copy; cgc_push;
cgc_push_copy;
[metrics] References to non-analyzed functions
------------------------------------
Function cgc_eval_formula calls cgc_push_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:395)
Function cgc_eval_formula calls cgc_infixtorpn (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:396)
Function cgc_eval_formula calls cgc_dequeue_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:405)
Function cgc_eval_formula calls cgc_push (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:409)
Function cgc_eval_formula calls cgc_eval_function (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:413)
Function cgc_eval_formula calls cgc_push_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:417)
Function cgc_eval_formula calls cgc_push_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:435)
Function cgc_eval_formula calls cgc_push_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:437)
Function cgc_eval_formula calls cgc_push_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:444)
Function cgc_eval_formula calls cgc_pop_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:455)
Function cgc_eval_formula calls cgc_atof (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:459)
Function cgc_eval_formula calls cgc_clear_queue (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:468)
Function cgc_eval_formula calls cgc_clear_queue (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:469)
Function cgc_eval_formula calls cgc_clear_stack (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:470)
Function cgc_eval_formula calls cgc_pop_copy (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:472)
Initializer of operators references cgc_handle_op_avg (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:60)
Initializer of operators references cgc_handle_op_count (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:61)
Initializer of operators references cgc_handle_op_max (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:62)
Initializer of operators references cgc_handle_op_median (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:63)
Initializer of operators references cgc_handle_op_min (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:64)
Initializer of operators references cgc_handle_op_stddev (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:65)
Initializer of operators references cgc_handle_op_abs (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:66)
Initializer of operators references cgc_handle_op_add (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:67)
Initializer of operators references cgc_handle_op_cos (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:68)
Initializer of operators references cgc_handle_op_ln (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:69)
Initializer of operators references cgc_handle_op_log10 (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:70)
Initializer of operators references cgc_handle_op_power (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:71)
Initializer of operators references cgc_handle_op_product (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:72)
Initializer of operators references cgc_handle_op_quotient (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:73)
Initializer of operators references cgc_handle_op_sin (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:74)
Initializer of operators references cgc_handle_op_sqrt (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:75)
Initializer of operators references cgc_handle_op_subtract (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:76)
Initializer of operators references cgc_handle_op_sum (at /home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:77)
Function cgc_eval_formula calls cgc_push_copy (at accel.c:395)
Function cgc_eval_formula calls cgc_infixtorpn (at accel.c:396)
Function cgc_eval_formula calls cgc_dequeue_copy (at accel.c:405)
Function cgc_eval_formula calls cgc_push (at accel.c:409)
Function cgc_eval_formula calls cgc_eval_function (at accel.c:413)
Function cgc_eval_formula calls cgc_push_copy (at accel.c:417)
Function cgc_eval_formula calls cgc_push_copy (at accel.c:435)
Function cgc_eval_formula calls cgc_push_copy (at accel.c:437)
Function cgc_eval_formula calls cgc_push_copy (at accel.c:444)
Function cgc_eval_formula calls cgc_pop_copy (at accel.c:455)
Function cgc_eval_formula calls cgc_atof (at accel.c:459)
Function cgc_eval_formula calls cgc_clear_queue (at accel.c:468)
Function cgc_eval_formula calls cgc_clear_queue (at accel.c:469)
Function cgc_eval_formula calls cgc_clear_stack (at accel.c:470)
Function cgc_eval_formula calls cgc_pop_copy (at accel.c:472)
Initializer of operators references cgc_handle_op_avg (at accel.c:60)
Initializer of operators references cgc_handle_op_count (at accel.c:61)
Initializer of operators references cgc_handle_op_max (at accel.c:62)
Initializer of operators references cgc_handle_op_median (at accel.c:63)
Initializer of operators references cgc_handle_op_min (at accel.c:64)
Initializer of operators references cgc_handle_op_stddev (at accel.c:65)
Initializer of operators references cgc_handle_op_abs (at accel.c:66)
Initializer of operators references cgc_handle_op_add (at accel.c:67)
Initializer of operators references cgc_handle_op_cos (at accel.c:68)
Initializer of operators references cgc_handle_op_ln (at accel.c:69)
Initializer of operators references cgc_handle_op_log10 (at accel.c:70)
Initializer of operators references cgc_handle_op_power (at accel.c:71)
Initializer of operators references cgc_handle_op_product (at accel.c:72)
Initializer of operators references cgc_handle_op_quotient (at accel.c:73)
Initializer of operators references cgc_handle_op_sin (at accel.c:74)
Initializer of operators references cgc_handle_op_sqrt (at accel.c:75)
Initializer of operators references cgc_handle_op_subtract (at accel.c:76)
Initializer of operators references cgc_handle_op_sum (at accel.c:77)
[metrics] Statements analyzed by Eva
--------------------------
943 stmts in analyzed functions, 817 stmts analyzed (86.6%)
......
cgc-challenges/Accel/.frama-c/Accel.eva/warnings.log
+ 28
− 39
View file @ 665d5d74
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:157:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause *
accel.c:157:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause *
(dest + (0 .. strlen{Old}(src))).
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:157:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause \result.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accelio.c:77:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accelio.c:82:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:217:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause *
accel.c:157:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause \result.
accelio.c:77:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
accelio.c:82:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
accel.c:217:[eva:garbled-mix] warning: The specification of function strcpy has generated a garbled mix for assigns clause assigns clause *
(dest + (0 .. strlen{Old}(src))).
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:220:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:205:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:135:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:137:[eva:garbled-mix] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:179:[eva:garbled-mix] warning: The specification of function printf_va_6 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:182:[eva:garbled-mix] warning: The specification of function printf_va_7 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:185:[eva:garbled-mix] warning: The specification of function printf_va_8 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:188:[eva:garbled-mix] warning: The specification of function printf_va_9 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:191:[eva:garbled-mix] warning: The specification of function printf_va_10 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:170:[eva:garbled-mix] warning: The specification of function printf_va_4 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:173:[eva:garbled-mix] warning: The specification of function printf_va_5 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:195:[eva:garbled-mix] warning: The specification of function printf_va_11 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
accel.c:220:[eva:garbled-mix] warning: The specification of function toupper has generated a garbled mix for assigns clause assigns clause \result.
accel.c:205:[eva:garbled-mix] warning: The specification of function printf_va_1 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:135:[eva:garbled-mix] warning: The specification of function printf_va_2 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:137:[eva:garbled-mix] warning: The specification of function printf_va_3 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:179:[eva:garbled-mix] warning: The specification of function printf_va_6 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:182:[eva:garbled-mix] warning: The specification of function printf_va_7 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:185:[eva:garbled-mix] warning: The specification of function printf_va_8 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:188:[eva:garbled-mix] warning: The specification of function printf_va_9 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:191:[eva:garbled-mix] warning: The specification of function printf_va_10 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:170:[eva:garbled-mix] warning: The specification of function printf_va_4 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:173:[eva:garbled-mix] warning: The specification of function printf_va_5 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
main.c:195:[eva:garbled-mix] warning: The specification of function printf_va_11 has generated a garbled mix for assigns clause assigns clause __fc_stdout->__fc_FILE_data.
[eva:garbled-mix] warning: Garbled mix generated during analysis:
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:153}) }}
(origin: Misaligned {accel.c:153}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:114}) }}
(origin: Misaligned {accel.c:114}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:116}) }}
(origin: Misaligned {accel.c:116}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:120}) }}
(origin: Misaligned {accel.c:120}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:122}) }}
(origin: Misaligned {accel.c:122}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:124}) }}
(origin: Misaligned {accel.c:124}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:132}) }}
(origin: Misaligned {accel.c:132}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:179}) }}
(origin: Misaligned {accel.c:179}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:180}) }}
(origin: Misaligned {accel.c:180}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:146}) }}
(origin: Misaligned {accel.c:146}) }}
{{ garbled mix of &{__malloc_w_cgc_set_cell_l153}
(origin: Misaligned
{/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:147}) }}
(origin: Misaligned {accel.c:147}) }}
cgc-challenges/Accel/.frama-c/Accel.parse/framac.ast
+ 13
− 13
View file @ 665d5d74
......@@ -64,19 +64,6 @@ struct cell {
char *formula ;
};
typedef struct cell cell_t;
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
__attribute__((__noreturn__)) void cgc__terminate(unsigned int status);
int cgc_transmit(int fd, void const *buf, size_t count, size_t *tx_bytes);
......@@ -92,6 +79,19 @@ int cgc_deallocate(void *addr, size_t length);
int cgc_random(void *buf, size_t count, size_t *rnd_bytes);
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
int receive_bytes_iPcz(char *buffer, size_t count)
{
int __retres;
......
cgc-challenges/Accel/.frama-c/Accel.parse/warnings.log
+ 5
− 5
View file @ 665d5d74
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accel.c:372:[kernel:typing:no-proto] warning: Calling function cgc_clear_stack that is declared without prototype.
accel.c:372:[kernel:typing:no-proto] warning: Calling function cgc_clear_stack that is declared without prototype.
Its formals will be inferred from actual arguments
/home/andr/git/oscs-pub3/cgc-challenges/Accel/accelfunc.c:53:[kernel:typing:no-proto] warning: Calling function cgc_clear_stack that is declared without prototype.
accelfunc.c:53:[kernel:typing:no-proto] warning: Calling function cgc_clear_stack that is declared without prototype.
Its formals will be inferred from actual arguments
/home/andr/git/oscs-pub3/cgc-challenges/Accel/ftoa.c:50:[kernel:parser:decimal-float] warning: Floating-point constant 0.001 is not represented exactly. Will use 0x1.0624dd2f1a9fcp-10.
ftoa.c:50:[kernel:parser:decimal-float] warning: Floating-point constant 0.001 is not represented exactly. Will use 0x1.0624dd2f1a9fcp-10.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:51:[kernel:typing:no-proto] warning: Calling function cgc_print_assigned_cells that is declared without prototype.
main.c:51:[kernel:typing:no-proto] warning: Calling function cgc_print_assigned_cells that is declared without prototype.
Its formals will be inferred from actual arguments
/home/andr/git/oscs-pub3/cgc-challenges/Accel/main.c:165:[kernel:typing:no-proto] warning: Calling function cgc_init_sheet that is declared without prototype.
main.c:165:[kernel:typing:no-proto] warning: Calling function cgc_init_sheet that is declared without prototype.
Its formals will be inferred from actual arguments
cgc-challenges/Accel/.frama-c/GNUmakefile
+ 2
− 1
View file @ 665d5d74
......@@ -18,7 +18,7 @@ CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
......@@ -30,6 +30,7 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = Accel.eva
......
cgc-challenges/HackMan/.frama-c/GNUmakefile
+ 2
− 1
View file @ 665d5d74
......@@ -22,7 +22,7 @@ CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
......@@ -34,6 +34,7 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = HackMan.eva
......
cgc-challenges/HackMan/.frama-c/HackMan.eva/alarms.csv
+ 7
− 7
View file @ 665d5d74
directory file line function property kind status property
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 65 cgc_read_until initialization Unknown \initialized(tmp_0)
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 68 cgc_read_until mem_access Unknown \valid(c - 1)
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 88 cgc_parse_input precondition of isalpha Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 89 cgc_parse_input precondition of tolower Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 145 cgc_record_winner precondition of dprintf_va_6 Unknown valid_read_string(param0)
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 145 dprintf_va_6 precondition Unknown valid_read_string(param0)
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src main.c 149 cgc_record_winner signed_overflow Unknown total + 1 ≤ 2147483647
FRAMAC_SHARE/libc ctype.h 55 isalpha precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
FRAMAC_SHARE/libc ctype.h 203 tolower precondition Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
src main.c 65 cgc_read_until initialization Unknown \initialized(tmp_0)
src main.c 68 cgc_read_until mem_access Unknown \valid(c - 1)
src main.c 88 cgc_parse_input precondition of isalpha Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
src main.c 89 cgc_parse_input precondition of tolower Unknown c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1
src main.c 145 cgc_record_winner precondition of dprintf_va_6 Unknown valid_read_string(param0)
src main.c 145 dprintf_va_6 precondition Unknown valid_read_string(param0)
src main.c 149 cgc_record_winner signed_overflow Unknown total + 1 ≤ 2147483647
cgc-challenges/HackMan/.frama-c/HackMan.eva/nonterm.log
+ 4
− 5
View file @ 665d5d74
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src/main.c:179:[nonterm] warning: unreachable implicit return
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src/main.c:223:[nonterm] warning: non-terminating function call
stack: cgc_play_game :: /home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src/main.c:277 <-
main
/home/dario/git/open-source-case-studies/cgc-challenges/HackMan/src/main.c:271:[nonterm] warning: non-terminating loop
src/main.c:179:[nonterm] warning: unreachable implicit return
src/main.c:223:[nonterm] warning: non-terminating function call
stack: cgc_play_game :: src/main.c:277 <- main
src/main.c:271:[nonterm] warning: non-terminating loop
stack: main
cgc-challenges/Monster_Game/.frama-c/GNUmakefile
+ 2
− 1
View file @ 665d5d74
......@@ -20,7 +20,7 @@ CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
......@@ -35,6 +35,7 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = Monster_Game.eva
......
cgc-challenges/Monster_Game/.frama-c/Monster_Game.parse/metrics.log
+ 0
− 64
View file @ 665d5d74
[metrics] Defined functions (71)
======================
cgc_AddUser (0 call); cgc_ChangeMode (0 call); cgc_ChangeOwner (0 call);
cgc_ChangePasswd (0 call); cgc_CheckPasswd (0 call);
cgc_ClearFsError (22 calls); cgc_CreateEmptyFile (1 call);
cgc_DeleteFile (12 calls); cgc_DeleteUser (0 call);
cgc_DestroyFilesystem (1 call); cgc_FindFile (4 calls);
cgc_FsError (0 call); cgc_InitFilesystem (0 call); cgc_InitPasswd (1 call);
cgc_ListFiles (0 call); cgc_Login (9 calls); cgc_Logout (14 calls);
cgc_RenameFile (3 calls); cgc_SetFsError (102 calls); cgc_Uid (0 call);
cgc_UserExists (2 calls); cgc__terminate (17 calls);
cgc_add_queue (4 calls); cgc_allocate (0 call); cgc_capture_boss (1 call);
cgc_capture_monster (1 call); cgc_change_monster_name (1 call);
cgc_check_adjacent (1 call); cgc_check_egg (1 call);
cgc_check_timeout (1 call); cgc_copy_cgc_fd_set (2 calls);
cgc_copy_os_fd_set (2 calls); cgc_daboss (1 call); cgc_deallocate (0 call);
cgc_dequeue (2 calls); cgc_fclose (34 calls); cgc_fdwait (0 call);
cgc_fgets (5 calls); cgc_fight (1 call); cgc_find_path (2 calls);
cgc_fopen (9 calls); cgc_fread (0 call); cgc_fwrite (8 calls);
cgc_generate_boss (1 call); cgc_generate_map (1 call);
cgc_generate_monster (2 calls); cgc_generate_player (1 call);
cgc_initialize_map (1 call); cgc_initialize_queue_matrix (1 call);
cgc_movement_loop (1 call); cgc_oneup_monster (2 calls);
cgc_place_marker (1 call); cgc_print_map (4 calls);
cgc_print_monster (6 calls); cgc_print_player (1 call); cgc_prng (2 calls);
cgc_random (0 call); cgc_random_in_range (0 call); cgc_read_line (10 calls);
cgc_read_line_u (1 call); cgc_receive (2 calls);
cgc_reset_monsters (4 calls); cgc_seed_prng (0 call);
cgc_seed_prng_array (1 call); cgc_select_monster (2 calls);
cgc_select_name (2 calls); cgc_set_marker (10 calls); cgc_transmit (0 call);
cgc_try_init_prng (1 call); cgc_update_page_index (21 calls); main (0 call);
Undefined functions (6)
=======================
cgc_aes_get_bytes (1 call); cgc_init_prng (1 call);
cgc_initialize_flag_page (0 call); cgc_puts (1 call); cgc_sprintf (5 calls);
seed_prng (0 call);
'Extern' global variables (0)
=============================
Potential entry points (19)
===========================
cgc_AddUser; cgc_ChangeMode; cgc_ChangeOwner; cgc_ChangePasswd;
cgc_CheckPasswd; cgc_DeleteUser; cgc_FsError; cgc_InitFilesystem;
cgc_ListFiles; cgc_Uid; cgc_allocate; cgc_deallocate; cgc_fdwait;
cgc_fread; cgc_random; cgc_random_in_range; cgc_seed_prng; cgc_transmit;
main;
Global metrics
==============
Sloc = 2197
Decision point = 387
Global variables = 15
If = 383
Loop = 46
Goto = 178
Assignment = 704
Exit point = 71
Function = 77
Function call = 625
Pointer dereferencing = 617
Cyclomatic complexity = 458
cgc-challenges/Monster_Game/.frama-c/Monster_Game.parse/warnings.log
+ 1
− 0
View file @ 665d5d74
[kernel] warning: attempting to save on non-zero exit code: modifying filename into `/home/andr/git/oscs-internal/cgc-challenges/Monster_Game/.frama-c/Monster_Game.parse/framac.sav.error'.
cgc-challenges/chess_mimic/.frama-c/GNUmakefile
+ 2
− 1
View file @ 665d5d74
......@@ -22,7 +22,7 @@ CPPFLAGS += \
## General flags
FCFLAGS += \
-add-symbolic-path=..:. \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
......@@ -35,6 +35,7 @@ EVAFLAGS += \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = chess_mimic.eva
......
cgc-challenges/chess_mimic/.frama-c/chess_mimic.eva/alarms.csv
+ 60
− 60
View file @ 665d5d74
directory file line function property kind status property
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece initialization Unknown \initialized(&loc.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece initialization Unknown \initialized(&loc.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece index_bound Unknown 0 ≤ loc.x
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece index_bound Unknown loc.x < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece index_bound Unknown 0 ≤ loc.y
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 129 cgc_getPiece index_bound Unknown loc.y < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 164 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 164 cgc_checkNoCollision initialization Unknown \initialized(&move.src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 166 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 166 cgc_checkNoCollision initialization Unknown \initialized(&move.src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 198 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 198 cgc_checkNoCollision initialization Unknown \initialized(&move.src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&dst.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 241 cgc_checkNoCollision index_bound Unknown square_cnt < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 244 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 244 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 246 cgc_checkNoCollision index_bound Unknown square_cnt < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 249 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 249 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 251 cgc_checkNoCollision index_bound Unknown square_cnt < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 254 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 254 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 256 cgc_checkNoCollision index_bound Unknown square_cnt < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 272 cgc_checkNoCollision initialization Unknown \initialized(&squares[i_4][0])
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 272 cgc_checkNoCollision initialization Unknown \initialized(&squares[i_4][1])
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 352 cgc_performMove initialization Unknown \initialized(&dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 352 cgc_performMove initialization Unknown \initialized(&dst.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 360 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 360 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 373 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 373 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 389 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 391 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 400 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 417 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 419 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 428 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 444 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 445 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 457 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 459 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 480 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 481 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 497 cgc_performMove initialization Unknown \initialized(&src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 497 cgc_performMove initialization Unknown \initialized(&src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 515 cgc_swap initialization Unknown \initialized(&move.dst.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 515 cgc_swap initialization Unknown \initialized(&move.dst.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 515 cgc_swap index_bound Unknown move.dst.x < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 515 cgc_swap index_bound Unknown move.dst.y < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 516 cgc_swap initialization Unknown \initialized(&move.src.x)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 516 cgc_swap initialization Unknown \initialized(&move.src.y)
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 516 cgc_swap index_bound Unknown move.src.x < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 516 cgc_swap index_bound Unknown move.src.y < 8
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 609 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.src.x ≤ 9
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 615 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.src.y ≤ 9
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 621 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.dst.x ≤ 9
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src service.c 627 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.dst.y ≤ 9
src service.c 129 cgc_getPiece initialization Unknown \initialized(&loc.x)
src service.c 129 cgc_getPiece initialization Unknown \initialized(&loc.y)
src service.c 129 cgc_getPiece index_bound Unknown 0 ≤ loc.x
src service.c 129 cgc_getPiece index_bound Unknown loc.x < 8
src service.c 129 cgc_getPiece index_bound Unknown 0 ≤ loc.y
src service.c 129 cgc_getPiece index_bound Unknown loc.y < 8
src service.c 164 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.x)
src service.c 164 cgc_checkNoCollision initialization Unknown \initialized(&move.src.x)
src service.c 166 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.y)
src service.c 166 cgc_checkNoCollision initialization Unknown \initialized(&move.src.y)
src service.c 198 cgc_checkNoCollision initialization Unknown \initialized(&move.dst.y)
src service.c 198 cgc_checkNoCollision initialization Unknown \initialized(&move.src.y)
src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&dst.y)
src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&src.y)
src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
src service.c 239 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
src service.c 241 cgc_checkNoCollision index_bound Unknown square_cnt < 8
src service.c 244 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
src service.c 244 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
src service.c 246 cgc_checkNoCollision index_bound Unknown square_cnt < 8
src service.c 249 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
src service.c 249 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
src service.c 251 cgc_checkNoCollision index_bound Unknown square_cnt < 8
src service.c 254 cgc_checkNoCollision initialization Unknown \initialized(&dst.x)
src service.c 254 cgc_checkNoCollision initialization Unknown \initialized(&src.x)
src service.c 256 cgc_checkNoCollision index_bound Unknown square_cnt < 8
src service.c 272 cgc_checkNoCollision initialization Unknown \initialized(&squares[i_4][0])
src service.c 272 cgc_checkNoCollision initialization Unknown \initialized(&squares[i_4][1])
src service.c 352 cgc_performMove initialization Unknown \initialized(&dst.x)
src service.c 352 cgc_performMove initialization Unknown \initialized(&dst.y)
src service.c 360 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 360 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 373 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 373 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 389 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 391 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 400 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 417 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 419 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 428 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 444 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 445 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 457 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 459 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 480 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 481 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 497 cgc_performMove initialization Unknown \initialized(&src.x)
src service.c 497 cgc_performMove initialization Unknown \initialized(&src.y)
src service.c 515 cgc_swap initialization Unknown \initialized(&move.dst.x)
src service.c 515 cgc_swap initialization Unknown \initialized(&move.dst.y)
src service.c 515 cgc_swap index_bound Unknown move.dst.x < 8
src service.c 515 cgc_swap index_bound Unknown move.dst.y < 8
src service.c 516 cgc_swap initialization Unknown \initialized(&move.src.x)
src service.c 516 cgc_swap initialization Unknown \initialized(&move.src.y)
src service.c 516 cgc_swap index_bound Unknown move.src.x < 8
src service.c 516 cgc_swap index_bound Unknown move.src.y < 8
src service.c 609 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.src.x ≤ 9
src service.c 615 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.src.y ≤ 9
src service.c 621 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.dst.x ≤ 9
src service.c 627 cgc_parseUserInput user assertion Unknown 0 ≤ tmp.dst.y ≤ 9
cgc-challenges/chess_mimic/.frama-c/chess_mimic.eva/nonterm.log
+ 2
− 2
View file @ 665d5d74
/home/dario/git/open-source-case-studies/cgc-challenges/lib/libcgc.c:24:[nonterm] warning: unreachable implicit return
/home/dario/git/open-source-case-studies/cgc-challenges/chess_mimic/src/service.c:660:[nonterm] warning: non-terminating loop
CGC_LIB/libcgc.c:24:[nonterm] warning: unreachable implicit return
src/service.c:660:[nonterm] warning: non-terminating loop
stack: main
cgc-challenges/chess_mimic/.frama-c/chess_mimic.parse/framac.ast
+ 13
− 13
View file @ 665d5d74
......@@ -39,19 +39,6 @@ struct Move {
Location dst ;
};
typedef struct Move Move;
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
__attribute__((__noreturn__)) void cgc__terminate(unsigned int status);
int cgc_transmit(int fd, void const *buf, size_t count, size_t *tx_bytes);
......@@ -67,6 +54,19 @@ int cgc_deallocate(void *addr, size_t length);
int cgc_random(void *buf, size_t count, size_t *rnd_bytes);
int receive_bytes_iPcz(char *buffer, size_t count);
int __prng_state;
/*@ assigns __prng_state;
assigns __prng_state \from seedValue; */
void seed_prng(uint32_t seedValue);
/*@ assigns \result, __prng_state;
assigns \result \from __prng_state;
assigns __prng_state \from __prng_state;
*/
uint32_t cgc_prng(void);
int receive_bytes_iPcz(char *buffer, size_t count)
{
int __retres;
......
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