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

Merge branch 'add-kgflags' into 'master'

[kgflags] add new case study

See merge request !11
parents b503aa14 d82cd6ac
Pipeline #32510 passed with stage
in 76 minutes and 16 seconds
......@@ -62,6 +62,7 @@ TARGETS=\
icpc \
itc-benchmarks \
jsmn \
kgflags \
khash \
kilo \
libmodbus \
......
......@@ -133,6 +133,7 @@ when available. We also summarize the license of each directory below.
- `icpc`: Unlicense
- `itc-benchmarks`: BSD 2-clause, see `COPYING`
- `jsmn`: MIT
- `kgflags`: MIT, see `LICENSE`
- `khash`: MIT
- `kilo`: BSD 2-clause "Simplified"
(see https://github.com/antirez/kilo/blob/master/LICENSE)
......
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
MACHDEP = x86_64
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
## General flags
FCFLAGS += \
-main eva_main \
-add-symbolic-path=..:. \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## GUI-only flags
FCGUIFLAGS += \
## Analysis targets (suffixed with .eva)
TARGETS = kgflags-simple.eva kgflags-full_api.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
kgflags-simple.parse: \
fc_stubs.c \
../examples/simple.c \
kgflags-full_api.parse: \
fc_stubs.c \
../examples/full_api.c \
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
###############################################################################
# optional, for OSCS
-include ../../Makefile.common
// Stub for a main function which reads arguments from the command line, to be
// used by the Eva plug-in.
// This stub emulates non-deterministic input of up to 5 arguments, each up
// to 256 characters long. This is sufficient to ensure arbitrary input in
// virtually every case.
// Do not forget to add option '-main eva_main' in order to use this stub.
#ifdef __FRAMAC__
# include "__fc_builtin.h"
int main(int, char **);
static volatile int nondet;
int eva_main() {
int argc = Frama_C_interval(0, 5);
char argv0[256], argv1[256], argv2[256], argv3[256], argv4[256];
char *argv[6] = {argv0, argv1, argv2, argv3, argv4, 0};
//@ loop unroll 5;
for (int i = 0; i < 5; i++) {
Frama_C_make_unknown(argv[i], 255);
argv[i][255] = 0;
}
return main(argc, argv);
}
#endif // __FRAMAC__
directory file line function property kind status property
. kgflags.h 402 kgflags_print_errors initialization Unknown \initialized(&err->kind)
. kgflags.h 404 fprintf_va_1 precondition Unknown valid_read_string(param1)
. kgflags.h 404 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 404 kgflags_print_errors precondition of fprintf_va_1 Unknown valid_read_string(param1)
. kgflags.h 408 fprintf_va_2 precondition Unknown valid_read_string(param1)
. kgflags.h 408 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 408 kgflags_print_errors precondition of fprintf_va_2 Unknown valid_read_string(param1)
. kgflags.h 412 fprintf_va_3 precondition Unknown valid_read_string(param1)
. kgflags.h 412 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 412 kgflags_print_errors precondition of fprintf_va_3 Unknown valid_read_string(param1)
. kgflags.h 416 fprintf_va_4 precondition Unknown valid_read_string(param1)
. kgflags.h 416 fprintf_va_4 precondition Unknown valid_read_string(param2)
. kgflags.h 416 kgflags_print_errors initialization Unknown \initialized(&err->arg)
. kgflags.h 416 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 416 kgflags_print_errors precondition of fprintf_va_4 Unknown valid_read_string(param1)
. kgflags.h 416 kgflags_print_errors precondition of fprintf_va_4 Unknown valid_read_string(param2)
. kgflags.h 420 fprintf_va_5 precondition Unknown valid_read_string(param1)
. kgflags.h 420 fprintf_va_5 precondition Unknown valid_read_string(param2)
. kgflags.h 420 kgflags_print_errors initialization Unknown \initialized(&err->arg)
. kgflags.h 420 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 420 kgflags_print_errors precondition of fprintf_va_5 Unknown valid_read_string(param1)
. kgflags.h 420 kgflags_print_errors precondition of fprintf_va_5 Unknown valid_read_string(param2)
. kgflags.h 432 fprintf_va_8 precondition Unknown valid_read_string(param1)
. kgflags.h 432 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 432 kgflags_print_errors precondition of fprintf_va_8 Unknown valid_read_string(param1)
. kgflags.h 436 fprintf_va_9 precondition Unknown valid_read_string(param1)
. kgflags.h 436 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 436 kgflags_print_errors precondition of fprintf_va_9 Unknown valid_read_string(param1)
. kgflags.h 440 fprintf_va_10 precondition Unknown valid_read_string(param1)
. kgflags.h 440 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 440 kgflags_print_errors precondition of fprintf_va_10 Unknown valid_read_string(param1)
. kgflags.h 467 fprintf_va_16 precondition Unknown valid_read_string(param1)
. kgflags.h 467 fprintf_va_16 precondition Unknown valid_read_string(param3)
. kgflags.h 467 kgflags_print_usage precondition of fprintf_va_16 Unknown valid_read_string(param1)
. kgflags.h 467 kgflags_print_usage precondition of fprintf_va_16 Unknown valid_read_string(param3)
. kgflags.h 475 fprintf_va_18 precondition Unknown valid_read_string(param1)
. kgflags.h 475 kgflags_print_usage precondition of fprintf_va_18 Unknown valid_read_string(param1)
. kgflags.h 482 fprintf_va_20 precondition Unknown valid_read_string(param1)
. kgflags.h 482 kgflags_print_usage precondition of fprintf_va_20 Unknown valid_read_string(param1)
. kgflags.h 489 fprintf_va_22 precondition Unknown valid_read_string(param1)
. kgflags.h 489 kgflags_print_usage precondition of fprintf_va_22 Unknown valid_read_string(param1)
. kgflags.h 493 fprintf_va_23 precondition Unknown valid_read_string(param1)
. kgflags.h 493 kgflags_print_usage precondition of fprintf_va_23 Unknown valid_read_string(param1)
. kgflags.h 497 fprintf_va_24 precondition Unknown valid_read_string(param1)
. kgflags.h 497 kgflags_print_usage precondition of fprintf_va_24 Unknown valid_read_string(param1)
. kgflags.h 504 fprintf_va_25 precondition Unknown valid_read_string(param0)
. kgflags.h 504 kgflags_print_usage precondition of fprintf_va_25 Unknown valid_read_string(param0)
. kgflags.h 522 kgflags_string_array_get_item mem_access Unknown \valid_read(arr->_items + at)
. kgflags.h 533 kgflags_int_array_get_item mem_access Unknown \valid_read(arr->_items + at)
. kgflags.h 550 kgflags_double_array_get_item mem_access Unknown \valid_read(arr->_items + at)
. kgflags.h 608 _kgflags_get_flag precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
. kgflags.h 608 _kgflags_get_flag precondition of strcmp Unknown valid_string_s2: valid_read_string(s2)
. kgflags.h 611 _kgflags_get_flag precondition of strstr Unknown valid_string_haystack: valid_read_string(haystack)
. kgflags.h 612 _kgflags_get_flag precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
. kgflags.h 612 _kgflags_get_flag precondition of strcmp Unknown valid_string_s2: valid_read_string(s2)
. kgflags.h 626 _kgflags_parse_int precondition of strtol Unknown valid_nptr: \valid_read(nptr)
. kgflags.h 627 _kgflags_parse_int ptr_comparison Unknown \pointer_comparable((void *)end, (void *)str)
. kgflags.h 627 _kgflags_parse_int mem_access Unknown \valid_read(end)
. kgflags.h 639 _kgflags_parse_double precondition of strtod Unknown valid_nptr: \valid_read(nptr)
. kgflags.h 640 _kgflags_parse_double ptr_comparison Unknown \pointer_comparable((void *)end, (void *)str)
. kgflags.h 640 _kgflags_parse_double mem_access Unknown \valid_read(end)
. kgflags.h 641 _kgflags_parse_double is_nan_or_infinite Unknown \is_finite(res)
. kgflags.h 641 _kgflags_parse_double is_nan_or_infinite Invalid or unreachable \is_finite((float)INFINITY)
. kgflags.h 675 _kgflags_assign_default_values mem_access Unknown \valid(flag->result.bool_value)
. kgflags.h 680 _kgflags_assign_default_values mem_access Unknown \valid(flag->result.int_value)
. kgflags.h 685 _kgflags_assign_default_values mem_access Unknown \valid(flag->result.double_value)
. kgflags.h 735 _kgflags_parse_flag mem_access Unknown \valid(flag->result.bool_value)
. kgflags.h 753 _kgflags_parse_flag mem_access Unknown \valid(flag->result.int_value)
. kgflags.h 784 _kgflags_parse_flag signed_overflow Unknown count + 1 ≤ 2147483647
. kgflags.h 787 _kgflags_parse_flag mem_access Unknown \valid(&arr->_items)
. kgflags.h 788 _kgflags_parse_flag mem_access Unknown \valid(&arr->_count)
. kgflags.h 809 _kgflags_parse_flag signed_overflow Unknown count_0 + 1 ≤ 2147483647
. kgflags.h 813 _kgflags_parse_flag mem_access Unknown \valid(&arr_0->_items)
. kgflags.h 814 _kgflags_parse_flag mem_access Unknown \valid(&arr_0->_count)
. kgflags.h 836 _kgflags_parse_flag signed_overflow Unknown count_1 + 1 ≤ 2147483647
. kgflags.h 840 _kgflags_parse_flag mem_access Unknown \valid(&arr_1->_items)
. kgflags.h 841 _kgflags_parse_flag mem_access Unknown \valid(&arr_1->_count)
FRAMAC_SHARE/libc stdlib.h 98 strtod precondition Unknown valid_nptr: \valid_read(nptr)
FRAMAC_SHARE/libc stdlib.h 165 strtol precondition Unknown valid_nptr: \valid_read(nptr)
FRAMAC_SHARE/libc string.h 137 strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
FRAMAC_SHARE/libc string.h 138 strcmp precondition Unknown valid_string_s2: valid_read_string(s2)
FRAMAC_SHARE/libc string.h 220 strstr precondition Unknown valid_string_haystack: valid_read_string(haystack)
examples full_api.c 34 main precondition of printf_va_1 Unknown valid_read_string(param0)
examples full_api.c 34 printf_va_1 precondition Unknown valid_read_string(param0)
examples full_api.c 37 main is_nan_or_infinite Unknown \is_finite(double_val)
examples full_api.c 41 main precondition of printf_va_6 Unknown valid_read_string(param1)
examples full_api.c 41 printf_va_6 precondition Unknown valid_read_string(param1)
examples full_api.c 56 main precondition of printf_va_11 Unknown valid_read_string(param1)
examples full_api.c 56 printf_va_11 precondition Unknown valid_read_string(param1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 34 (out of 34)
Semantically reached functions = 34
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
736 stmts in analyzed functions, 707 stmts analyzed (96.1%)
_kgflags_add_error: 9 stmts out of 9 (100.0%)
_kgflags_add_non_flag_arg: 9 stmts out of 9 (100.0%)
_kgflags_consume_arg: 8 stmts out of 8 (100.0%)
_kgflags_get_flag: 29 stmts out of 29 (100.0%)
_kgflags_get_flag_name: 15 stmts out of 15 (100.0%)
_kgflags_is_flag: 3 stmts out of 3 (100.0%)
_kgflags_peek_arg: 6 stmts out of 6 (100.0%)
eva_main: 13 stmts out of 13 (100.0%)
kgflags_bool: 18 stmts out of 18 (100.0%)
kgflags_double: 11 stmts out of 11 (100.0%)
kgflags_double_array: 11 stmts out of 11 (100.0%)
kgflags_double_array_get_count: 2 stmts out of 2 (100.0%)
kgflags_get_non_flag_args_count: 2 stmts out of 2 (100.0%)
kgflags_int: 11 stmts out of 11 (100.0%)
kgflags_int_array: 11 stmts out of 11 (100.0%)
kgflags_int_array_get_count: 2 stmts out of 2 (100.0%)
kgflags_print_errors: 40 stmts out of 40 (100.0%)
kgflags_set_custom_description: 2 stmts out of 2 (100.0%)
kgflags_set_prefix: 2 stmts out of 2 (100.0%)
kgflags_string: 11 stmts out of 11 (100.0%)
kgflags_string_array: 11 stmts out of 11 (100.0%)
kgflags_string_array_get_count: 2 stmts out of 2 (100.0%)
main: 89 stmts out of 89 (100.0%)
kgflags_parse: 47 stmts out of 48 (97.9%)
_kgflags_parse_flag: 121 stmts out of 124 (97.6%)
kgflags_print_usage: 106 stmts out of 110 (96.4%)
kgflags_int_array_get_item: 15 stmts out of 16 (93.8%)
kgflags_get_non_flag_arg: 8 stmts out of 9 (88.9%)
kgflags_string_array_get_item: 8 stmts out of 9 (88.9%)
_kgflags_parse_int: 21 stmts out of 24 (87.5%)
kgflags_double_array_get_item: 14 stmts out of 16 (87.5%)
_kgflags_assign_default_values: 27 stmts out of 31 (87.1%)
_kgflags_add_flag: 9 stmts out of 12 (75.0%)
_kgflags_parse_double: 14 stmts out of 20 (70.0%)
kgflags.h:641:[nonterm] warning: non-terminating statement
stack 1: _kgflags_parse_double :: kgflags.h:765 <-
_kgflags_parse_flag :: kgflags.h:380 <-
kgflags_parse :: examples/full_api.c:28 <-
main :: fc_stubs.c:21 <-
eva_main
stack 2: _kgflags_parse_double :: kgflags.h:830 <-
_kgflags_parse_flag :: kgflags.h:380 <-
kgflags_parse :: examples/full_api.c:28 <-
main :: fc_stubs.c:21 <-
eva_main
stack 3: _kgflags_parse_double :: kgflags.h:552 <-
kgflags_double_array_get_item :: examples/full_api.c:51 <-
main :: fc_stubs.c:21 <-
eva_main
examples/full_api.c:37:[eva:garbled-mix] warning: The specification of function printf_va_4 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
examples/full_api.c:39:[eva:garbled-mix] warning: The specification of function printf_va_5 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
examples/full_api.c:41:[eva:garbled-mix] warning: The specification of function printf_va_6 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
examples/full_api.c:44:[eva:garbled-mix] warning: The specification of function printf_va_7 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
kgflags.h:626:[eva:garbled-mix] warning: The specification of function strtol has generated a garbled mix for assigns clause *endptr.
examples/full_api.c:46:[eva:garbled-mix] warning: The specification of function printf_va_8 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
examples/full_api.c:49:[eva:garbled-mix] warning: The specification of function printf_va_9 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
kgflags.h:639:[eva:garbled-mix] warning: The specification of function strtod has generated a garbled mix for assigns clause *endptr.
examples/full_api.c:51:[eva:garbled-mix] warning: The specification of function printf_va_10 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
examples/full_api.c:56:[eva:garbled-mix] warning: The specification of function printf_va_11 has generated a garbled mix for assigns clause __fc_stdout->__fc_FILE_data.
fc_stubs.c:21:[eva:locals-escaping] warning: locals {string_val} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {bool_val, int_val, double_val, string_arr, int_arr, double_arr} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {int_val, double_val, string_arr, int_arr, double_arr} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {double_val, string_arr, int_arr, double_arr} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {string_arr, int_arr, double_arr} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {int_arr, double_arr} escaping the scope of main through _kgflags_g
fc_stubs.c:21:[eva:locals-escaping] warning: locals {double_arr} escaping the scope of main through _kgflags_g
[eva:garbled-mix] warning: Garbled mix generated during analysis:
{{ garbled mix of &{argv1; argv2; argv3; argv4}
(origin: Misaligned {kgflags.h:657}) }}
{{ garbled mix of &{"bool"; "int"; "double"; "string-array"; "int-array";
"double-array"} (origin: Misaligned {kgflags.h:657}) }}
{{ garbled mix of &{argv} (origin: Merge {kgflags.h:849}) }}
{{ garbled mix of &{"string"; "bool"; "int"; "double"; "string-array";
"int-array"; "double-array"}
(origin: Misaligned {kgflags.h:657}) }}
{{ garbled mix of &{"string"} (origin: Misaligned {kgflags.h:657}) }}
{{ garbled mix of &{argv} (origin: Merge {kgflags.h:735}) }}
{{ garbled mix of &{argv} (origin: Misaligned {examples/full_api.c:37}) }}
{{ garbled mix of &{argv} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv1} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv3} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv2} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv4} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv0} (origin: Misaligned {kgflags.h:522}) }}
{{ garbled mix of &{argv} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv1} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv3} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv2} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv4} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv0} (origin: Misaligned {kgflags.h:533}) }}
{{ garbled mix of &{argv} (origin: Misaligned {kgflags.h:550}) }}
{{ garbled mix of &{argv1} (origin: Misaligned {kgflags.h:550}) }}
{{ garbled mix of &{argv3} (origin: Misaligned {kgflags.h:550}) }}
{{ garbled mix of &{argv2} (origin: Misaligned {kgflags.h:550}) }}
{{ garbled mix of &{argv4} (origin: Misaligned {kgflags.h:550}) }}
{{ garbled mix of &{argv0} (origin: Misaligned {kgflags.h:550}) }}
This diff is collapsed.
[metrics] Defined functions (34)
======================
_kgflags_add_error (14 calls); _kgflags_add_flag (7 calls);
_kgflags_add_non_flag_arg (1 call); _kgflags_assign_default_values (1 call);
_kgflags_consume_arg (7 calls); _kgflags_get_flag (2 calls);
_kgflags_get_flag_name (2 calls); _kgflags_is_flag (4 calls);
_kgflags_parse_double (3 calls); _kgflags_parse_flag (1 call);
_kgflags_parse_int (3 calls); _kgflags_peek_arg (3 calls);
eva_main (0 call); kgflags_bool (1 call); kgflags_double (1 call);
kgflags_double_array (1 call); kgflags_double_array_get_count (2 calls);
kgflags_double_array_get_item (1 call); kgflags_get_non_flag_arg (1 call);
kgflags_get_non_flag_args_count (1 call); kgflags_int (1 call);
kgflags_int_array (1 call); kgflags_int_array_get_count (2 calls);
kgflags_int_array_get_item (1 call); kgflags_parse (1 call);
kgflags_print_errors (1 call); kgflags_print_usage (1 call);
kgflags_set_custom_description (1 call); kgflags_set_prefix (1 call);
kgflags_string (1 call); kgflags_string_array (1 call);
kgflags_string_array_get_count (2 calls);
kgflags_string_array_get_item (1 call); main (1 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
eva_main;
Global metrics
==============
Sloc = 736
Decision point = 118
Global variables = 1
If = 90
Loop = 14
Goto = 44
Assignment = 269
Exit point = 34
Function = 34
Function call = 127
Pointer dereferencing = 140
Cyclomatic complexity = 152
directory file line function property kind status property
. kgflags.h 402 kgflags_print_errors initialization Unknown \initialized(&err->kind)
. kgflags.h 404 fprintf_va_1 precondition Unknown valid_read_string(param1)
. kgflags.h 404 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 404 kgflags_print_errors precondition of fprintf_va_1 Unknown valid_read_string(param1)
. kgflags.h 408 fprintf_va_2 precondition Unknown valid_read_string(param1)
. kgflags.h 408 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 408 kgflags_print_errors precondition of fprintf_va_2 Unknown valid_read_string(param1)
. kgflags.h 412 fprintf_va_3 precondition Unknown valid_read_string(param1)
. kgflags.h 412 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 412 kgflags_print_errors precondition of fprintf_va_3 Unknown valid_read_string(param1)
. kgflags.h 416 fprintf_va_4 precondition Unknown valid_read_string(param1)
. kgflags.h 416 fprintf_va_4 precondition Unknown valid_read_string(param2)
. kgflags.h 416 kgflags_print_errors initialization Unknown \initialized(&err->arg)
. kgflags.h 416 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 416 kgflags_print_errors precondition of fprintf_va_4 Unknown valid_read_string(param1)
. kgflags.h 416 kgflags_print_errors precondition of fprintf_va_4 Unknown valid_read_string(param2)
. kgflags.h 420 fprintf_va_5 precondition Unknown valid_read_string(param1)
. kgflags.h 420 fprintf_va_5 precondition Unknown valid_read_string(param2)
. kgflags.h 420 kgflags_print_errors initialization Unknown \initialized(&err->arg)
. kgflags.h 420 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 420 kgflags_print_errors precondition of fprintf_va_5 Unknown valid_read_string(param1)
. kgflags.h 420 kgflags_print_errors precondition of fprintf_va_5 Unknown valid_read_string(param2)
. kgflags.h 432 fprintf_va_8 precondition Unknown valid_read_string(param1)
. kgflags.h 432 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 432 kgflags_print_errors precondition of fprintf_va_8 Unknown valid_read_string(param1)
. kgflags.h 436 fprintf_va_9 precondition Unknown valid_read_string(param1)
. kgflags.h 436 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 436 kgflags_print_errors precondition of fprintf_va_9 Unknown valid_read_string(param1)
. kgflags.h 440 fprintf_va_10 precondition Unknown valid_read_string(param1)
. kgflags.h 440 kgflags_print_errors initialization Unknown \initialized(&err->flag_name)
. kgflags.h 440 kgflags_print_errors precondition of fprintf_va_10 Unknown valid_read_string(param1)
. kgflags.h 608 _kgflags_get_flag precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
FRAMAC_SHARE/libc stdio.h 336 puts precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 137 strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
examples simple.c 12 main precondition of puts Unknown valid_string_s: valid_read_string(s)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 18 (out of 34)
Semantically reached functions = 15
Coverage estimation = 83.3%
Unreached functions (3) =
<kgflags.h>: _kgflags_parse_double; _kgflags_parse_int; _kgflags_peek_arg;
[metrics] References to non-analyzed functions
------------------------------------
Function _kgflags_parse_flag calls _kgflags_parse_int (at kgflags.h:747)
Function _kgflags_parse_flag calls _kgflags_parse_double (at kgflags.h:765)
Function _kgflags_parse_flag calls _kgflags_peek_arg (at kgflags.h:779)
Function _kgflags_parse_flag calls _kgflags_peek_arg (at kgflags.h:797)
Function _kgflags_parse_flag calls _kgflags_parse_int (at kgflags.h:803)
Function _kgflags_parse_flag calls _kgflags_peek_arg (at kgflags.h:824)
Function _kgflags_parse_flag calls _kgflags_parse_double (at kgflags.h:830)
[metrics] Statements analyzed by Eva
--------------------------
474 stmts in analyzed functions, 240 stmts analyzed (50.6%)
_kgflags_add_error: 9 stmts out of 9 (100.0%)
_kgflags_add_non_flag_arg: 9 stmts out of 9 (100.0%)
_kgflags_consume_arg: 8 stmts out of 8 (100.0%)
_kgflags_get_flag_name: 15 stmts out of 15 (100.0%)
_kgflags_is_flag: 3 stmts out of 3 (100.0%)
eva_main: 13 stmts out of 13 (100.0%)
kgflags_print_errors: 40 stmts out of 40 (100.0%)
kgflags_string: 11 stmts out of 11 (100.0%)
main: 12 stmts out of 12 (100.0%)
kgflags_parse: 45 stmts out of 48 (93.8%)
_kgflags_get_flag: 18 stmts out of 29 (62.1%)
_kgflags_add_flag: 6 stmts out of 12 (50.0%)
_kgflags_assign_default_values: 13 stmts out of 31 (41.9%)
kgflags_print_usage: 26 stmts out of 110 (23.6%)
_kgflags_parse_flag: 12 stmts out of 124 (9.7%)
fc_stubs.c:21:[eva:locals-escaping] warning: locals {to_print} escaping the scope of main through _kgflags_g
[eva:garbled-mix] warning: Garbled mix generated during analysis:
{{ garbled mix of &{argv1; argv2; argv3; argv4}
(origin: Misaligned {kgflags.h:657}) }}
{{ garbled mix of &{"to-print"} (origin: Misaligned {kgflags.h:657}) }}
This diff is collapsed.
[metrics] Defined functions (34)
======================
_kgflags_add_error (14 calls); _kgflags_add_flag (7 calls);
_kgflags_add_non_flag_arg (1 call); _kgflags_assign_default_values (1 call);
_kgflags_consume_arg (7 calls); _kgflags_get_flag (2 calls);
_kgflags_get_flag_name (2 calls); _kgflags_is_flag (4 calls);
_kgflags_parse_double (3 calls); _kgflags_parse_flag (1 call);
_kgflags_parse_int (3 calls); _kgflags_peek_arg (3 calls);
eva_main (0 call); kgflags_bool (0 call); kgflags_double (0 call);
kgflags_double_array (0 call); kgflags_double_array_get_count (0 call);
kgflags_double_array_get_item (0 call); kgflags_get_non_flag_arg (0 call);
kgflags_get_non_flag_args_count (0 call); kgflags_int (0 call);
kgflags_int_array (0 call); kgflags_int_array_get_count (0 call);
kgflags_int_array_get_item (0 call); kgflags_parse (1 call);
kgflags_print_errors (1 call); kgflags_print_usage (1 call);
kgflags_set_custom_description (0 call); kgflags_set_prefix (0 call);
kgflags_string (1 call); kgflags_string_array (0 call);
kgflags_string_array_get_count (0 call);
kgflags_string_array_get_item (0 call); main (1 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (17)
===========================
eva_main; kgflags_bool; kgflags_double; kgflags_double_array;
kgflags_double_array_get_count; kgflags_double_array_get_item;
kgflags_get_non_flag_arg; kgflags_get_non_flag_args_count; kgflags_int;
kgflags_int_array; kgflags_int_array_get_count; kgflags_int_array_get_item;
kgflags_set_custom_description; kgflags_set_prefix; kgflags_string_array;
kgflags_string_array_get_count; kgflags_string_array_get_item;
Global metrics
==============
Sloc = 659
Decision point = 113
Global variables = 1
If = 85
Loop = 10
Goto = 44
Assignment = 245
Exit point = 34
Function = 34
Function call = 98
Pointer dereferencing = 140
Cyclomatic complexity = 147
FRAMAC_BIN=/home/andr/git/frama-c-quebec/bin
ifeq ($(wildcard $(FRAMAC_BIN)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=$(FRAMAC_BIN)/frama-c
FRAMAC_GUI=$(FRAMAC_BIN)/frama-c-gui
endif
MIT License
Copyright (c) 2020 Krzysztof Gabis
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
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