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

[libyaml] add new case study

parent 561967d4
Pipeline #32359 passed with stage
in 49 minutes and 23 seconds
......@@ -65,6 +65,7 @@ TARGETS=\
kilo \
libmodbus \
libspng \
libyaml \
microstrain \
mini-gmp \
miniz \
......
......@@ -137,6 +137,7 @@ when available. We also summarize the license of each directory below.
(see https://github.com/antirez/kilo/blob/master/LICENSE)
- `libmodbus`: LGPL
- `libspng`: BSD 2-clause, see `LICENSE`
- `libyaml`: MIT, see `License`
- `mibench`: several (see `LICENSE` file inside each subdirectory)
- `mini-gmp`: LGPL or GPL
- `miniz`: MIT
......
# 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 += \
-I../include \
-DHAVE_CONFIG_H \
-DYAML_DECLARE_STATIC \
## General flags
FCFLAGS += \
-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 = \
test-reader.eva \
test-version.eva \
# TODO: modify handling of dynamic memory allocation to speed up these tests
# run-dumper.eva \
# run-emitter.eva \
# run-parser-test-suite.eva \
# run-scanner.eva \
COMMON_SRCS=\
../src/api.c \
../src/dumper.c \
../src/emitter.c \
../src/loader.c \
../src/parser.c \
../src/reader.c \
../src/scanner.c \
../src/writer.c \
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
run-dumper.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-dumper.c \
run-emitter.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-emitter.c \
run-emitter-test-suite.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-emitter-test-suite.c \
run-parser.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-parser.c \
run-parser-test-suite.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-parser-test-suite.c \
run-scanner.parse: \
$(COMMON_SRCS) \
fc_stubs.c \
../tests/run-scanner.c \
run-*.parse: FCFLAGS += -main eva_main
test-reader.parse: \
$(COMMON_SRCS) \
../tests/test-reader.c \
test-version.parse: \
$(COMMON_SRCS) \
../tests/test-version.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__
../../path.mk
\ No newline at end of file
directory file line function property kind status property
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Unknown nonnull_c: c ≢ 0
FRAMAC_SHARE/libc string.h 55 memcmp precondition Unknown valid_s1: valid_read_or_empty(s1, n)
FRAMAC_SHARE/libc string.h 57 memcmp precondition Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
FRAMAC_SHARE/libc string.h 59 memcmp precondition Unknown danglingness: s1: non_escaping(s1, n)
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 104 memmove precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 105 memmove precondition Unknown valid_src: valid_read_or_empty(src, n)
src api.c 235 yaml_parser_delete mem_access Invalid or unreachable \valid_read(parser->tag_directives.top)
src api.c 254 yaml_string_read_handler ptr_comparison Unknown \pointer_comparable((void *)parser->input.string.current, (void *)parser->input.string.end)
src api.c 259 yaml_string_read_handler differing_blocks Unknown \base_addr(parser->input.string.end) ≡ \base_addr(parser->input.string.current)
src api.c 259 yaml_string_read_handler signed_overflow Unknown -9223372036854775808 ≤ parser->input.string.end - parser->input.string.current
src api.c 259 yaml_string_read_handler signed_overflow Unknown parser->input.string.end - parser->input.string.current ≤ 9223372036854775807
src api.c 264 yaml_string_read_handler precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
src api.c 264 yaml_string_read_handler precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
src api.c 586 yaml_token_delete precondition of __FC_assert Unknown nonnull_c: c ≢ 0
src api.c 588 yaml_token_delete initialization Invalid or unreachable \initialized(&token->type)
src reader.c 56 yaml_parser_determine_encoding dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 56 yaml_parser_determine_encoding differing_blocks Unknown \base_addr(parser->raw_buffer.last) ≡ \base_addr(parser->raw_buffer.pointer)
src reader.c 56 yaml_parser_determine_encoding signed_overflow Unknown -9223372036854775808 ≤ parser->raw_buffer.last - parser->raw_buffer.pointer
src reader.c 56 yaml_parser_determine_encoding signed_overflow Unknown parser->raw_buffer.last - parser->raw_buffer.pointer ≤ 9223372036854775807
src reader.c 64 yaml_parser_determine_encoding dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 64 yaml_parser_determine_encoding differing_blocks Unknown \base_addr(parser->raw_buffer.last) ≡ \base_addr(parser->raw_buffer.pointer)
src reader.c 64 yaml_parser_determine_encoding signed_overflow Unknown -9223372036854775808 ≤ parser->raw_buffer.last - parser->raw_buffer.pointer
src reader.c 64 yaml_parser_determine_encoding signed_overflow Unknown parser->raw_buffer.last - parser->raw_buffer.pointer ≤ 9223372036854775807
src reader.c 65 yaml_parser_determine_encoding precondition of memcmp Unknown danglingness: s1: non_escaping(s1, n)
src reader.c 65 yaml_parser_determine_encoding precondition of memcmp Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
src reader.c 65 yaml_parser_determine_encoding precondition of memcmp Unknown valid_s1: valid_read_or_empty(s1, n)
src reader.c 71 yaml_parser_determine_encoding precondition of memcmp Unknown danglingness: s1: non_escaping(s1, n)
src reader.c 71 yaml_parser_determine_encoding precondition of memcmp Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
src reader.c 71 yaml_parser_determine_encoding precondition of memcmp Unknown valid_s1: valid_read_or_empty(s1, n)
src reader.c 77 yaml_parser_determine_encoding precondition of memcmp Unknown danglingness: s1: non_escaping(s1, n)
src reader.c 77 yaml_parser_determine_encoding precondition of memcmp Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
src reader.c 77 yaml_parser_determine_encoding precondition of memcmp Unknown valid_s1: valid_read_or_empty(s1, n)
src reader.c 100 yaml_parser_update_raw_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.start, (void *)parser->raw_buffer.pointer)
src reader.c 101 yaml_parser_update_raw_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 101 yaml_parser_update_raw_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.last, (void *)parser->raw_buffer.end)
src reader.c 111 yaml_parser_update_raw_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 111 yaml_parser_update_raw_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.pointer, (void *)parser->raw_buffer.last)
src reader.c 112 yaml_parser_update_raw_buffer precondition of memmove Unknown valid_dest: valid_or_empty(dest, n)
src reader.c 112 yaml_parser_update_raw_buffer precondition of memmove Unknown valid_src: valid_read_or_empty(src, n)
src reader.c 113 yaml_parser_update_raw_buffer differing_blocks Unknown \base_addr(parser->raw_buffer.last) ≡ \base_addr(parser->raw_buffer.pointer)
src reader.c 113 yaml_parser_update_raw_buffer signed_overflow Unknown -9223372036854775808 ≤ parser->raw_buffer.last - parser->raw_buffer.pointer
src reader.c 113 yaml_parser_update_raw_buffer signed_overflow Unknown parser->raw_buffer.last - parser->raw_buffer.pointer ≤ 9223372036854775807
src reader.c 115 yaml_parser_update_raw_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 116 yaml_parser_update_raw_buffer differing_blocks Unknown \base_addr(parser->raw_buffer.pointer) ≡ \base_addr(parser->raw_buffer.start)
src reader.c 116 yaml_parser_update_raw_buffer signed_overflow Unknown parser->raw_buffer.pointer - parser->raw_buffer.start ≤ 9223372036854775807
src reader.c 122 yaml_parser_update_raw_buffer differing_blocks Unknown \base_addr(parser->raw_buffer.end) ≡ \base_addr(parser->raw_buffer.last)
src reader.c 122 yaml_parser_update_raw_buffer signed_overflow Unknown -9223372036854775808 ≤ parser->raw_buffer.end - parser->raw_buffer.last
src reader.c 122 yaml_parser_update_raw_buffer signed_overflow Unknown parser->raw_buffer.end - parser->raw_buffer.last ≤ 9223372036854775807
src reader.c 150 yaml_parser_update_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 150 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.pointer, (void *)parser->raw_buffer.last)
src reader.c 167 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->buffer.start, (void *)parser->buffer.pointer)
src reader.c 168 yaml_parser_update_buffer dangling_pointer Unknown ¬\dangling(&parser->buffer.last)
src reader.c 168 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->buffer.pointer, (void *)parser->buffer.last)
src reader.c 169 yaml_parser_update_buffer differing_blocks Unknown \base_addr(parser->buffer.last) ≡ \base_addr(parser->buffer.pointer)
src reader.c 169 yaml_parser_update_buffer signed_overflow Unknown parser->buffer.last - parser->buffer.pointer ≤ 9223372036854775807
src reader.c 170 yaml_parser_update_buffer precondition of memmove Unknown valid_dest: valid_or_empty(dest, n)
src reader.c 170 yaml_parser_update_buffer precondition of memmove Unknown valid_src: valid_read_or_empty(src, n)
src reader.c 174 yaml_parser_update_buffer dangling_pointer Unknown ¬\dangling(&parser->buffer.last)
src reader.c 174 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->buffer.pointer, (void *)parser->buffer.last)
src reader.c 185 yaml_parser_update_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 185 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.pointer, (void *)parser->raw_buffer.last)
src reader.c 192 yaml_parser_update_buffer dangling_pointer Unknown ¬\dangling(&parser->raw_buffer.last)
src reader.c 192 yaml_parser_update_buffer ptr_comparison Unknown \pointer_comparable((void *)parser->raw_buffer.pointer, (void *)parser->raw_buffer.last)
src reader.c 200 yaml_parser_update_buffer differing_blocks Unknown \base_addr(parser->raw_buffer.last) ≡ \base_addr(parser->raw_buffer.pointer)
src reader.c 200 yaml_parser_update_buffer signed_overflow Unknown -9223372036854775808 ≤ parser->raw_buffer.last - parser->raw_buffer.pointer
src reader.c 200 yaml_parser_update_buffer signed_overflow Unknown parser->raw_buffer.last - parser->raw_buffer.pointer ≤ 9223372036854775807
src reader.c 230 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + 0)
src reader.c 230 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + 0)
src reader.c 266 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + k)
src reader.c 266 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + k)
src reader.c 345 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + high)
src reader.c 345 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + low)
src reader.c 345 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + high)
src reader.c 345 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + low)
src reader.c 375 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + (int)(high + 2))
src reader.c 375 yaml_parser_update_buffer initialization Unknown \initialized(parser->raw_buffer.pointer + (int)(low + 2))
src reader.c 375 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + (int)(high + 2))
src reader.c 375 yaml_parser_update_buffer mem_access Unknown \valid_read(parser->raw_buffer.pointer + (int)(low + 2))
src reader.c 429 yaml_parser_update_buffer mem_access Unknown \valid(tmp_17)
src reader.c 433 yaml_parser_update_buffer mem_access Unknown \valid(tmp_18)
src reader.c 434 yaml_parser_update_buffer mem_access Unknown \valid(tmp_19)
src reader.c 438 yaml_parser_update_buffer mem_access Unknown \valid(tmp_20)
src reader.c 439 yaml_parser_update_buffer mem_access Unknown \valid(tmp_21)
src reader.c 440 yaml_parser_update_buffer mem_access Unknown \valid(tmp_22)
src reader.c 444 yaml_parser_update_buffer mem_access Unknown \valid(tmp_23)
src reader.c 445 yaml_parser_update_buffer mem_access Unknown \valid(tmp_24)
src reader.c 446 yaml_parser_update_buffer mem_access Unknown \valid(tmp_25)
src reader.c 447 yaml_parser_update_buffer mem_access Unknown \valid(tmp_26)
src reader.c 456 yaml_parser_update_buffer mem_access Unknown \valid(tmp_27)
tests test-reader.c 131 check_utf8_sequences mem_access Unknown \valid_read(end)
tests test-reader.c 133 check_utf8_sequences differing_blocks Unknown \base_addr(end) ≡ \base_addr(start)
tests test-reader.c 137 check_utf8_sequences signed_overflow Unknown failed + 1 ≤ 2147483647
tests test-reader.c 147 check_utf8_sequences precondition of printf_va_6 Unknown valid_read_string(param0)
tests test-reader.c 147 printf_va_6 precondition Unknown valid_read_string(param0)
tests test-reader.c 151 check_utf8_sequences precondition of printf_va_7 Unknown valid_read_string(param0)
tests test-reader.c 151 printf_va_7 precondition Unknown valid_read_string(param0)
tests test-reader.c 177 check_boms mem_access Unknown \valid_read(end)
tests test-reader.c 180 check_boms differing_blocks Unknown \base_addr(end) ≡ \base_addr(start)
tests test-reader.c 183 check_boms precondition of printf_va_12 Unknown valid_read_string(param0)
tests test-reader.c 183 printf_va_12 precondition Unknown valid_read_string(param0)
tests test-reader.c 184 check_boms signed_overflow Unknown failed + 1 ≤ 2147483647
tests test-reader.c 189 check_boms signed_overflow Unknown failed + 1 ≤ 2147483647
tests test-reader.c 191 check_boms precondition of memcmp Unknown danglingness: s1: non_escaping(s1, n)
tests test-reader.c 191 check_boms precondition of memcmp Unknown initialization: s1: \initialized((char *)s1 + (0 .. n - 1))
tests test-reader.c 191 check_boms precondition of memcmp Unknown valid_s1: valid_read_or_empty(s1, n)
tests test-reader.c 192 check_boms precondition of printf_va_14 Unknown valid_read_string(param0)
tests test-reader.c 192 printf_va_14 precondition Unknown valid_read_string(param0)
tests test-reader.c 193 check_boms signed_overflow Unknown failed + 1 ≤ 2147483647
tests test-reader.c 215 check_long_utf8 precondition of __FC_assert Unknown nonnull_c: c ≢ 0
tests test-reader.c 222 check_long_utf8 signed_overflow Unknown k + 1 ≤ 2147483647
tests test-reader.c 222 check_long_utf8 mem_access Unknown \valid(buffer + tmp_3)
tests test-reader.c 223 check_long_utf8 mem_access Unknown \valid(buffer + tmp_4)
tests test-reader.c 226 check_long_utf8 signed_overflow Unknown k + 1 ≤ 2147483647
tests test-reader.c 226 check_long_utf8 mem_access Unknown \valid(buffer + tmp_5)
tests test-reader.c 227 check_long_utf8 mem_access Unknown \valid(buffer + tmp_6)
tests test-reader.c 235 check_long_utf8 precondition of printf_va_18 Unknown valid_read_string(param0)
tests test-reader.c 235 printf_va_18 precondition Unknown valid_read_string(param0)
tests test-reader.c 253 check_long_utf8 initialization Unknown \initialized(parser.buffer.pointer + 0)
tests test-reader.c 253 check_long_utf8 mem_access Unknown \valid_read(parser.buffer.pointer + 0)
tests test-reader.c 253 check_long_utf8 initialization Unknown \initialized(parser.buffer.pointer + 1)
tests test-reader.c 254 check_long_utf8 initialization Unknown \initialized(parser.buffer.pointer + 1)
tests test-reader.c 265 check_long_utf8 precondition of printf_va_22 Unknown valid_read_string(param0)
tests test-reader.c 265 printf_va_22 precondition Unknown valid_read_string(param0)
tests test-reader.c 268 check_long_utf8 initialization Unknown \initialized(parser.buffer.pointer + 0)
tests test-reader.c 268 check_long_utf8 mem_access Unknown \valid_read(parser.buffer.pointer + 0)
tests test-reader.c 287 check_long_utf16 precondition of __FC_assert Unknown nonnull_c: c ≢ 0
tests test-reader.c 293 check_long_utf16 mem_access Unknown \valid(buffer + tmp_2)
tests test-reader.c 294 check_long_utf16 signed_overflow Unknown k + 1 ≤ 2147483647
tests test-reader.c 294 check_long_utf16 mem_access Unknown \valid(buffer + tmp_3)
tests test-reader.c 297 check_long_utf16 mem_access Unknown \valid(buffer + tmp_4)
tests test-reader.c 298 check_long_utf16 signed_overflow Unknown k + 1 ≤ 2147483647
tests test-reader.c 298 check_long_utf16 mem_access Unknown \valid(buffer + tmp_5)
tests test-reader.c 306 check_long_utf16 precondition of printf_va_25 Unknown valid_read_string(param0)
tests test-reader.c 306 printf_va_25 precondition Unknown valid_read_string(param0)
tests test-reader.c 324 check_long_utf16 initialization Unknown \initialized(parser.buffer.pointer + 0)
tests test-reader.c 324 check_long_utf16 mem_access Unknown \valid_read(parser.buffer.pointer + 0)
tests test-reader.c 324 check_long_utf16 initialization Unknown \initialized(parser.buffer.pointer + 1)
tests test-reader.c 325 check_long_utf16 initialization Unknown \initialized(parser.buffer.pointer + 1)
tests test-reader.c 336 check_long_utf16 precondition of printf_va_29 Unknown valid_read_string(param0)
tests test-reader.c 336 printf_va_29 precondition Unknown valid_read_string(param0)
tests test-reader.c 339 check_long_utf16 initialization Unknown \initialized(parser.buffer.pointer + 0)
tests test-reader.c 339 check_long_utf16 mem_access Unknown \valid_read(parser.buffer.pointer + 0)
tests test-reader.c 353 main signed_overflow Unknown (int)((int)(tmp + tmp_0) + tmp_1) + tmp_2 ≤ 2147483647
tests test-reader.c 353 main signed_overflow Unknown (int)(tmp + tmp_0) + tmp_1 ≤ 2147483647
tests test-reader.c 353 main signed_overflow Unknown tmp + tmp_0 ≤ 2147483647
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 16 (out of 199)
Semantically reached functions = 16
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
946 stmts in analyzed functions, 913 stmts analyzed (96.5%)
check_boms: 34 stmts out of 34 (100.0%)
check_long_utf16: 80 stmts out of 80 (100.0%)
check_long_utf8: 84 stmts out of 84 (100.0%)
check_utf8_sequences: 43 stmts out of 43 (100.0%)
main: 7 stmts out of 7 (100.0%)
yaml_free: 3 stmts out of 3 (100.0%)
yaml_parser_initialize: 207 stmts out of 207 (100.0%)
yaml_parser_set_input_string: 9 stmts out of 9 (100.0%)
yaml_parser_set_reader_error: 6 stmts out of 6 (100.0%)
yaml_string_read_handler: 13 stmts out of 13 (100.0%)
yaml_parser_delete: 102 stmts out of 104 (98.1%)
yaml_parser_update_buffer: 262 stmts out of 270 (97.0%)
yaml_parser_determine_encoding: 35 stmts out of 38 (92.1%)
yaml_parser_update_raw_buffer: 22 stmts out of 26 (84.6%)
yaml_malloc: 4 stmts out of 5 (80.0%)
yaml_token_delete: 2 stmts out of 17 (11.8%)
src/api.c:235:[nonterm] warning: non-terminating statement
stack 1: yaml_parser_delete :: tests/test-reader.c:157 <-
check_utf8_sequences :: tests/test-reader.c:353 <-
main
stack 2: yaml_parser_delete :: tests/test-reader.c:199 <-
check_boms :: tests/test-reader.c:353 <-
main
stack 3: yaml_parser_delete :: tests/test-reader.c:273 <-
check_long_utf8 :: tests/test-reader.c:353 <-
main
stack 4: yaml_parser_delete :: tests/test-reader.c:344 <-
check_long_utf16 :: tests/test-reader.c:353 <-
main
src/api.c:588:[nonterm] warning: non-terminating switch
stack 1: yaml_token_delete :: src/api.c:227 <-
yaml_parser_delete :: tests/test-reader.c:157 <-
check_utf8_sequences :: tests/test-reader.c:353 <-
main
stack 2: yaml_token_delete :: src/api.c:227 <-
yaml_parser_delete :: tests/test-reader.c:199 <-
check_boms :: tests/test-reader.c:353 <-
main
stack 3: yaml_token_delete :: src/api.c:227 <-
yaml_parser_delete :: tests/test-reader.c:273 <-
check_long_utf8 :: tests/test-reader.c:353 <-
main
stack 4: yaml_token_delete :: src/api.c:227 <-
yaml_parser_delete :: tests/test-reader.c:344 <-
check_long_utf16 :: tests/test-reader.c:353 <-
main
This diff is collapsed.
[metrics] Defined functions (199)
=======================
check_boms (1 call); check_long_utf16 (1 call); check_long_utf8 (1 call);
check_utf8_sequences (1 call); main (0 call);
yaml_alias_event_initialize (0 call); yaml_check_utf8 (16 calls);
yaml_document_add_mapping (0 call); yaml_document_add_scalar (0 call);
yaml_document_add_sequence (0 call);
yaml_document_append_mapping_pair (0 call);
yaml_document_append_sequence_item (0 call); yaml_document_delete (2 calls);
yaml_document_end_event_initialize (0 call);
yaml_document_get_node (0 call); yaml_document_get_root_node (0 call);
yaml_document_initialize (0 call);
yaml_document_start_event_initialize (0 call);
yaml_emitter_analyze_anchor (4 calls); yaml_emitter_analyze_event (1 call);
yaml_emitter_analyze_scalar (1 call); yaml_emitter_analyze_tag (3 calls);
yaml_emitter_analyze_tag_directive (1 call);
yaml_emitter_analyze_version_directive (1 call);
yaml_emitter_anchor_node (4 calls);
yaml_emitter_append_tag_directive (2 calls);
yaml_emitter_check_empty_document (1 call);
yaml_emitter_check_empty_mapping (2 calls);
yaml_emitter_check_empty_sequence (2 calls);
yaml_emitter_check_simple_key (2 calls); yaml_emitter_close (1 call);
yaml_emitter_delete (0 call);
yaml_emitter_delete_document_and_anchors (3 calls);
yaml_emitter_dump (0 call); yaml_emitter_dump_alias (1 call);
yaml_emitter_dump_mapping (1 call); yaml_emitter_dump_node (4 calls);
yaml_emitter_dump_scalar (1 call); yaml_emitter_dump_sequence (1 call);
yaml_emitter_emit (10 calls); yaml_emitter_emit_alias (1 call);
yaml_emitter_emit_block_mapping_key (2 calls);
yaml_emitter_emit_block_mapping_value (2 calls);
yaml_emitter_emit_block_sequence_item (2 calls);
yaml_emitter_emit_document_content (1 call);
yaml_emitter_emit_document_end (1 call);
yaml_emitter_emit_document_start (2 calls);
yaml_emitter_emit_flow_mapping_key (2 calls);
yaml_emitter_emit_flow_mapping_value (2 calls);
yaml_emitter_emit_flow_sequence_item (2 calls);
yaml_emitter_emit_mapping_start (1 call); yaml_emitter_emit_node (9 calls);
yaml_emitter_emit_scalar (1 call);
yaml_emitter_emit_sequence_start (1 call);
yaml_emitter_emit_stream_start (1 call); yaml_emitter_flush (60 calls);
yaml_emitter_generate_anchor (1 call);
yaml_emitter_increase_indent (5 calls); yaml_emitter_initialize (0 call);
yaml_emitter_need_more_events (1 call); yaml_emitter_open (1 call);
yaml_emitter_process_anchor (4 calls); yaml_emitter_process_scalar (1 call);
yaml_emitter_process_tag (3 calls);
yaml_emitter_select_scalar_style (1 call); yaml_emitter_set_break (0 call);
yaml_emitter_set_canonical (0 call);
yaml_emitter_set_emitter_error (16 calls);
yaml_emitter_set_encoding (0 call); yaml_emitter_set_indent (0 call);
yaml_emitter_set_output (0 call); yaml_emitter_set_output_file (0 call);
yaml_emitter_set_output_string (0 call); yaml_emitter_set_unicode (0 call);
yaml_emitter_set_width (0 call); yaml_emitter_set_writer_error (2 calls);
yaml_emitter_state_machine (1 call); yaml_emitter_write_anchor (1 call);
yaml_emitter_write_block_scalar_hints (2 calls);
yaml_emitter_write_bom (1 call);
yaml_emitter_write_double_quoted_scalar (1 call);
yaml_emitter_write_folded_scalar (1 call);
yaml_emitter_write_indent (25 calls);
yaml_emitter_write_indicator (34 calls);
yaml_emitter_write_literal_scalar (1 call);
yaml_emitter_write_plain_scalar (1 call);
yaml_emitter_write_single_quoted_scalar (1 call);
yaml_emitter_write_tag_content (3 calls);
yaml_emitter_write_tag_handle (2 calls); yaml_event_delete (3 calls);
yaml_file_read_handler (address taken) (0 call);
yaml_file_write_handler (address taken) (0 call); yaml_free (169 calls);
yaml_get_version (0 call); yaml_get_version_string (0 call);
yaml_malloc (52 calls); yaml_mapping_end_event_initialize (0 call);
yaml_mapping_start_event_initialize (0 call);
yaml_parser_append_tag_directive (2 calls);
yaml_parser_decrease_flow_level (1 call); yaml_parser_delete (4 calls);
yaml_parser_delete_aliases (2 calls);
yaml_parser_determine_encoding (1 call); yaml_parser_fetch_anchor (2 calls);
yaml_parser_fetch_block_entry (1 call);
yaml_parser_fetch_block_scalar (2 calls);
yaml_parser_fetch_directive (1 call);
yaml_parser_fetch_document_indicator (2 calls);
yaml_parser_fetch_flow_collection_end (2 calls);
yaml_parser_fetch_flow_collection_start (2 calls);
yaml_parser_fetch_flow_entry (1 call);
yaml_parser_fetch_flow_scalar (2 calls); yaml_parser_fetch_key (1 call);
yaml_parser_fetch_more_tokens (37 calls);
yaml_parser_fetch_next_token (1 call);
yaml_parser_fetch_plain_scalar (1 call);
yaml_parser_fetch_stream_end (1 call);
yaml_parser_fetch_stream_start (1 call); yaml_parser_fetch_tag (1 call);
yaml_parser_fetch_value (1 call); yaml_parser_increase_flow_level (1 call);
yaml_parser_initialize (4 calls); yaml_parser_load (0 call);
yaml_parser_load_alias (1 call); yaml_parser_load_document (1 call);
yaml_parser_load_mapping (1 call); yaml_parser_load_mapping_end (1 call);
yaml_parser_load_node_add (4 calls); yaml_parser_load_nodes (1 call);
yaml_parser_load_scalar (1 call); yaml_parser_load_sequence (1 call);
yaml_parser_load_sequence_end (1 call); yaml_parser_parse (3 calls);
yaml_parser_parse_block_mapping_key (2 calls);
yaml_parser_parse_block_mapping_value (1 call);
yaml_parser_parse_block_sequence_entry (2 calls);
yaml_parser_parse_document_content (1 call);
yaml_parser_parse_document_end (1 call);
yaml_parser_parse_document_start (2 calls);
yaml_parser_parse_flow_mapping_key (2 calls);
yaml_parser_parse_flow_mapping_value (2 calls);
yaml_parser_parse_flow_sequence_entry (2 calls);
yaml_parser_parse_flow_sequence_entry_mapping_end (1 call);
yaml_parser_parse_flow_sequence_entry_mapping_key (1 call);
yaml_parser_parse_flow_sequence_entry_mapping_value (1 call);
yaml_parser_parse_indentless_sequence_entry (1 call);
yaml_parser_parse_node (14 calls); yaml_parser_parse_stream_start (1 call);
yaml_parser_process_directives (2 calls);
yaml_parser_process_empty_scalar (11 calls);
yaml_parser_register_anchor (3 calls);
yaml_parser_remove_simple_key (9 calls); yaml_parser_roll_indent (4 calls);
yaml_parser_save_simple_key (5 calls); yaml_parser_scan (0 call);
yaml_parser_scan_anchor (1 call); yaml_parser_scan_block_scalar (1 call);
yaml_parser_scan_block_scalar_breaks (2 calls);
yaml_parser_scan_directive (1 call);
yaml_parser_scan_directive_name (1 call);
yaml_parser_scan_flow_scalar (1 call);
yaml_parser_scan_plain_scalar (1 call); yaml_parser_scan_tag (1 call);
yaml_parser_scan_tag_directive_value (1 call);
yaml_parser_scan_tag_handle (2 calls); yaml_parser_scan_tag_uri (4 calls);
yaml_parser_scan_to_next_token (1 call);
yaml_parser_scan_uri_escapes (1 call);
yaml_parser_scan_version_directive_number (2 calls);
yaml_parser_scan_version_directive_value (1 call);
yaml_parser_set_composer_error (1 call);
yaml_parser_set_composer_error_context (1 call);
yaml_parser_set_encoding (0 call); yaml_parser_set_input (0 call);
yaml_parser_set_input_file (0 call); yaml_parser_set_input_string (4 calls);
yaml_parser_set_parser_error (5 calls);
yaml_parser_set_parser_error_context (6 calls);
yaml_parser_set_reader_error (12 calls);
yaml_parser_set_scanner_error (35 calls);
yaml_parser_stale_simple_keys (2 calls); yaml_parser_state_machine (1 call);
yaml_parser_unroll_indent (4 calls); yaml_parser_update_buffer (65 calls);
yaml_parser_update_raw_buffer (2 calls); yaml_queue_extend (20 calls);
yaml_realloc (3 calls); yaml_scalar_event_initialize (0 call);
yaml_sequence_end_event_initialize (0 call);
yaml_sequence_start_event_initialize (0 call); yaml_stack_extend (47 calls);
yaml_strdup (21 calls); yaml_stream_end_event_initialize (0 call);
yaml_stream_start_event_initialize (0 call); yaml_string_extend (26 calls);
yaml_string_join (12 calls);
yaml_string_read_handler (address taken) (0 call);
yaml_string_write_handler (address taken) (0 call);
yaml_token_delete (7 calls);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (38)
===========================
main; yaml_alias_event_initialize; yaml_document_add_mapping;
yaml_document_add_scalar; yaml_document_add_sequence;
yaml_document_append_mapping_pair; yaml_document_append_sequence_item;
yaml_document_end_event_initialize; yaml_document_get_node;
yaml_document_get_root_node; yaml_document_initialize;
yaml_document_start_event_initialize; yaml_emitter_delete;
yaml_emitter_dump; yaml_emitter_initialize; yaml_emitter_set_break;
yaml_emitter_set_canonical; yaml_emitter_set_encoding;
yaml_emitter_set_indent; yaml_emitter_set_output;
yaml_emitter_set_output_file; yaml_emitter_set_output_string;
yaml_emitter_set_unicode; yaml_emitter_set_width; yaml_get_version;
yaml_get_version_string; yaml_mapping_end_event_initialize;
yaml_mapping_start_event_initialize; yaml_parser_load; yaml_parser_scan;
yaml_parser_set_encoding; yaml_parser_set_input;
yaml_parser_set_input_file; yaml_scalar_event_initialize;
yaml_sequence_end_event_initialize; yaml_sequence_start_event_initialize;
yaml_stream_end_event_initialize; yaml_stream_start_event_initialize;
Global metrics
==============
Sloc = 16578
Decision point = 3337
Global variables = 3
If = 3210
Loop = 106
Goto = 1588
Assignment = 7722
Exit point = 199
Function = 199
Function call = 1263
Pointer dereferencing = 8750
Cyclomatic complexity = 3536
tests/test-reader.c:147:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
tests/test-reader.c:254:[variadic] warning: Incorrect type for argument 2. The argument will be cast from int to unsigned int.
tests/test-reader.c:254:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
tests/test-reader.c:254:[variadic] warning: Incorrect type for argument 4. The argument will be cast from int to unsigned int.
tests/test-reader.c:254:[variadic] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
tests/test-reader.c:269:[variadic] warning: Incorrect type for argument 2. The argument will be cast from int to unsigned int.
tests/test-reader.c:325:[variadic] warning: Incorrect type for argument 2. The argument will be cast from int to unsigned int.
tests/test-reader.c:325:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
tests/test-reader.c:325:[variadic] warning: Incorrect type for argument 4. The argument will be cast from int to unsigned int.
tests/test-reader.c:325:[variadic] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
tests/test-reader.c:340:[variadic] warning: Incorrect type for argument 2. The argument will be cast from int to unsigned int.
directory file line function property kind status property
FRAMAC_SHARE/libc assert.h 31 __FC_assert precondition Unknown nonnull_c: c ≢ 0
FRAMAC_SHARE/libc string.h 137 strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
tests test-version.c 21 main precondition of __FC_assert Unknown nonnull_c: c ≢ 0
tests test-version.c 21 main precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 3 (out of 195)
Semantically reached functions = 3
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
19 stmts in analyzed functions, 19 stmts analyzed (100.0%)
main: 13 stmts out of 13 (100.0%)
yaml_get_version: 4 stmts out of 4 (100.0%)
yaml_get_version_string: 2 stmts out of 2 (100.0%)
This diff is collapsed.
[metrics] Defined functions (195)
=======================
main (0 call); yaml_alias_event_initialize (0 call);
yaml_check_utf8 (16 calls); yaml_document_add_mapping (0 call);
yaml_document_add_scalar (0 call); yaml_document_add_sequence (0 call);
yaml_document_append_mapping_pair (0 call);
yaml_document_append_sequence_item (0 call); yaml_document_delete (2 calls);
yaml_document_end_event_initialize (0 call);
yaml_document_get_node (0 call); yaml_document_get_root_node (0 call);
yaml_document_initialize (0 call);
yaml_document_start_event_initialize (0 call);
yaml_emitter_analyze_anchor (4 calls); yaml_emitter_analyze_event (1 call);
yaml_emitter_analyze_scalar (1 call); yaml_emitter_analyze_tag (3 calls);
yaml_emitter_analyze_tag_directive (1 call);
yaml_emitter_analyze_version_directive (1 call);
yaml_emitter_anchor_node (4 calls);
yaml_emitter_append_tag_directive (2 calls);
yaml_emitter_check_empty_document (1 call);
yaml_emitter_check_empty_mapping (2 calls);
yaml_emitter_check_empty_sequence (2 calls);
yaml_emitter_check_simple_key (2 calls); yaml_emitter_close (1 call);
yaml_emitter_delete (0 call);
yaml_emitter_delete_document_and_anchors (3 calls);
yaml_emitter_dump (0 call); yaml_emitter_dump_alias (1 call);
yaml_emitter_dump_mapping (1 call); yaml_emitter_dump_node (4 calls);
yaml_emitter_dump_scalar (1 call); yaml_emitter_dump_sequence (1 call);
yaml_emitter_emit (10 calls); yaml_emitter_emit_alias (1 call);
yaml_emitter_emit_block_mapping_key (2 calls);