Merge branch 'improve-miniz' into 'master'

[miniz] add more examples as use cases

See merge request !17

miniz/.frama-c/GNUmakefile

@@ -17,6 +17,7 @@ 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 \
@@ -29,14 +30,55 @@ EVAFLAGS    += \
 FCGUIFLAGS += \
 
 ## Analysis targets (suffixed with .eva)
-TARGETS = miniz.eva
+TARGETS = \
+  miniz-example1.eva \
+  miniz-example2.eva \
+  miniz-example3.eva \
+  miniz-example4.eva \
+  miniz-example5.eva \
+  miniz-example6.eva \
 
 ### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
-miniz.parse: \
+miniz-example1.parse: \
+  stubs.c \
   ../examples/example1.c \
   ../miniz.c \
   ../miniz_tdef.c \
 
+miniz-example2.parse: \
+  stubs.c \
+  ../examples/example2.c \
+  ../miniz.c \
+  ../miniz_tdef.c \
+  ../miniz_tinfl.c \
+  ../miniz_zip.c \
+
+miniz-example3.parse: \
+  stubs.c \
+  ../examples/example3.c \
+  ../miniz.c \
+  ../miniz_tdef.c \
+  ../miniz_tinfl.c \
+
+miniz-example4.parse: \
+  stubs.c \
+  ../examples/example4.c \
+  ../miniz.c \
+  ../miniz_tinfl.c \
+
+miniz-example5.parse: \
+  stubs.c \
+  ../examples/example5.c \
+  ../miniz.c \
+  ../miniz_tdef.c \
+  ../miniz_tinfl.c \
+
+miniz-example6.parse: \
+  stubs.c \
+  ../examples/example6.c \
+  ../miniz.c \
+  ../miniz_tdef.c \
+
 ### Epilogue. Do not modify this block. #######################################
 include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################

miniz/.frama-c/miniz.eva/metrics.log → miniz/.frama-c/miniz-example1.eva/metrics.log

 [metrics] Eva coverage statistics
 =======================
-Syntactically reachable functions = 41 (out of 58)
-Semantically reached functions = 18
-Coverage estimation = 43.9% 
+Syntactically reachable functions = 42 (out of 59)
+Semantically reached functions = 19
+Coverage estimation = 45.2% 
 
 Unreached functions (23) =
   <miniz.c>: miniz_def_free_func; mz_adler32; mz_inflate; mz_inflateEnd;
@@ -30,9 +30,10 @@ Function tdefl_compress_normal calls tdefl_record_match (at miniz_tdef.c:1196)
 Function tdefl_compress_normal calls tdefl_flush_block (at miniz_tdef.c:1217)
 [metrics] Statements analyzed by Eva
 --------------------------
-781 stmts in analyzed functions, 334 stmts analyzed (42.8%)
+794 stmts in analyzed functions, 347 stmts analyzed (43.7%)
 TDEFL_READ_UNALIGNED_WORD: 2 stmts out of 2 (100.0%)
 TDEFL_READ_UNALIGNED_WORD2: 2 stmts out of 2 (100.0%)
+eva_main: 13 stmts out of 13 (100.0%)
 miniz_def_alloc_func: 2 stmts out of 2 (100.0%)
 mz_compress: 2 stmts out of 2 (100.0%)
 mz_compressBound: 2 stmts out of 2 (100.0%)

miniz/.frama-c/miniz.eva/nonterm.log → miniz/.frama-c/miniz-example1.eva/nonterm.log

@@ -5,12 +5,14 @@ stack: tdefl_record_literal :: miniz_tdef.c:1193 <-
        mz_deflate :: miniz.c:335 <-
        mz_compress2 :: miniz.c:348 <-
        mz_compress :: examples/example1.c:43 <-
-       main
+       main :: stubs.c:21 <-
+       eva_main
 miniz_tdef.c:1088:[nonterm:stmt] warning: non-terminating loop
 stack: tdefl_compress_normal :: miniz_tdef.c:1293 <-
        tdefl_compress :: miniz.c:264 <-
        mz_deflate :: miniz.c:335 <-
        mz_compress2 :: miniz.c:348 <-
        mz_compress :: examples/example1.c:43 <-
-       main
+       main :: stubs.c:21 <-
+       eva_main
 miniz_tdef.c:1313:[nonterm:unreachable] warning: unreachable return

miniz/.frama-c/miniz.parse/framac.ast → miniz/.frama-c/miniz-example1.parse/framac.ast

 /* Generated by Frama-C */
+#include "__fc_builtin.h"
 #include "assert.h"
 #include "errno.h"
 #include "signal.h"
 #include "stdarg.h"
-#include "stddef.h"
 #include "stdint.h"
 #include "stdio.h"
 #include "stdlib.h"
@@ -251,6 +251,31 @@ struct __anonstruct_tdefl_output_buffer_26 {
    mz_bool m_expandable ;
 };
 typedef struct __anonstruct_tdefl_output_buffer_26 tdefl_output_buffer;
+int main(int argc, char **argv);
+
+int eva_main(void)
+{
+  char argv0[256];
+  char argv1[256];
+  char argv2[256];
+  char argv3[256];
+  char argv4[256];
+  int tmp_0;
+  int argc = Frama_C_interval(0,5);
+  char *argv[6] = {argv0, argv1, argv2, argv3, argv4, (char *)0};
+  {
+    int i = 0;
+    /*@ loop unroll 5; */
+    while (i < 5) {
+      Frama_C_make_unknown(argv[i],(unsigned long)255);
+      *(argv[i] + 255) = (char)0;
+      i ++;
+    }
+  }
+  tmp_0 = main(argc,argv);
+  return tmp_0;
+}
+
 void __attribute__((__visibility__("default"))) mz_free(void *p);
 
 mz_ulong __attribute__((__visibility__("default"))) mz_adler32(mz_ulong adler,

miniz/.frama-c/miniz.parse/metrics.log → miniz/.frama-c/miniz-example1.parse/metrics.log

-[metrics] Defined functions (57)
+[metrics] Defined functions (58)
 ======================
  TDEFL_READ_UNALIGNED_WORD (5 calls); TDEFL_READ_UNALIGNED_WORD2 (18 calls);
- TDEFL_READ_UNALIGNED_WORD32 (2 calls); main (0 call);
+ TDEFL_READ_UNALIGNED_WORD32 (2 calls); eva_main (0 call); main (1 call);
  miniz_def_alloc_func (address taken) (0 call);
  miniz_def_free_func (address taken) (0 call);
  miniz_def_realloc_func (0 call); mz_adler32 (1 call); mz_compress (1 call);
@@ -44,22 +44,22 @@ Undefined and unspecified functions (1)
 
 Potential entry points (13)
 ===========================
- main; miniz_def_realloc_func; mz_deflateReset; mz_error; mz_free;
+ eva_main; miniz_def_realloc_func; mz_deflateReset; mz_error; mz_free;
   mz_inflateReset; mz_version; tdefl_compress_mem_to_heap;
   tdefl_compress_mem_to_mem; tdefl_compressor_alloc; tdefl_compressor_free;
   tdefl_get_prev_return_status; tdefl_write_image_to_png_file_in_memory; 
 
 Global metrics
 ============== 
-Sloc = 2795
-Decision point = 457
+Sloc = 2808
+Decision point = 458
 Global variables = 14
-If = 457
-Loop = 94
+If = 458
+Loop = 95
 Goto = 117
-Assignment = 1405
-Exit point = 57
-Function = 58
-Function call = 206
-Pointer dereferencing = 1239
-Cyclomatic complexity = 514
+Assignment = 1411
+Exit point = 58
+Function = 59
+Function call = 209
+Pointer dereferencing = 1240
+Cyclomatic complexity = 516

miniz/.frama-c/miniz-example2.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 89 (out of 179)
+Semantically reached functions = 73
+Coverage estimation = 82.0% 
+
+Unreached functions (16) =
+  <miniz.c>: mz_adler32; 
+  <miniz_tdef.c>: tdefl_calculate_minimum_redundancy; tdefl_compress_block;
+    tdefl_compress_fast; tdefl_compress_lz_codes; tdefl_flush_block;
+    tdefl_flush_output_buffer; tdefl_huffman_enforce_max_code_size;
+    tdefl_optimize_huffman_table; tdefl_radix_sort_syms;
+    TDEFL_READ_UNALIGNED_WORD32; tdefl_record_match;
+    tdefl_start_dynamic_block; tdefl_start_static_block; 
+  <miniz_zip.c>: mz_zip_heap_write_func; mz_zip_writer_add_put_buf_callback;
+[metrics] References to non-analyzed functions
+------------------------------------
+Function mz_zip_writer_add_mem_ex_v2 references mz_zip_writer_add_put_buf_callback (at miniz_zip.c:3367)
+Function mz_zip_writer_end_internal references mz_zip_heap_write_func (at miniz_zip.c:2676)
+Function mz_zip_writer_init_from_reader_v2 references mz_zip_heap_write_func (at miniz_zip.c:2929)
+Function tdefl_compress calls tdefl_flush_output_buffer (at miniz_tdef.c:1280)
+Function tdefl_compress calls tdefl_compress_fast (at miniz_tdef.c:1287)
+Function tdefl_compress calls mz_adler32 (at miniz_tdef.c:1298)
+Function tdefl_compress calls tdefl_flush_block (at miniz_tdef.c:1302)
+Function tdefl_compress calls tdefl_flush_output_buffer (at miniz_tdef.c:1313)
+Function tdefl_compress_normal calls tdefl_record_match (at miniz_tdef.c:1174)
+Function tdefl_compress_normal calls tdefl_record_match (at miniz_tdef.c:1187)
+Function tdefl_compress_normal calls tdefl_record_match (at miniz_tdef.c:1196)
+Function tdefl_compress_normal calls tdefl_flush_block (at miniz_tdef.c:1217)
+[metrics] Statements analyzed by Eva
+--------------------------
+4017 stmts in analyzed functions, 2311 stmts analyzed (57.5%)
+TDEFL_READ_UNALIGNED_WORD: 2 stmts out of 2 (100.0%)
+TDEFL_READ_UNALIGNED_WORD2: 2 stmts out of 2 (100.0%)
+eva_main: 13 stmts out of 13 (100.0%)
+main: 131 stmts out of 131 (100.0%)
+miniz_def_alloc_func: 2 stmts out of 2 (100.0%)
+miniz_def_free_func: 2 stmts out of 2 (100.0%)
+miniz_def_realloc_func: 2 stmts out of 2 (100.0%)
+mz_crc32: 21 stmts out of 21 (100.0%)
+mz_free: 2 stmts out of 2 (100.0%)
+mz_write_le16: 3 stmts out of 3 (100.0%)
+mz_write_le32: 5 stmts out of 5 (100.0%)
+mz_write_le64: 3 stmts out of 3 (100.0%)
+mz_zip_add_mem_to_archive_file_in_place: 2 stmts out of 2 (100.0%)
+mz_zip_array_clear: 3 stmts out of 3 (100.0%)
+mz_zip_array_ensure_capacity: 23 stmts out of 23 (100.0%)
+mz_zip_array_ensure_room: 2 stmts out of 2 (100.0%)
+mz_zip_array_push_back: 10 stmts out of 10 (100.0%)
+mz_zip_array_reserve: 8 stmts out of 8 (100.0%)
+mz_zip_array_resize: 9 stmts out of 9 (100.0%)
+mz_zip_dos_to_time_t: 10 stmts out of 10 (100.0%)
+mz_zip_file_read_func: 16 stmts out of 16 (100.0%)
+mz_zip_file_write_func: 16 stmts out of 16 (100.0%)
+mz_zip_filename_compare: 36 stmts out of 36 (100.0%)
+mz_zip_locate_file_binary_search: 31 stmts out of 31 (100.0%)
+mz_zip_reader_end: 2 stmts out of 2 (100.0%)
+mz_zip_reader_extract_file_to_heap: 10 stmts out of 10 (100.0%)
+mz_zip_reader_extract_to_mem: 2 stmts out of 2 (100.0%)
+mz_zip_reader_file_stat: 7 stmts out of 7 (100.0%)
+mz_zip_reader_filename_less: 39 stmts out of 39 (100.0%)
+mz_zip_reader_init_file: 2 stmts out of 2 (100.0%)
+mz_zip_reader_is_file_a_directory: 21 stmts out of 21 (100.0%)
+mz_zip_reader_is_file_encrypted: 9 stmts out of 9 (100.0%)
+mz_zip_reader_is_file_supported: 26 stmts out of 26 (100.0%)
+mz_zip_reader_sort_central_dir_offsets_by_filename: 72 stmts out of 72 (100.0%)
+mz_zip_set_error: 4 stmts out of 4 (100.0%)
+mz_zip_time_t_to_dos_time: 4 stmts out of 4 (100.0%)
+mz_zip_writer_add_mem_ex: 2 stmts out of 2 (100.0%)
+mz_zip_writer_end: 2 stmts out of 2 (100.0%)
+mz_zip_writer_validate_archive_name: 6 stmts out of 6 (100.0%)
+mz_zip_zero_struct: 3 stmts out of 3 (100.0%)
+tdefl_init: 80 stmts out of 80 (100.0%)
+mz_zip_reader_read_central_dir: 269 stmts out of 273 (98.5%)
+mz_zip_file_stat_internal: 108 stmts out of 110 (98.2%)
+mz_zip_writer_finalize_archive: 102 stmts out of 104 (98.1%)
+mz_zip_writer_create_central_dir_header: 39 stmts out of 41 (95.1%)
+mz_zip_writer_create_local_dir_header: 30 stmts out of 32 (93.8%)
+mz_zip_reader_locate_header_sig: 44 stmts out of 47 (93.6%)
+mz_zip_reader_end_internal: 33 stmts out of 36 (91.7%)
+mz_zip_writer_add_to_central_dir: 41 stmts out of 45 (91.1%)
+mz_zip_writer_end_internal: 34 stmts out of 38 (89.5%)
+mz_zip_reader_init_file_v2: 47 stmts out of 54 (87.0%)
+mz_zip_string_equal: 25 stmts out of 29 (86.2%)
+mz_zip_reader_init_internal: 30 stmts out of 36 (83.3%)
+mz_zip_reader_extract_to_heap: 29 stmts out of 35 (82.9%)
+mz_zip_writer_add_mem_ex_v2: 266 stmts out of 329 (80.9%)
+mz_zip_reader_get_num_files: 4 stmts out of 5 (80.0%)
+mz_zip_add_mem_to_archive_file_in_place_v2: 62 stmts out of 78 (79.5%)
+mz_zip_get_cdh: 11 stmts out of 14 (78.6%)
+mz_zip_reader_extract_to_mem_no_alloc: 142 stmts out of 182 (78.0%)
+tdefl_create_comp_flags_from_zip_params: 22 stmts out of 29 (75.9%)
+mz_zip_writer_init_from_reader_v2: 56 stmts out of 74 (75.7%)
+mz_zip_writer_compute_padding_needed_for_file_alignment: 5 stmts out of 7 (71.4%)
+mz_zip_writer_create_zip64_extra_data: 14 stmts out of 20 (70.0%)
+tdefl_compress_buffer: 2 stmts out of 3 (66.7%)
+mz_zip_writer_init_v2: 33 stmts out of 50 (66.0%)
+mz_zip_reader_locate_file_v2: 48 stmts out of 82 (58.5%)
+mz_zip_writer_init_file_v2: 26 stmts out of 49 (53.1%)
+tdefl_record_literal: 6 stmts out of 15 (40.0%)
+tdefl_compress_normal: 58 stmts out of 166 (34.9%)
+mz_zip_writer_write_zeros: 8 stmts out of 24 (33.3%)
+tdefl_compress: 32 stmts out of 103 (31.1%)
+tdefl_find_match: 29 stmts out of 142 (20.4%)
+tinfl_decompress: 11 stmts out of 1120 (1.0%)

miniz/.frama-c/miniz-example2.eva/nonterm.log

+miniz_tdef.c:1043:[nonterm:stmt] warning: non-terminating statement
+stack: tdefl_record_literal :: miniz_tdef.c:1193 <-
+       tdefl_compress_normal :: miniz_tdef.c:1293 <-
+       tdefl_compress :: miniz_tdef.c:1319 <-
+       tdefl_compress_buffer :: miniz_zip.c:3368 <-
+       mz_zip_writer_add_mem_ex_v2 :: miniz_zip.c:3139 <-
+       mz_zip_writer_add_mem_ex :: miniz_zip.c:4409 <-
+       mz_zip_add_mem_to_archive_file_in_place_v2 :: miniz_zip.c:4346 <-
+       mz_zip_add_mem_to_archive_file_in_place :: examples/example2.c:64 <-
+       main :: stubs.c:21 <-
+       eva_main
+miniz_tdef.c:1088:[nonterm:stmt] warning: non-terminating loop
+stack: tdefl_compress_normal :: miniz_tdef.c:1293 <-
+       tdefl_compress :: miniz_tdef.c:1319 <-
+       tdefl_compress_buffer :: miniz_zip.c:3368 <-
+       mz_zip_writer_add_mem_ex_v2 :: miniz_zip.c:3139 <-
+       mz_zip_writer_add_mem_ex :: miniz_zip.c:4409 <-
+       mz_zip_add_mem_to_archive_file_in_place_v2 :: miniz_zip.c:4346 <-
+       mz_zip_add_mem_to_archive_file_in_place :: examples/example2.c:64 <-
+       main :: stubs.c:21 <-
+       eva_main
+miniz_tdef.c:1313:[nonterm:unreachable] warning: unreachable return
+miniz_tdef.c:1319:[nonterm:unreachable] warning: unreachable return
+miniz_tinfl.c:197:[nonterm:stmt] warning: non-terminating statement
+stack: tinfl_decompress :: miniz_zip.c:1544 <-
+       mz_zip_reader_extract_to_mem_no_alloc :: miniz_zip.c:1583 <-
+       mz_zip_reader_extract_to_mem :: miniz_zip.c:1622 <-
+       mz_zip_reader_extract_to_heap :: miniz_zip.c:1642 <-
+       mz_zip_reader_extract_file_to_heap :: examples/example2.c:134 <-
+       main :: stubs.c:21 <-
+       eva_main

miniz/.frama-c/miniz-example2.eva/warnings.log

+miniz_zip.c:2910:[eva:garbled-mix] warning: The specification of function freopen has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:2782:[eva:garbled-mix] warning: The specification of function fseeko has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:2788:[eva:garbled-mix] warning: The specification of function fwrite has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:4303:[eva:garbled-mix] warning: The specification of function fflush has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:4303:[eva:garbled-mix] warning: The specification of function fflush has generated a garbled mix for assigns clause __fc_fopen[
+0 .. 16 - 1].
+miniz_zip.c:998:[eva:garbled-mix] warning: The specification of function fseeko has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:972:[eva:garbled-mix] warning: The specification of function fseeko has generated a garbled mix for assigns clause *stream.
+miniz_zip.c:975:[eva:garbled-mix] warning: The specification of function fread has generated a garbled mix for assigns clause *stream.

miniz/.frama-c/miniz-example2.parse/metrics.log

+[metrics] Defined functions (179)
+=======================
+ TDEFL_READ_UNALIGNED_WORD (5 calls); TDEFL_READ_UNALIGNED_WORD2 (18 calls);
+ TDEFL_READ_UNALIGNED_WORD32 (2 calls); eva_main (0 call); main (1 call);
+ miniz_def_alloc_func (address taken) (0 call);
+ miniz_def_free_func (address taken) (0 call);
+ miniz_def_realloc_func (address taken) (0 call); mz_adler32 (1 call);
+ mz_compress (0 call); mz_compress2 (1 call); mz_compressBound (0 call);
+ mz_crc32 (13 calls); mz_deflate (1 call); mz_deflateBound (1 call);
+ mz_deflateEnd (3 calls); mz_deflateInit (1 call); mz_deflateInit2 (1 call);
+ mz_deflateReset (0 call); mz_error (0 call);
+ mz_file_read_func_stdio (address taken) (0 call); mz_free (2 calls);
+ mz_inflate (1 call); mz_inflateEnd (2 calls); mz_inflateInit (1 call);
+ mz_inflateInit2 (1 call); mz_inflateReset (0 call); mz_uncompress (0 call);
+ mz_uncompress2 (1 call); mz_version (0 call); mz_write_le16 (26 calls);
+ mz_write_le32 (33 calls); mz_write_le64 (18 calls);
+ mz_zip_add_mem_to_archive_file_in_place (2 calls);
+ mz_zip_add_mem_to_archive_file_in_place_v2 (1 call);
+ mz_zip_array_clear (20 calls); mz_zip_array_ensure_capacity (2 calls);
+ mz_zip_array_ensure_room (2 calls); mz_zip_array_init (3 calls);
+ mz_zip_array_push_back (15 calls); mz_zip_array_reserve (2 calls);
+ mz_zip_array_resize (14 calls); mz_zip_clear_last_error (0 call);
+ mz_zip_compute_crc32_callback (address taken) (0 call);
+ mz_zip_dos_to_time_t (1 call); mz_zip_end (0 call);
+ mz_zip_extract_archive_file_to_heap (0 call);
+ mz_zip_extract_archive_file_to_heap_v2 (1 call);
+ mz_zip_file_read_func (address taken) (0 call);
+ mz_zip_file_stat_internal (3 calls);
+ mz_zip_file_write_callback (address taken) (0 call);
+ mz_zip_file_write_func (address taken) (0 call);
+ mz_zip_filename_compare (1 call);
+ mz_zip_get_archive_file_start_offset (0 call);
+ mz_zip_get_archive_size (0 call); mz_zip_get_cdh (8 calls);
+ mz_zip_get_central_dir_size (0 call); mz_zip_get_cfile (0 call);
+ mz_zip_get_error_string (0 call); mz_zip_get_file_modified_time (1 call);
+ mz_zip_get_last_error (0 call); mz_zip_get_mode (0 call);
+ mz_zip_get_type (0 call); mz_zip_heap_write_func (address taken) (0 call);
+ mz_zip_is_zip64 (0 call); mz_zip_locate_file_binary_search (1 call);
+ mz_zip_mem_read_func (address taken) (0 call);
+ mz_zip_peek_last_error (0 call); mz_zip_read_archive_data (0 call);
+ mz_zip_reader_end (7 calls); mz_zip_reader_end_internal (10 calls);
+ mz_zip_reader_extract_file_iter_new (0 call);
+ mz_zip_reader_extract_file_to_callback (0 call);
+ mz_zip_reader_extract_file_to_cfile (0 call);
+ mz_zip_reader_extract_file_to_file (0 call);
+ mz_zip_reader_extract_file_to_heap (1 call);
+ mz_zip_reader_extract_file_to_mem (0 call);
+ mz_zip_reader_extract_file_to_mem_no_alloc (1 call);
+ mz_zip_reader_extract_iter_free (0 call);
+ mz_zip_reader_extract_iter_new (1 call);
+ mz_zip_reader_extract_iter_read (0 call);
+ mz_zip_reader_extract_to_callback (4 calls);
+ mz_zip_reader_extract_to_cfile (1 call);
+ mz_zip_reader_extract_to_file (1 call);
+ mz_zip_reader_extract_to_heap (2 calls);
+ mz_zip_reader_extract_to_mem (1 call);
+ mz_zip_reader_extract_to_mem_no_alloc (2 calls);
+ mz_zip_reader_file_stat (7 calls); mz_zip_reader_filename_less (4 calls);
+ mz_zip_reader_get_filename (0 call); mz_zip_reader_get_num_files (1 call);
+ mz_zip_reader_init (0 call); mz_zip_reader_init_cfile (0 call);
+ mz_zip_reader_init_file (2 calls); mz_zip_reader_init_file_v2 (4 calls);
+ mz_zip_reader_init_internal (4 calls); mz_zip_reader_init_mem (1 call);
+ mz_zip_reader_is_file_a_directory (3 calls);
+ mz_zip_reader_is_file_encrypted (1 call);
+ mz_zip_reader_is_file_supported (1 call);
+ mz_zip_reader_locate_file (0 call); mz_zip_reader_locate_file_v2 (9 calls);
+ mz_zip_reader_locate_header_sig (1 call);
+ mz_zip_reader_read_central_dir (4 calls);
+ mz_zip_reader_sort_central_dir_offsets_by_filename (1 call);
+ mz_zip_set_error (256 calls); mz_zip_set_file_times (1 call);
+ mz_zip_set_last_error (1 call); mz_zip_string_equal (2 calls);
+ mz_zip_time_t_to_dos_time (3 calls); mz_zip_validate_archive (2 calls);
+ mz_zip_validate_file (1 call); mz_zip_validate_file_archive (0 call);
+ mz_zip_validate_mem_archive (0 call); mz_zip_writer_add_cfile (1 call);
+ mz_zip_writer_add_file (0 call); mz_zip_writer_add_from_zip_reader (0 call);
+ mz_zip_writer_add_mem (0 call); mz_zip_writer_add_mem_ex (2 calls);
+ mz_zip_writer_add_mem_ex_v2 (1 call);
+ mz_zip_writer_add_put_buf_callback (address taken) (0 call);
+ mz_zip_writer_add_read_buf_callback (1 call);
+ mz_zip_writer_add_to_central_dir (2 calls);
+ mz_zip_writer_compute_padding_needed_for_file_alignment (3 calls);
+ mz_zip_writer_create_central_dir_header (1 call);
+ mz_zip_writer_create_local_dir_header (4 calls);
+ mz_zip_writer_create_zip64_extra_data (4 calls);
+ mz_zip_writer_end (3 calls); mz_zip_writer_end_internal (3 calls);
+ mz_zip_writer_finalize_archive (2 calls);
+ mz_zip_writer_finalize_heap_archive (0 call); mz_zip_writer_init (0 call);
+ mz_zip_writer_init_cfile (0 call); mz_zip_writer_init_file (0 call);
+ mz_zip_writer_init_file_v2 (2 calls);
+ mz_zip_writer_init_from_reader (0 call);
+ mz_zip_writer_init_from_reader_v2 (2 calls);
+ mz_zip_writer_init_heap (0 call); mz_zip_writer_init_heap_v2 (1 call);
+ mz_zip_writer_init_v2 (4 calls);
+ mz_zip_writer_update_zip64_extension_block (1 call);
+ mz_zip_writer_validate_archive_name (3 calls);
+ mz_zip_writer_write_zeros (3 calls); mz_zip_zero_struct (4 calls);
+ tdefl_calculate_minimum_redundancy (1 call); tdefl_compress (2 calls);
+ tdefl_compress_block (2 calls); tdefl_compress_buffer (6 calls);
+ tdefl_compress_fast (1 call); tdefl_compress_lz_codes (1 call);
+ tdefl_compress_mem_to_heap (0 call); tdefl_compress_mem_to_mem (0 call);
+ tdefl_compress_mem_to_output (2 calls); tdefl_compress_normal (1 call);
+ tdefl_compressor_alloc (0 call); tdefl_compressor_free (0 call);
+ tdefl_create_comp_flags_from_zip_params (3 calls);
+ tdefl_find_match (1 call); tdefl_flush_block (4 calls);
+ tdefl_flush_output_buffer (2 calls); tdefl_get_adler32 (1 call);
+ tdefl_get_prev_return_status (0 call);
+ tdefl_huffman_enforce_max_code_size (1 call); tdefl_init (6 calls);
+ tdefl_optimize_huffman_table (5 calls);
+ tdefl_output_buffer_putter (address taken) (2 calls);
+ tdefl_radix_sort_syms (1 call); tdefl_record_literal (2 calls);
+ tdefl_record_match (3 calls); tdefl_start_dynamic_block (1 call);
+ tdefl_start_static_block (1 call);
+ tdefl_write_image_to_png_file_in_memory (0 call);
+ tdefl_write_image_to_png_file_in_memory_ex (1 call);
+ tinfl_decompress (8 calls); tinfl_decompress_mem_to_callback (0 call);
+ tinfl_decompress_mem_to_heap (0 call); tinfl_decompress_mem_to_mem (0 call);
+ tinfl_decompressor_alloc (0 call); tinfl_decompressor_free (0 call); 
+
+Specified-only functions (0)
+============================
+ 
+
+Undefined and unspecified functions (0)
+=======================================
+ 
+
+'Extern' global variables (0)
+=============================
+ 
+
+Potential entry points (55)
+===========================
+ eva_main; mz_compress; mz_compressBound; mz_deflateReset; mz_error;
+  mz_inflateReset; mz_uncompress; mz_version; mz_zip_clear_last_error;
+  mz_zip_end; mz_zip_extract_archive_file_to_heap;
+  mz_zip_get_archive_file_start_offset; mz_zip_get_archive_size;
+  mz_zip_get_central_dir_size; mz_zip_get_cfile; mz_zip_get_error_string;
+  mz_zip_get_last_error; mz_zip_get_mode; mz_zip_get_type; mz_zip_is_zip64;
+  mz_zip_peek_last_error; mz_zip_read_archive_data;
+  mz_zip_reader_extract_file_iter_new;
+  mz_zip_reader_extract_file_to_callback;
+  mz_zip_reader_extract_file_to_cfile; mz_zip_reader_extract_file_to_file;
+  mz_zip_reader_extract_file_to_mem; mz_zip_reader_extract_iter_free;
+  mz_zip_reader_extract_iter_read; mz_zip_reader_get_filename;
+  mz_zip_reader_init; mz_zip_reader_init_cfile; mz_zip_reader_locate_file;
+  mz_zip_validate_file_archive; mz_zip_validate_mem_archive;
+  mz_zip_writer_add_file; mz_zip_writer_add_from_zip_reader;
+  mz_zip_writer_add_mem; mz_zip_writer_finalize_heap_archive;
+  mz_zip_writer_init; mz_zip_writer_init_cfile; mz_zip_writer_init_file;
+  mz_zip_writer_init_from_reader; mz_zip_writer_init_heap;
+  tdefl_compress_mem_to_heap; tdefl_compress_mem_to_mem;
+  tdefl_compressor_alloc; tdefl_compressor_free;
+  tdefl_get_prev_return_status; tdefl_write_image_to_png_file_in_memory;
+  tinfl_decompress_mem_to_callback; tinfl_decompress_mem_to_heap;
+  tinfl_decompress_mem_to_mem; tinfl_decompressor_alloc;
+  tinfl_decompressor_free; 
+
+Global metrics
+============== 
+Sloc = 8478
+Decision point = 1622
+Global variables = 22
+If = 1558
+Loop = 211
+Goto = 660
+Assignment = 3859
+Exit point = 179
+Function = 179
+Function call = 991
+Pointer dereferencing = 2782
+Cyclomatic complexity = 1801

miniz/.frama-c/miniz-example2.parse/warnings.log

+examples/example2.c:58:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
+examples/example2.c:59:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
+examples/example2.c:59:[variadic] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
+examples/example2.c:101:[variadic] warning: Incorrect type for argument 6. The argument will be cast from int to unsigned int.
+examples/example2.c:130:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
+examples/example2.c:131:[variadic] warning: Incorrect type for argument 3. The argument will be cast from int to unsigned int.
+examples/example2.c:131:[variadic] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.

miniz/.frama-c/miniz-example3.eva/metrics.log

+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 36 (out of 64)
+Semantically reached functions = 35
+Coverage estimation = 97.2% 
+
+Unreached functions (1) =
+  <miniz.c>: mz_inflateEnd;
+[metrics] References to non-analyzed functions
+------------------------------------
+Function main calls mz_inflateEnd (at examples/example3.c:246)
+[metrics] Statements analyzed by Eva
+--------------------------
+3726 stmts in analyzed functions, 2306 stmts analyzed (61.9%)
+TDEFL_READ_UNALIGNED_WORD: 2 stmts out of 2 (100.0%)
+TDEFL_READ_UNALIGNED_WORD2: 2 stmts out of 2 (100.0%)
+TDEFL_READ_UNALIGNED_WORD32: 2 stmts out of 2 (100.0%)
+eva_main: 13 stmts out of 13 (100.0%)
+miniz_def_alloc_func: 2 stmts out of 2 (100.0%)
+miniz_def_free_func: 2 stmts out of 2 (100.0%)
+mz_deflateInit: 2 stmts out of 2 (100.0%)
+mz_inflateInit: 2 stmts out of 2 (100.0%)
+tdefl_calculate_minimum_redundancy: 82 stmts out of 82 (100.0%)
+tdefl_compress_block: 5 stmts out of 5 (100.0%)
+tdefl_compress_lz_codes: 131 stmts out of 131 (100.0%)
+tdefl_find_match: 142 stmts out of 142 (100.0%)
+tdefl_flush_output_buffer: 18 stmts out of 18 (100.0%)
+tdefl_get_adler32: 2 stmts out of 2 (100.0%)
+tdefl_huffman_enforce_max_code_size: 32 stmts out of 32 (100.0%)
+tdefl_init: 80 stmts out of 80 (100.0%)
+tdefl_optimize_huffman_table: 79 stmts out of 79 (100.0%)
+tdefl_radix_sort_syms: 51 stmts out of 51 (100.0%)
+tdefl_record_literal: 15 stmts out of 15 (100.0%)
+tdefl_record_match: 33 stmts out of 33 (100.0%)
+tdefl_start_static_block: 55 stmts out of 55 (100.0%)
+tdefl_compress_fast: 256 stmts out of 257 (99.6%)
+tdefl_compress_normal: 164 stmts out of 166 (98.8%)
+mz_adler32: 46 stmts out of 49 (93.9%)
+tdefl_start_dynamic_block: 366 stmts out of 399 (91.7%)
+main: 206 stmts out of 230 (89.6%)
+tdefl_compress: 87 stmts out of 103 (84.5%)
+mz_inflateInit2: 28 stmts out of 35 (80.0%)
+tdefl_create_comp_flags_from_zip_params: 23 stmts out of 29 (79.3%)
+tdefl_flush_block: 251 stmts out of 318 (78.9%)
+mz_deflate: 55 stmts out of 72 (76.4%)
+mz_deflateEnd: 6 stmts out of 9 (66.7%)
+mz_deflateInit2: 27 stmts out of 47 (57.4%)
+mz_inflate: 28 stmts out of 140 (20.0%)
+tinfl_decompress: 11 stmts out of 1120 (1.0%)

miniz/.frama-c/miniz-example3.eva/nonterm.log

+miniz_tinfl.c:197:[nonterm:stmt] warning: non-terminating statement
+stack: tinfl_decompress :: miniz.c:506 <-
+       mz_inflate :: examples/example3.c:222 <-
+       main :: stubs.c:21 <-
+       eva_main

miniz/.frama-c/miniz-example3.eva/warnings.log

+examples/example3.c:161:[eva:locals-escaping] warning: locals {in_bytes} escaping the scope of mz_deflate through __malloc_miniz_def_alloc_func_l169
+examples/example3.c:161:[eva:locals-escaping] warning: locals {out_bytes} escaping the scope of mz_deflate through __malloc_miniz_def_alloc_func_l169