[kgflags] add new case study

Makefile

@@ -61,6 +61,7 @@ TARGETS=\
   icpc \
   itc-benchmarks \
   jsmn \
+  kgflags \
   khash \
   kilo \
   libmodbus \

README.md

@@ -132,6 +132,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)

kgflags/.frama-c/GNUmakefile

+# 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

kgflags/.frama-c/fc_stubs.c

+// 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__

kgflags/.frama-c/kgflags-full_api.eva/alarms.csv

+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)

kgflags/.frama-c/kgflags-full_api.eva/metrics.log

+[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/.frama-c/kgflags-full_api.eva/nonterm.log

+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

kgflags/.frama-c/kgflags-full_api.eva/warnings.log

+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}) }}

kgflags/.frama-c/kgflags-full_api.parse/metrics.log

+[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

kgflags/.frama-c/kgflags-simple.eva/alarms.csv

+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)

kgflags/.frama-c/kgflags-simple.eva/metrics.log

+[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%)

kgflags/.frama-c/kgflags-simple.eva/warnings.log

+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}) }}

kgflags/.frama-c/kgflags-simple.parse/metrics.log

+[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

kgflags/.frama-c/path.mk

+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

kgflags/LICENSE

+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.