2021-02-24 19:09 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000801Frama-CPlug-in > slicingpublic2011-10-10 14:14
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000801: r12951, slicing is slow
DescriptionNot sure whether this is a real issue and how much is can be changed, but slicing is very slow with this command and program:


i=s.20000836.1.c ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms $i -cpp-command "gcc -m32 -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.c -kernel-debug 1

The -kernel-debug 1 is to get a backtrace when pressing ctrl-C:

[from] Computing for function safe_rshift_func_int16_t_s_u
/home/cuoq/csmith-2.0.0/runtime/safe_math.h:265:[from] Non terminating function (no dependencies)
[from] Done for function safe_rshift_func_int16_t_s_u
^CFatal error: exception Sys.Break
Raised at file "sys.ml", line 79, characters 52-57
Called from file "hashtbl.ml", line 62, characters 6-29
Called from file "cil/src/ext/dataflow.ml", line 450, characters 32-52
Called from file "cil/src/ext/dataflow.ml", line 435, characters 32-35
Called from file "queue.ml", line 134, characters 6-20
Called from file "cil/src/ext/dataflow.ml", line 435, characters 8-54
Called from file "cil/src/ext/dataflow.ml", line 450, characters 14-131
Called from file "cil/src/ext/dataflow.ml", line 495, characters 16-43
Called from file "cil/src/ext/dataflow.ml", line 500, characters 9-22
Called from file "src/pdg/build.ml", line 1114, characters 10-33
Called from file "src/pdg/build.ml", line 1141, characters 14-34
Called from file "src/project/state_builder.ml", line 634, characters 17-22
Called from file "src/slicing/slicingMacros.ml", line 151, characters 46-60
Called from file "src/slicing/fct_slice.ml", line 756, characters 23-50
Called from file "src/slicing/fct_slice.ml", line 1116, characters 46-73
Called from file "src/slicing/fct_slice.ml", line 1161, characters 12-52
Called from file "src/slicing/slicingProject.ml", line 329, characters 12-52
Called from file "src/slicing/slicingProject.ml", line 371, characters 16-48
Called from file "src/slicing/slicingProject.ml", line 402, characters 26-45
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 403, characters 10-27
Called from file "src/slicing/slicingProject.ml", line 411, characters 10-27
Called from file "src/slicing/register.ml", line 465, characters 10-44
Called from file "src/slicing/register.ml", line 1161, characters 4-50
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Re-raised at file "src/kernel/cmdline.ml", line 214, characters 7-10
Called from file "src/kernel/boot.ml", line 65, characters 2-330
TagsNo tags attached.
Attached Files
  • c file icon s.20000836.1.c (28,931 bytes) 2011-04-20 11:34 -
    /*
     * This is a RANDOMLY GENERATED PROGRAM.
     *
     * Generator: csmith 2.0.0
     * svn version: exported
     * Options:   --max-array-dim 1 --max-funcs 1 --max-struct-fields 2 --no-pointers --no-volatiles --no-argc
     * Seed:      3822969836
     */
    
    #include "csmith.h"
    
    
    long __undefined;
    
    /* --- Struct/Union Declarations --- */
    struct S0 {
       int64_t  f0;
    };
    
    struct S2 {
       int8_t  f0;
    };
    
    struct S3 {
       struct S0  f0;
       int16_t  f1;
    };
    
    /* --- GLOBAL VARIABLES --- */
    int32_t g_3[1] = {6L};
    int32_t g_7 = 0xA927213EL;
    int64_t g_39 = 0xD8EB7BFBL;
    struct S0 g_45 = {0xE702B68169B2B293LL};
    int64_t g_105[8] = {1L, 1L, 0xE2787FF9L, (-6L), 0x026DF2D4L, (-6L), 0xE2787FF9L, 1L};
    uint32_t g_144 = 0x0CEF9D81L;
    struct S2 g_154 = {0x73L};
    int16_t g_188 = 8L;
    struct S3 g_207[1] = {{{-4L},1L}};
    uint64_t g_252[2] = {0xB04EDA8FA795F43DLL, 0xB04EDA8FA795F43DLL};
    int64_t g_253 = 0x4DDBDFA936F0B847LL;
    uint16_t g_408 = 0xDD93L;
    
    
    /* --- FORWARD DECLARATIONS --- */
    struct S2  func_1(void);
    
    
    /* --- FUNCTIONS --- */
    /* ------------------------------------------ */
    /* 
     * reads : g_3 g_7 g_45.f0 g_39 g_45 g_105 g_154.f0 g_144 g_188 g_207 g_154 g_252 g_253 g_408
     * writes: g_3 g_7 g_39 g_45 g_105 g_144 g_154 g_207
     */
    struct S2  func_1(void)
    { /* block id: 0 */
        uint64_t l_2[7] = {18446744073709551615U, 0x4822B16580849F84LL, 18446744073709551608U, 0x4822B16580849F84LL, 18446744073709551615U, 18446744073709551611U, 18446744073709551615U};
        struct S0 l_53 = {-1L};
        int64_t l_60[8];
        int32_t l_61 = 0x573153EDL;
        int64_t l_155[6];
        struct S2 l_268[1] = {{0xCBL}};
        uint64_t l_332 = 18446744073709551615U;
        uint32_t l_368 = 1U;
        int8_t l_394 = 1L;
        const uint32_t l_409 = 0x6E722CEAL;
        int i;
        for (i = 0; i < 8; i++)
            l_60[i] = 0xA6F2DB44L;
        for (i = 0; i < 6; i++)
            l_155[i] = 0x01D75DE8CEC1B3EELL;
        for (g_3[0] = 0; g_3[0] < 7; g_3[0] += 1)
        { /* block id: 1 */
            uint64_t l_4 = 0xEDB5CABFC3938DD4LL;
            struct S2 l_86 = {9L};
            uint64_t l_132 = 3U;
            struct S3 l_190[8] = {{{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}, {{-6L},-4L}};
            struct S2 l_208 = {-6L};
            int64_t l_215 = 0L;
            int32_t l_218 = (-2L);
            const struct S2 l_219 = {-3L};
            int8_t l_251 = 0x7CL;
            int32_t l_267 = (-1L);
            int16_t l_288 = 4L;
            int64_t l_410 = 4L;
            int i;
            if (l_4)
            { /* block id: 2 */
                uint8_t l_10 = 249U;
                int64_t l_40 = 0xCB0C7B249E3C8D3FLL;
                struct S2 l_42 = {0x41L};
                struct S0 l_44[2] = {{0xF33BC6C2DB602708LL}, {0xF33BC6C2DB602708LL}};
                uint32_t l_93 = 0xF90230FDL;
                int16_t l_149[10] = {(-1L), 0x6D51L, 0x7970L, 0x6D51L, (-1L), 0x6D51L, 0x7970L, 0x6D51L, (-1L), 0x6D51L};
                struct S2 l_153 = {0x81L};
                int i;
    lbl_177:
                if (g_3[0])
                { /* block id: 3 */
                    int16_t l_32 = 0L;
                    int32_t l_41 = 0L;
                    int i;
                    for (l_4 = (-20); (l_4 < 13); l_4 = safe_add_func_uint64_t_u_u(l_4, 1))
                    { /* block id: 6 */
                        uint64_t l_15 = 18446744073709551609U;
                        for (g_7 = (-13); (g_7 <= (-12)); g_7 = safe_add_func_int64_t_s_s(g_7, 1))
                        { /* block id: 9 */
                            int64_t l_20 = 0x7AD53A38L;
                            uint64_t l_29 = 0x63E91CB6L;
                            g_3[0] = l_10;
                            g_3[0] = (safe_lshift_func_uint16_t_u_u((safe_rshift_func_int8_t_s_s((((g_3[0] || l_15) == (safe_add_func_int32_t_s_s((safe_mul_func_int8_t_s_s(g_7, l_2[(uint32_t)(g_3[0]) % 7])), l_20))) && ((0x4EDC0223L == 0xC995F762L) ^ (0x422D5FBA2522ABF7LL | (safe_add_func_uint8_t_u_u(l_20, g_7))))), (safe_sub_func_int16_t_s_s(((safe_add_func_int8_t_s_s((safe_rshift_func_uint16_t_u_s(l_29, 6)), (l_2[(uint32_t)(g_3[0]) % 7] < l_2[(uint32_t)(g_3[0]) % 7]))) > ((safe_lshift_func_int16_t_s_s(g_7, l_32)) >= (safe_add_func_int8_t_s_s(g_7, l_2[(uint32_t)(g_3[0]) % 7])))), (l_10 | l_2[(uint32_t)(g_3[0]) % 7]))))), 6));
                            g_39 |= (g_7 | (((safe_lshift_func_uint16_t_u_s(l_4, 12)) ^ l_15) > g_3[0]));
                        }
                    }
                    l_41 = (l_2[(uint32_t)(g_3[0]) % 7] | l_40);
                    for (l_4 = 0; l_4 < 1; l_4 += 1)
                    { /* block id: 16 */
                        struct S2 l_43 = {0xB3L};
                        int i;
                        l_43 = l_42;
                        g_45 = l_44[0];
                        for (g_39 = 0; g_39 < 2; g_39 += 1)
                        { /* block id: 19 */
                            struct S0 l_52 = {0xA6287676E3B61EA5LL};
                            g_3[0] = (safe_mul_func_uint16_t_u_u(((safe_mod_func_uint32_t_u_u((0x4AL < l_44[0].f0), (g_45.f0 ^ 0L))) & (-9L)), 0xFA2FL));
                            l_53 = l_52;
                            l_61 ^= (g_39 && (((safe_add_func_uint32_t_u_u(((safe_mul_func_uint16_t_u_u(l_2[3], g_39)) && l_4), g_39)) <= (safe_div_func_int8_t_s_s(g_3[0], l_41))) < l_60[4]));
                            g_3[0] = g_45.f0;
                        }
                    }
                }
                else
                { /* block id: 26 */
                    int64_t l_79 = 1L;
                    int16_t l_114 = (-7L);
                    int32_t l_117 = 0x40C93662L;
                    int i;
                    for (l_10 = 9; (l_10 < 53); l_10 = safe_add_func_int32_t_s_s(l_10, 2))
                    { /* block id: 29 */
                        uint16_t l_80 = 65532U;
                        int32_t l_81 = 0L;
                        for (g_45.f0 = 0; g_45.f0 < 8; g_45.f0 += 1)
                        {
                            l_60[g_45.f0] = (-1L);
                        }
                        g_3[0] = (safe_rshift_func_uint8_t_u_s((safe_div_func_int16_t_s_s((safe_mod_func_uint16_t_u_u(0U, l_2[(uint32_t)(g_3[0]) % 7])), l_53.f0)), 7));
                        g_7 = (g_3[0] > (((safe_unary_minus_func_int64_t_s((0x01C9AC71L == (safe_rshift_func_int16_t_s_s(l_44[0].f0, l_2[(uint32_t)(g_3[0]) % 7]))))) < l_2[(uint32_t)(g_3[0]) % 7]) <= (((safe_mul_func_int8_t_s_s(g_3[0], (g_7 != g_3[0]))) != (safe_mul_func_uint16_t_u_u((safe_sub_func_uint32_t_u_u(l_2[(uint32_t)(g_3[0]) % 7], g_3[0])), (g_45.f0 ^ l_2[(uint32_t)(g_3[0]) % 7])))) & (l_79 >= ((g_45.f0 > l_80) || (l_79 && l_42.f0))))));
                        l_81 &= g_7;
                    }
                    for (l_79 = 0; l_79 < 1; l_79 += 1)
                    { /* block id: 35 */
                        int64_t l_104 = 0x820E1BCBL;
                        int32_t l_131[5];
                        int i;
                        for (i = 0; i < 5; i++)
                            l_131[i] = 1L;
                        if ((safe_lshift_func_uint16_t_u_u((safe_mod_func_uint32_t_u_u(g_3[0], (0xA9B9L & g_3[0]))), g_3[(uint64_t)(l_79) % 1])))
                        { /* block id: 36 */
                            l_86 = l_42;
                            if (l_53.f0)
                                goto lbl_222;
                        }
                        else
                        { /* block id: 38 */
                            l_61 = ((safe_add_func_int32_t_s_s(g_7, g_3[(uint64_t)(l_79) % 1])) ^ (g_45.f0 > g_3[(uint64_t)(l_79) % 1]));
                            g_105[5] ^= (safe_add_func_int16_t_s_s((g_3[0] >= (safe_add_func_uint32_t_u_u(g_3[0], l_93))), (safe_lshift_func_uint8_t_u_u((((safe_add_func_uint64_t_u_u((safe_mul_func_uint8_t_u_u(g_3[0], g_3[0])), (g_39 != g_3[(uint64_t)(l_79) % 1]))) != g_39) > (((l_86.f0 && g_3[0]) && (l_2[5] || l_44[0].f0)) | (safe_div_func_uint16_t_u_u((safe_div_func_uint16_t_u_u(g_39, l_104)), g_45.f0)))), g_7))));
                        }
                        if ((safe_rshift_func_int8_t_s_u(0x81L, 6)))
                        { /* block id: 42 */
                            uint32_t l_128 = 1U;
                            l_53 = g_45;
                            l_117 &= ((g_105[7] != (((safe_add_func_uint64_t_u_u(0xED4C97A6105BDF17LL, (safe_mod_func_uint8_t_u_u(g_3[0], g_105[7])))) ^ l_104) >= (+((safe_mod_func_int32_t_s_s(g_3[(uint64_t)(l_79) % 1], l_114)) ^ (safe_rshift_func_uint16_t_u_s(g_3[(uint64_t)(l_79) % 1], 12)))))) & g_3[(uint32_t)((l_79 + 1)) % 1]);
                            l_131[3] |= (safe_mod_func_int16_t_s_s((safe_mod_func_int32_t_s_s(((safe_add_func_uint8_t_u_u(251U, (+(safe_lshift_func_uint16_t_u_u(l_86.f0, g_105[5]))))) | ((safe_lshift_func_int8_t_s_s(l_61, l_128)) > (l_128 || (g_105[1] < g_3[(uint64_t)(l_79) % 1])))), ((safe_div_func_uint16_t_u_u(g_3[0], ((l_104 >= l_86.f0) || l_86.f0))) && g_7))), (g_3[(uint64_t)(l_79) % 1] || g_105[5])));
                        }
                        else
                        { /* block id: 46 */
                            int16_t l_141 = 0xC346L;
                            l_117 &= l_132;
                            g_144 &= (0x92015BDFL ^ ((g_3[(uint64_t)(l_79) % 1] >= (safe_sub_func_int16_t_s_s((0L && g_3[(uint32_t)((l_79 + 1)) % 1]), (safe_sub_func_uint16_t_u_u((l_53.f0 | l_4), g_7))))) & (safe_mod_func_int32_t_s_s((l_131[0] | ((safe_add_func_uint32_t_u_u(l_2[5], l_44[0].f0)) == (l_141 && g_3[(uint64_t)(l_79) % 1]))), (safe_rshift_func_uint8_t_u_u(g_3[0], g_3[(uint64_t)(l_79) % 1]))))));
                        }
                    }
                    for (l_10 = (-15); (l_10 > 32); l_10 = safe_add_func_int64_t_s_s(l_10, 1))
                    { /* block id: 53 */
                        for (l_117 = 0; (l_117 == (-17)); l_117 = safe_sub_func_int32_t_s_s(l_117, 1))
                        { /* block id: 56 */
                            int64_t l_152 = 0x685BE090L;
                            g_45 = g_45;
                            l_152 &= (l_149[3] <= (safe_sub_func_uint64_t_u_u(0U, 0x12332C83D21EB911LL)));
                            g_154 = l_153;
                            g_7 = l_155[3];
                        }
                        for (g_39 = 0; (g_39 != 21); g_39 = safe_add_func_uint64_t_u_u(g_39, 1))
                        { /* block id: 64 */
                            struct S2 l_158[10] = {{0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}, {0xD2L}};
                            int i;
                            return l_158[9];
                        }
                    }
                }
    lbl_222:
                if ((((l_44[0].f0 | ((safe_lshift_func_uint16_t_u_s(g_154.f0, 15)) > (0xD60A08B2L && g_39))) || ((safe_mul_func_uint16_t_u_u((safe_sub_func_int8_t_s_s(0L, (l_53.f0 <= l_93))), (1L ^ l_86.f0))) >= (l_60[4] & g_105[5]))) != g_144))
                { /* block id: 69 */
                    int64_t l_182[9] = {0x02CAF5ADL, 0L, 0x02CAF5ADL, 0L, 0x02CAF5ADL, 0L, 0x02CAF5ADL, 0L, 0x02CAF5ADL};
                    int32_t l_187[8] = {0L, (-2L), 0L, (-2L), 0L, (-2L), 0L, (-2L)};
                    struct S2 l_209 = {-3L};
                    int i;
                    if (((l_40 == (((g_7 & (g_144 && g_105[0])) || (~0U)) < (safe_mod_func_uint8_t_u_u((safe_mul_func_int16_t_s_s((+g_45.f0), g_105[5])), g_154.f0)))) && (safe_rshift_func_uint16_t_u_s((safe_sub_func_uint32_t_u_u((l_2[(uint32_t)(g_3[0]) % 7] < ((g_39 & l_10) >= l_2[(uint32_t)(g_3[0]) % 7])), (safe_lshift_func_uint16_t_u_s(((safe_div_func_int64_t_s_s(g_45.f0, l_2[(uint32_t)(g_3[0]) % 7])) & g_105[5]), l_2[(uint32_t)(g_3[0]) % 7])))), g_105[5]))))
                    { /* block id: 70 */
                        if (l_132)
                            goto lbl_177;
                    }
                    else
                    { /* block id: 72 */
                        int i;
                        if (((safe_sub_func_int16_t_s_s(0x4A51L, ((safe_mod_func_uint8_t_u_u(247U, (l_2[(uint32_t)(g_3[0]) % 7] && (l_182[8] >= g_154.f0)))) ^ (safe_add_func_int64_t_s_s((safe_sub_func_int32_t_s_s((-1L), (l_86.f0 & g_7))), 1L))))) >= l_182[8]))
                        { /* block id: 73 */
                            struct S3 l_189 = {{0xFF799FEAB6E62887LL},0L};
                            l_187[6] = l_2[(uint32_t)(g_3[0]) % 7];
                            g_3[0] ^= g_188;
                            l_190[3] = l_189;
                            g_7 = ((safe_mod_func_int32_t_s_s(((((g_45.f0 & g_3[0]) < (safe_lshift_func_uint16_t_u_u(l_2[(uint32_t)(g_3[0]) % 7], 4))) <= ((l_2[(uint32_t)(g_3[0]) % 7] >= l_86.f0) != (g_7 == l_2[(uint32_t)(g_3[0]) % 7]))) == l_189.f0.f0), (safe_div_func_int32_t_s_s(l_182[5], (safe_mod_func_uint16_t_u_u(((g_105[4] ^ l_182[8]) || 2L), g_3[0])))))) > ((((safe_add_func_int16_t_s_s((g_105[0] > l_182[8]), g_105[5])) > (safe_sub_func_uint32_t_u_u((g_3[0] || g_7), l_189.f1))) != 4L) <= l_2[(uint32_t)(g_3[0]) % 7]));
                        }
                        else
                        { /* block id: 78 */
                            g_7 ^= (((safe_lshift_func_int8_t_s_u(0x08L, 7)) < (safe_unary_minus_func_uint32_t_u(l_2[(uint32_t)(g_3[0]) % 7]))) <= (safe_unary_minus_func_uint16_t_u(0U)));
                            l_190[3] = g_207[0];
                            l_209 = l_208;
                            g_7 = (safe_mod_func_uint8_t_u_u(((0L > (safe_lshift_func_uint16_t_u_u(((safe_unary_minus_func_uint32_t_u(l_215)) != (safe_rshift_func_int16_t_s_u(g_207[0].f1, 12))), ((l_2[(uint32_t)(g_3[0]) % 7] <= g_105[5]) & l_42.f0)))) <= g_154.f0), (+l_182[8])));
                        }
                        for (l_61 = 0; l_61 < 8; l_61 += 6)
                        { /* block id: 84 */
                            g_207[0] = g_207[0];
                            l_218 = 0x93AD4E58L;
                            return g_154;
                        }
                        if (g_39)
                        { /* block id: 89 */
                            int16_t l_220[1];
                            int i;
                            for (i = 0; i < 1; i++)
                                l_220[i] = 0L;
                            l_208 = g_154;
                            g_154 = l_219;
                            l_220[0] = l_155[3];
                            return l_219;
                        }
                        else
                        { /* block id: 94 */
                            struct S2 l_221[7] = {{2L}, {2L}, {2L}, {2L}, {2L}, {2L}, {2L}};
                            int i;
                            l_208 = l_221[1];
                            l_208 = g_154;
                            g_3[0] = (-1L);
                        }
                        g_3[0] &= 0x36AD9C87L;
                    }
                    g_207[0] = g_207[0];
                    g_3[0] &= (!0x40D45DD2L);
                }
                else
                { /* block id: 103 */
                    g_7 = 6L;
                }
                if (g_207[0].f1)
                    break;
            }
            else
            { /* block id: 108 */
    lbl_246:
                if ((+l_2[(uint32_t)(g_3[0]) % 7]))
                { /* block id: 109 */
    lbl_308:
                    g_7 |= ((safe_lshift_func_uint16_t_u_s(g_3[0], 13)) > ((safe_sub_func_int32_t_s_s(l_60[1], (0U <= (g_188 ^ g_105[5])))) != (g_188 != g_188)));
                }
                else
                { /* block id: 111 */
                    int32_t l_243[6] = {1L, 1L, 0xC0A8395AL, 1L, 1L, 0xC0A8395AL};
                    int i;
                    l_243[5] = ((safe_lshift_func_uint16_t_u_s((safe_lshift_func_int8_t_s_u((safe_rshift_func_uint16_t_u_u(l_155[3], 9)), (l_2[(uint32_t)(g_3[0]) % 7] & (~(safe_mod_func_int8_t_s_s(g_188, g_105[4])))))), (safe_add_func_int16_t_s_s(((safe_add_func_int64_t_s_s((safe_rshift_func_uint16_t_u_s(g_39, g_144)), (safe_mod_func_uint32_t_u_u(l_60[4], l_243[5])))) ^ (0x70L <= 0xC6L)), (safe_rshift_func_uint8_t_u_s(l_2[(uint32_t)((g_3[0] + 3)) % 7], g_105[5])))))) <= l_2[(uint32_t)(g_3[0]) % 7]);
                }
                if (g_39)
                    continue;
                if (l_61)
                    goto lbl_246;
                g_207[0].f0 = g_45;
            }
            if (l_2[(uint32_t)(g_3[0]) % 7])
            { /* block id: 118 */
                uint8_t l_247[8] = {0x7BL, 0x8BL, 255U, 255U, 0x8BL, 0x7BL, 0x8BL, 255U};
                int i;
                l_218 = l_247[5];
            }
            else
            { /* block id: 120 */
                struct S0 l_271 = {0L};
                int i;
                for (l_218 = 0; l_218 < 8; l_218 += 1)
                { /* block id: 121 */
                    uint64_t l_250 = 0xBDFE2882719CDBA8LL;
                    int32_t l_256 = (-2L);
                    l_256 |= (safe_add_func_uint64_t_u_u((l_250 ^ g_105[(uint32_t)(l_218) % 8]), (l_251 == ((g_252[0] <= (0x7FL && (l_2[2] != g_253))) | ((0x2BF4L > l_250) && (safe_lshift_func_int8_t_s_u(g_144, 0)))))));
                    g_7 = (safe_sub_func_uint16_t_u_u(g_3[0], (safe_mul_func_int16_t_s_s(l_60[4], (safe_div_func_int32_t_s_s(0xF885BBE7L, l_250))))));
                }
                for (l_215 = 0; l_215 < 1; l_215 += 1)
                { /* block id: 125 */
                    int64_t l_269 = 0L;
                    l_267 &= (safe_mul_func_uint16_t_u_u((safe_sub_func_int16_t_s_s((l_190[3].f0.f0 && g_3[(uint64_t)(l_215) % 1]), g_105[(uint32_t)(l_218) % 8])), (g_154.f0 >= g_3[(uint64_t)(l_215) % 1])));
                    if (g_3[(uint64_t)(l_215) % 1])
                    { /* block id: 127 */
                        int i;
                        for (l_208.f0 = 0; l_208.f0 < 1; l_208.f0 += 1)
                        { /* block id: 128 */
                            return l_268[0];
                        }
                        if (l_269)
                        { /* block id: 131 */
                            struct S0 l_270 = {0x5FEBA5A16B7DE68CLL};
                            g_7 = g_39;
                            g_154 = l_268[0];
                            l_271 = l_270;
                            g_3[0] = (g_3[0] > (safe_lshift_func_int16_t_s_u(g_3[0], (((g_252[0] ^ 0x92CFC96928D4B40CLL) ^ g_45.f0) <= g_3[(uint8_t)(l_208.f0) % 1]))));
                        }
                        else
                        { /* block id: 136 */
                            return g_154;
                        }
                    }
                    else
                    { /* block id: 139 */
                        int i;
                        for (l_271.f0 = 21; (l_271.f0 < (-23)); l_271.f0 = safe_sub_func_uint64_t_u_u(l_271.f0, 1))
                        { /* block id: 142 */
                            const int64_t l_276 = (-2L);
                            struct S2 l_277 = {-1L};
                            g_7 = l_276;
                            return l_277;
                        }
                        for (l_208.f0 = 4; l_208.f0 < 8; l_208.f0 += 8)
                        { /* block id: 146 */
                            g_3[0] = 0x0EBDD82FL;
                        }
                        if (g_154.f0)
                            continue;
                    }
                }
            }
            if (g_105[3])
            { /* block id: 153 */
                int32_t l_280 = 0xAFA11A28L;
                if (l_86.f0)
                    break;
                for (l_208.f0 = 5; (l_208.f0 >= (-24)); l_208.f0 = safe_sub_func_uint64_t_u_u(l_208.f0, 2))
                { /* block id: 157 */
                    l_280 = 0xF4403A96L;
                }
            }
            else
            { /* block id: 160 */
                int32_t l_293 = 0x22EB11DCL;
                struct S0 l_329 = {1L};
                struct S3 l_335 = {{0L},0L};
                const uint64_t l_344[2] = {0x80E5CDF09FE0713FLL, 0x80E5CDF09FE0713FLL};
                struct S2 l_358 = {0x83L};
                uint32_t l_388 = 0x458A64CCL;
                int i;
                for (l_251 = 0; (l_251 < (-28)); l_251 = safe_sub_func_uint32_t_u_u(l_251, 1))
                { /* block id: 163 */
                    int16_t l_285 = 0x5CD4L;
                    int32_t l_325 = 0xD68D3CEBL;
                    struct S0 l_328 = {0x55E09F5BEA1ABC11LL};
                    const uint16_t l_331 = 65530U;
                    if (((safe_div_func_uint64_t_u_u(l_285, (safe_div_func_uint8_t_u_u((!(l_288 == (g_7 >= l_2[(uint32_t)(g_3[0]) % 7]))), (safe_lshift_func_int16_t_s_s(((safe_lshift_func_uint16_t_u_u(l_132, l_293)) ^ (g_3[0] >= l_288)), l_251)))))) > (+(g_105[5] | g_154.f0))))
                    { /* block id: 164 */
                        int32_t l_300 = (-3L);
                        l_267 = 0xF798E078L;
                        for (g_7 = 0; g_7 < 7; g_7 += 1)
                        {
                            l_2[g_7] = 0x3E9DAC5E5D6FC0C6LL;
                        }
                        g_3[0] = (safe_lshift_func_uint16_t_u_u((safe_sub_func_int64_t_s_s((safe_mod_func_int32_t_s_s(((g_154.f0 > 18446744073709551615U) >= ((l_53.f0 != l_300) && (g_188 && l_2[(uint32_t)(g_3[0]) % 7]))), g_3[0])), (safe_rshift_func_int16_t_s_s(l_300, g_252[0])))), g_188));
                        for (g_45.f0 = 0; (g_45.f0 != (-29)); g_45.f0 = safe_sub_func_int64_t_s_s(g_45.f0, 1))
                        { /* block id: 170 */
                            int16_t l_307[6];
                            int i;
                            for (i = 0; i < 6; i++)
                                l_307[i] = (-2L);
                            l_293 = (safe_mod_func_uint32_t_u_u(l_307[4], l_307[4]));
                            return l_268[0];
                        }
                        if (l_208.f0)
                            goto lbl_330;
                    }
                    else
                    { /* block id: 174 */
                        int i;
                        for (l_4 = 0; l_4 < 1; l_4 += 1)
                        { /* block id: 175 */
                            g_207[0].f0 = g_207[0].f0;
                        }
                    }
                    if (l_219.f0)
                        goto lbl_308;
                    if (l_285)
                        continue;
                    if (((safe_div_func_int64_t_s_s((safe_div_func_int8_t_s_s((safe_add_func_uint64_t_u_u(0xDC7AD04161D741B9LL, l_155[3])), g_45.f0)), l_2[(uint32_t)(g_3[0]) % 7])) | (safe_mul_func_uint16_t_u_u(l_218, (safe_sub_func_int16_t_s_s(l_2[(uint32_t)((g_3[0] + 1)) % 7], l_251))))))
                    { /* block id: 181 */
                        if ((g_105[5] && (safe_rshift_func_uint16_t_u_u((safe_rshift_func_int16_t_s_s((l_190[3].f0.f0 > 3L), 1)), 7))))
                        { /* block id: 182 */
                            g_3[0] = g_188;
                        }
                        else
                        { /* block id: 184 */
                            l_325 = (safe_rshift_func_int8_t_s_s(l_2[(uint32_t)(g_3[0]) % 7], 7));
                        }
    lbl_330:
                        for (l_86.f0 = (-24); (l_86.f0 != (-10)); l_86.f0 = safe_add_func_int16_t_s_s(l_86.f0, 1))
                        { /* block id: 189 */
                            l_329 = l_328;
                        }
                        l_332 = l_331;
                        for (l_328.f0 = 21; (l_328.f0 < 2); l_328.f0 = safe_sub_func_int32_t_s_s(l_328.f0, 1))
                        { /* block id: 196 */
                            return g_154;
                        }
                    }
                    else
                    { /* block id: 199 */
                        int16_t l_345 = 9L;
                        l_335 = g_207[0];
                        l_345 &= (safe_add_func_int8_t_s_s(((safe_mod_func_uint32_t_u_u((l_268[0].f0 ^ l_325), (safe_rshift_func_uint16_t_u_s((safe_mul_func_int16_t_s_s(l_344[0], (g_252[1] >= g_105[1]))), (g_7 || 0xD9L))))) | (0x17DDL != g_207[0].f0.f0)), g_3[0]));
                        l_325 ^= (l_345 >= (safe_rshift_func_int8_t_s_u(((safe_rshift_func_int8_t_s_u(l_2[(uint32_t)((g_3[0] + 3)) % 7], 7)) == (((safe_div_func_uint16_t_u_u(l_218, l_61)) >= (l_285 <= l_2[(uint32_t)(g_3[0]) % 7])) == (safe_add_func_int8_t_s_s((safe_lshift_func_int16_t_s_s(l_335.f0.f0, 5)), (l_2[0] & g_252[0]))))), g_188)));
                        g_7 = l_267;
                    }
                }
                for (g_39 = 0; (g_39 == (-16)); g_39 = safe_sub_func_uint64_t_u_u(g_39, 6))
                { /* block id: 208 */
                    struct S2 l_379[9] = {{6L}, {6L}, {6L}, {6L}, {6L}, {6L}, {6L}, {6L}, {6L}};
                    struct S3 l_380 = {{-1L},0L};
                    int i;
                    l_358 = g_154;
                    for (g_45.f0 = 0; g_45.f0 < 1; g_45.f0 += 1)
                    { /* block id: 210 */
                        uint32_t l_359 = 4U;
                        uint8_t l_393[4];
                        int16_t l_401[6] = {9L, 9L, 0x0F5EL, 9L, 9L, 0x0F5EL};
                        int i;
                        for (i = 0; i < 4; i++)
                            l_393[i] = 0x25L;
                        if (((l_359 > (safe_sub_func_uint32_t_u_u(((safe_rshift_func_uint16_t_u_s((safe_mul_func_uint8_t_u_u(l_344[1], g_39)), g_3[(uint64_t)(g_45.f0) % 1])) < g_144), (safe_mod_func_uint16_t_u_u((l_368 ^ (g_207[0].f0.f0 > g_188)), (safe_sub_func_uint64_t_u_u((l_368 != g_252[1]), 0xA8C5B16D34A9AF0FLL))))))) && (((g_39 != (g_207[0].f0.f0 & (l_329.f0 <= g_144))) ^ ((safe_mod_func_uint64_t_u_u((safe_rshift_func_int16_t_s_u(l_359, 12)), (g_188 ^ l_344[0]))) >= (safe_add_func_uint32_t_u_u((safe_rshift_func_uint16_t_u_u(g_3[(uint64_t)(g_45.f0) % 1], 7)), 1U)))) > l_344[0])))
                        { /* block id: 211 */
                            return l_379[1];
                        }
                        else
                        { /* block id: 213 */
                            uint64_t l_381 = 18446744073709551608U;
                            g_207[0] = l_380;
                            l_381 |= l_379[1].f0;
                            l_267 ^= ((safe_mul_func_int8_t_s_s(g_252[0], 0xA3L)) & (safe_add_func_uint16_t_u_u((safe_mod_func_uint32_t_u_u(((l_388 < (g_188 || g_39)) == l_251), (safe_sub_func_uint16_t_u_u((safe_mod_func_int32_t_s_s((g_207[0].f1 | g_3[(uint64_t)(g_45.f0) % 1]), (l_393[1] | l_394))), g_188)))), (g_3[(uint64_t)(g_45.f0) % 1] >= (safe_mod_func_uint32_t_u_u(((g_207[0].f0.f0 < g_3[(uint64_t)(g_45.f0) % 1]) != g_105[3]), (safe_sub_func_int32_t_s_s((safe_mul_func_int16_t_s_s(l_155[2], l_401[3])), l_380.f0.f0))))))));
                            return g_154;
                        }
                    }
                    for (l_394 = (-29); (l_394 >= 19); l_394 = safe_add_func_uint16_t_u_u(l_394, 1))
                    { /* block id: 222 */
                        l_410 = (safe_lshift_func_uint16_t_u_s(((g_252[1] <= g_154.f0) < ((((g_39 ^ g_252[0]) | 0L) | ((l_2[(uint32_t)(g_3[0]) % 7] != g_45.f0) > (g_3[(uint64_t)(g_45.f0) % 1] < g_408))) <= (l_190[3].f0.f0 >= l_409))), 5));
                        if (l_2[(uint32_t)(g_3[0]) % 7])
                            continue;
                        for (g_154.f0 = 0; (g_154.f0 == (-24)); g_154.f0 = safe_sub_func_uint64_t_u_u(g_154.f0, 7))
                        { /* block id: 227 */
                            uint32_t l_419 = 0xF82F0E3FL;
                            l_293 |= ((safe_mod_func_int8_t_s_s((safe_sub_func_int16_t_s_s(((safe_lshift_func_uint16_t_u_u((l_419 < g_252[0]), (safe_add_func_int16_t_s_s(l_344[1], l_2[(uint32_t)(g_3[0]) % 7])))) == (5L != (l_2[(uint32_t)(g_3[0]) % 7] > g_252[1]))), 9U)), g_408)) || (safe_sub_func_uint8_t_u_u(l_2[(uint32_t)(g_3[0]) % 7], (safe_add_func_uint32_t_u_u((safe_lshift_func_uint16_t_u_s(l_2[(uint32_t)((g_3[0] + 3)) % 7], 1)), 0xD2BCC292L)))));
                            return g_154;
                        }
                    }
                    g_3[(uint64_t)(g_45.f0) % 1] = g_45.f0;
                }
            }
        }
        l_53 = l_53;
        return g_154;
    }
    
    
    
    
    /* ---------------------------------------- */
    int main (void)
    {
        int i;
        int print_hash_value = 0;
        platform_main_begin();
        crc32_gentab();
        func_1();
        for (i = 0; i < 1; i++)
        {
            transparent_crc(g_3[i], "g_3[i]", print_hash_value);
            if (print_hash_value) printf("index = [%d]\n", i);
    
        }
        transparent_crc(g_7, "g_7", print_hash_value);
        transparent_crc(g_39, "g_39", print_hash_value);
        transparent_crc(g_45.f0, "g_45.f0", print_hash_value);
        for (i = 0; i < 8; i++)
        {
            transparent_crc(g_105[i], "g_105[i]", print_hash_value);
            if (print_hash_value) printf("index = [%d]\n", i);
    
        }
        transparent_crc(g_144, "g_144", print_hash_value);
        transparent_crc(g_154.f0, "g_154.f0", print_hash_value);
        transparent_crc(g_188, "g_188", print_hash_value);
        for (i = 0; i < 1; i++)
        {
            transparent_crc(g_207[i].f0.f0, "g_207[i].f0.f0", print_hash_value);
            transparent_crc(g_207[i].f1, "g_207[i].f1", print_hash_value);
            if (print_hash_value) printf("index = [%d]\n", i);
    
        }
        for (i = 0; i < 2; i++)
        {
            transparent_crc(g_252[i], "g_252[i]", print_hash_value);
            if (print_hash_value) printf("index = [%d]\n", i);
    
        }
        transparent_crc(g_253, "g_253", print_hash_value);
        transparent_crc(g_408, "g_408", print_hash_value);
        platform_main_end(crc32_context ^ 0xFFFFFFFFUL);
        return 0;
    }
    
    /************************ statistics *************************
    XXX max struct depth: 2
    breakdown:
       depth: 0, occurrence: 67
       depth: 1, occurrence: 22
       depth: 2, occurrence: 5
    
    XXX max expression depth: 2
    breakdown:
       depth: 0, occurrence: 98
       depth: 1, occurrence: 7
       depth: 2, occurrence: 3
    
    XXX total number of pointers: 0
    
    XXX times a non-volatile is read: 390
    XXX times a non-volatile is write: 94
    XXX times a volatile is read: 0
    XXX    times read thru a pointer: 0
    XXX times a volatile is write: 0
    XXX    times written thru a pointer: 0
    XXX times a volatile is available for access: 0
    XXX percentage of non-volatile access: 100
    
    XXX forward jumps: 2
    XXX backward jumps: 3
    
    XXX stmts: 238
    
    XXX percentage a fresh-made variable is used: 23.1
    XXX percentage an existing variable is used: 76.9
    ********************* end of statistics **********************/
    
    
    c file icon s.20000836.1.c (28,931 bytes) 2011-04-20 11:34 +

-Relationships
+Relationships

-Notes

~0001797

Anne (reporter)

It seems that most of the time is spent building the pdg of [func_1] which is quite big (some of this time is used for the [from] computation, but not that much) :

# -slice-calls Frama_C_show_each
# real 2m41.191s user 2m40.136s sys 0m0.44
# -pdg
# real 2m41.277s user 2m38.952s sys 0m0.785s
# -fct-pdg func_1
# real 2m41.561s user 2m39.799s sys 0m0.315s


(well, I am not sure of how to interpret that since the whole PDG seems to take less time than the PDG of [func_1] but it gives an idea...)

I try to investigate further...

~0001798

Anne (reporter)

I am not sure that there is a problem here : it is just a quite big function with many operations and 34 loops, so it takes time to compute...

~0001820

Anne (reporter)

Can we close this one, Pascal ?
To me, it doesn't seem to be a bug... just a huge function.

~0001830

Anne (reporter)

Would need some profiling on the PDG part. One day...

~0002075

Anne (reporter)

Could you check if it is still long ? I changed nothing but just tried it, and it seems that is is much faster now...

# -slice-calls Frama_C_show_each
# real 0m3.536s user 0m3.364s sys 0m0.070s
+Notes

-Issue History
Date Modified Username Field Change
2011-04-20 11:34 pascal New Issue
2011-04-20 11:34 pascal Status new => assigned
2011-04-20 11:34 pascal Assigned To => Anne
2011-04-20 11:34 pascal File Added: s.20000836.1.c
2011-04-20 14:29 Anne Note Added: 0001797
2011-04-20 14:39 Anne Note Added: 0001798
2011-04-28 14:02 Anne Note Added: 0001820
2011-04-29 09:01 Anne Note Added: 0001830
2011-04-29 09:01 Anne Status assigned => acknowledged
2011-07-29 09:57 Anne Note Added: 0002075
2011-07-29 13:06 pascal Status acknowledged => resolved
2011-07-29 13:06 pascal Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
+Issue History