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

[gzip124] improve parametrization

parent afcd3024
No related branches found
No related tags found
1 merge request!50[gzip124] improve parametrization
Pipeline #67325 passed
Stage: test
    Expand all Hide whitespace changes
    Inline Side-by-side
    Showing
    with 7189 additions and 6807 deletions
    gzip124/.frama-c/GNUmakefile
    + 19
    − 15
    View file @ 481d0c58
    ......@@ -29,11 +29,15 @@ FCFLAGS += \
    ## Eva-specific flags
    EVAFLAGS += \
    -eva-slevel 4 \
    -eva-slevel 2 \
    -eva-no-alloc-returns-null \
    -eva-no-builtins-auto \
    -eva-widening-delay 3 \
    -eva-widening-period 3 \
    # Comparison with other parametrizations
    # Baseline: -eva-no-alloc-returns-null -eva-slevel 2: time 120s
    # -eva-slevel 3: time 511s, -0 alarms
    # -eva-domains equality: time 201s, -12 alarms
    # -eva-domains gauges: time 351s, -4 alarms
    # -eva-domains equality,gauges: time 491s, -17 alarms
    ## GUI-only flags
    FCGUIFLAGS += \
    ......@@ -41,22 +45,22 @@ FCGUIFLAGS += \
    TARGETS = gzip124.eva
    gzip124.parse: \
    ../gzip.c \
    ../zip.c \
    ../deflate.c \
    ../trees.c \
    $(shell $(FRAMAC)-config -print-share-path)/libc/stdlib.c \
    fc_stubs.c \
    ../bits.c \
    ../unzip.c \
    ../inflate.c \
    ../util.c \
    ../crypt.c \
    ../deflate.c \
    ../getopt.c \
    ../gzip.c \
    ../inflate.c \
    ../lzw.c \
    ../trees.c \
    ../unlzh.c \
    ../unlzw.c \
    ../unpack.c \
    ../unlzh.c \
    ../getopt.c \
    $(shell $(FRAMAC)-config -print-share-path)/libc/stdlib.c \
    fc_stubs.c \
    ../unzip.c \
    ../util.c \
    ../zip.c \
    ### Epilogue. Do not modify this block. #######################################
    include $(shell $(FRAMAC)-config -print-lib-path)/analysis-scripts/epilogue.mk
    ......
    gzip124/.frama-c/gzip124.eva/alarms.csv
    + 560
    − 144
    View file @ 481d0c58
    This diff is collapsed.
    gzip124/.frama-c/gzip124.eva/metrics.log
    + 12
    − 12
    View file @ 481d0c58
    ......@@ -13,7 +13,7 @@ Function flush_block calls set_file_type (at trees.c:864)
    Function main references lzw (at gzip.c:573)
    [metrics] Statements analyzed by Eva
    --------------------------
    4844 stmts in analyzed functions, 4292 stmts analyzed (88.6%)
    4844 stmts in analyzed functions, 4728 stmts analyzed (97.6%)
    bi_init: 6 stmts out of 6 (100.0%)
    bi_reverse: 11 stmts out of 11 (100.0%)
    bi_windup: 36 stmts out of 36 (100.0%)
    ......@@ -52,7 +52,12 @@ getbits: 3 stmts out of 3 (100.0%)
    getopt_long: 2 stmts out of 2 (100.0%)
    help: 13 stmts out of 13 (100.0%)
    huf_decode_start: 3 stmts out of 3 (100.0%)
    huft_free: 12 stmts out of 12 (100.0%)
    inflate: 26 stmts out of 26 (100.0%)
    inflate_block: 59 stmts out of 59 (100.0%)
    inflate_codes: 202 stmts out of 202 (100.0%)
    inflate_dynamic: 279 stmts out of 279 (100.0%)
    inflate_fixed: 49 stmts out of 49 (100.0%)
    inflate_stored: 87 stmts out of 87 (100.0%)
    init_block: 29 stmts out of 29 (100.0%)
    init_getbits: 5 stmts out of 5 (100.0%)
    ......@@ -78,32 +83,27 @@ treat_stdin: 83 stmts out of 83 (100.0%)
    unlzh: 13 stmts out of 13 (100.0%)
    unlzw: 167 stmts out of 167 (100.0%)
    unpack: 66 stmts out of 66 (100.0%)
    unzip: 118 stmts out of 118 (100.0%)
    updcrc: 16 stmts out of 16 (100.0%)
    usage: 2 stmts out of 2 (100.0%)
    version: 6 stmts out of 6 (100.0%)
    write_buf: 13 stmts out of 13 (100.0%)
    xmalloc: 4 stmts out of 4 (100.0%)
    unzip: 117 stmts out of 118 (99.2%)
    add_envopt: 90 stmts out of 91 (98.9%)
    check_ofname: 68 stmts out of 69 (98.6%)
    huft_build: 208 stmts out of 213 (97.7%)
    flush_block: 39 stmts out of 40 (97.5%)
    main: 146 stmts out of 154 (94.8%)
    main: 147 stmts out of 154 (95.5%)
    copy: 17 stmts out of 18 (94.4%)
    lm_init: 43 stmts out of 46 (93.5%)
    _getopt_internal: 216 stmts out of 232 (93.1%)
    eva_main: 12 stmts out of 13 (92.3%)
    shorten_name: 58 stmts out of 63 (92.1%)
    huft_build: 193 stmts out of 213 (90.6%)
    inflate_fixed: 42 stmts out of 49 (85.7%)
    zip: 191 stmts out of 225 (84.9%)
    inflate: 22 stmts out of 26 (84.6%)
    basename: 5 stmts out of 6 (83.3%)
    read_error: 5 stmts out of 6 (83.3%)
    do_exit: 9 stmts out of 11 (81.8%)
    abort_gzip: 4 stmts out of 5 (80.0%)
    write_error: 3 stmts out of 4 (75.0%)
    xmalloc: 3 stmts out of 4 (75.0%)
    error: 2 stmts out of 3 (66.7%)
    huft_free: 6 stmts out of 12 (50.0%)
    inflate_dynamic: 132 stmts out of 279 (47.3%)
    do_exit: 5 stmts out of 11 (45.5%)
    get_istat: 17 stmts out of 49 (34.7%)
    add_envopt: 14 stmts out of 91 (15.4%)
    inflate_codes: 24 stmts out of 202 (11.9%)
    gzip124/.frama-c/gzip124.eva/nonterm.log
    + 7
    − 101
    View file @ 481d0c58
    fc_stubs.c:21:[nonterm:unreachable] warning: unreachable return
    gzip.c:602:[nonterm:unreachable] warning: unreachable return
    gzip.c:1747:[nonterm:unreachable] warning: unreachable return
    inflate.c:412:[nonterm:stmt] warning: non-terminating statement
    stack 1: huft_build :: inflate.c:675 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 2: huft_build :: inflate.c:683 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 3: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:439:[nonterm:stmt] warning: non-terminating statement
    stack: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:454:[nonterm:stmt] warning: non-terminating statement
    stack 1: huft_build :: inflate.c:675 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 2: huft_build :: inflate.c:683 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 3: huft_build :: inflate.c:763 <-
    stack 1: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:513:[nonterm:stmt] warning: non-terminating loop
    stack 1: inflate_codes :: inflate.c:691 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:817 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 2: inflate_codes :: inflate.c:691 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    treat_stdin :: gzip.c:596 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:516:[nonterm:stmt] warning: non-terminating statement
    stack 1: inflate_codes :: inflate.c:691 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:817 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 2: inflate_codes :: inflate.c:691 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:778:[nonterm:stmt] warning: non-terminating statement
    stack 1: inflate_dynamic :: inflate.c:900 <-
    stack 2: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:817 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    stack 2: inflate_dynamic :: inflate.c:900 <-
    stack 3: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    ......@@ -118,9 +27,6 @@ stack 2: inflate_dynamic :: inflate.c:900 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    util.c:294:[nonterm:stmt] warning: non-terminating function call
    stack: add_envopt :: gzip.c:443 <- main :: fc_stubs.c:21 <- eva_main
    util.c:341:[nonterm:unreachable] warning: unreachable return
    util.c:358:[nonterm:unreachable] warning: unreachable return
    util.c:365:[nonterm:unreachable] warning: unreachable return
    fc_stubs.c:21:[nonterm:unreachable] warning: unreachable return
    gzip124/.frama-c/gzip124.eva/warnings.log
    + 58
    − 36
    View file @ 481d0c58
    util.c:186:[eva:garbled-mix:assigns] warning: The specification of function strrchr
    has generated a garbled mix of addresses for assigns clause \result.
    util.c:400:[eva] warning: ignoring unsupported allocates clause
    util.c:311:[eva] warning: calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
    FRAMAC_SHARE/libc/signal.h:129:[eva] warning: no 'assigns \result \from ...' clause specified for function signal
    inflate.c:403:[eva] warning: ignoring unsupported allocates clause
    inflate.c:412:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
    stack: huft_build :: inflate.c:763 <-
    inflate_dynamic :: inflate.c:900 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:412:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
    stack: huft_build :: inflate.c:675 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    inflate.c:412:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
    stack: huft_build :: inflate.c:683 <-
    inflate_fixed :: inflate.c:904 <-
    inflate_block :: inflate.c:931 <-
    inflate :: unzip.c:120 <-
    unzip :: gzip.c:675 <-
    treat_stdin :: gzip.c:710 <-
    treat_file :: gzip.c:593 <-
    main :: fc_stubs.c:21 <-
    eva_main
    gzip.c:675:[eva:locals-escaping] warning: locals {attr} escaping the scope of zip through file_type
    gzip.c:1487:[eva:garbled-mix:assigns] warning: The specification of function strrchr
    has generated a garbled mix of addresses for assigns clause \result.
    ......@@ -40,10 +9,63 @@ gzip.c:1503:[eva:garbled-mix:assigns] warning: The specification of function str
    has generated a garbled mix of addresses for assigns clause \result.
    gzip.c:817:[eva:locals-escaping] warning: locals {attr} escaping the scope of zip through file_type
    [eva:garbled-mix:summary] warning: Origins of garbled mix generated during analysis:
    inflate.c:446: imprecise merge of addresses
    (read 391618 times, propagated 113144 times)
    garbled mix of &{d_buf; window; prev; ll; pt_table;
    __malloc_w_huft_build_l403;
    __malloc_w_huft_build_l403_0;
    __malloc_w_huft_build_l403_1;
    __malloc_w_huft_build_l403_2;
    __malloc_w_huft_build_l403_3;
    __malloc_w_huft_build_l403_4;
    __malloc_w_huft_build_l403_5;
    __malloc_w_huft_build_l403_6;
    __malloc_w_huft_build_l403_7;
    __malloc_w_huft_build_l403_8;
    __malloc_w_huft_build_l403_9;
    __malloc_w_huft_build_l403_10;
    __malloc_w_huft_build_l403_11;
    __malloc_w_huft_build_l403_12;
    __malloc_w_huft_build_l403_13}
    util.c:186: assigns clause on addresses
    (read 1735 times, propagated 823 times)
    garbled mix of &{ifname; ofname; argv0}
    (read 1817 times, propagated 835 times)
    garbled mix of &{argv0; ifname; ofname}
    inflate.c:446: misaligned read of addresses
    (read 640 times, propagated 316 times)
    garbled mix of &{__malloc_w_huft_build_l403;
    __malloc_w_huft_build_l403_2;
    __malloc_w_huft_build_l403_4;
    __malloc_w_huft_build_l403_7;
    __malloc_w_huft_build_l403_9;
    __malloc_w_huft_build_l403_12}
    inflate.c:382: imprecise merge of addresses
    (read 618 times, propagated 618 times)
    garbled mix of &{__malloc_w_huft_build_l403;
    __malloc_w_huft_build_l403_0;
    __malloc_w_huft_build_l403_1;
    __malloc_w_huft_build_l403_2;
    __malloc_w_huft_build_l403_3;
    __malloc_w_huft_build_l403_4;
    __malloc_w_huft_build_l403_5;
    __malloc_w_huft_build_l403_6;
    __malloc_w_huft_build_l403_7;
    __malloc_w_huft_build_l403_8;
    __malloc_w_huft_build_l403_9;
    __malloc_w_huft_build_l403_10;
    __malloc_w_huft_build_l403_11;
    __malloc_w_huft_build_l403_12;
    __malloc_w_huft_build_l403_13}
    inflate.c:444: imprecise merge of addresses
    (read 574 times, propagated 574 times)
    garbled mix of &{__malloc_w_huft_build_l403_0;
    __malloc_w_huft_build_l403_5;
    __malloc_w_huft_build_l403_10}
    inflate.c:445: imprecise merge of addresses
    (read 492 times, propagated 492 times)
    garbled mix of &{__malloc_w_huft_build_l403_1;
    __malloc_w_huft_build_l403_6;
    __malloc_w_huft_build_l403_11}
    gzip.c:1487: assigns clause on addresses
    (read 108 times, propagated 36 times) garbled mix of &{ofname}
    (read 216 times, propagated 72 times) garbled mix of &{ofname}
    gzip.c:1503: assigns clause on addresses
    (read 30 times, propagated 6 times) garbled mix of &{ofname}
    (read 60 times, propagated 12 times) garbled mix of &{ofname}
    gzip124/.frama-c/gzip124.parse/framac.ast
    + 6530
    − 6496
    View file @ 481d0c58
    This diff is collapsed.
    gzip124/.frama-c/gzip124.parse/warnings.log
    + 3
    − 3
    View file @ 481d0c58
    getopt.c:362:[kernel:typing:no-proto] warning: Calling function getenv that is declared without prototype.
    Its formals will be inferred from actual arguments
    gzip.c:448:[kernel:typing:incompatible-types-call] warning: implicit conversion between incompatible function types:
    void (*)(void)
    and
    ......@@ -10,11 +12,9 @@ gzip.c:457:[kernel:typing:incompatible-types-call] warning: implicit conversion
    void (*)(void)
    and
    void (*)(int )
    getopt.c:362:[kernel:typing:no-proto] warning: Calling function getenv that is declared without prototype.
    Its formals will be inferred from actual arguments
    gzip.c:1207:[variadic:typing] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
    gzip.c:1348:[variadic:typing] warning: Incorrect type for argument 2. The argument will be cast from long to unsigned long.
    gzip.c:1348:[variadic:typing] warning: Incorrect type for argument 3. The argument will be cast from long to unsigned long.
    unlzw.c:218:[variadic:typing] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
    unzip.c:134:[variadic:typing] warning: Incorrect type for argument 3. The argument will be cast from ulg to long.
    unzip.c:134:[variadic:typing] warning: Incorrect type for argument 4. The argument will be cast from unsigned long to long.
    unlzw.c:218:[variadic:typing] warning: Incorrect type for argument 5. The argument will be cast from int to unsigned int.
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment