2021-02-24 18:52 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000807Frama-CPlug-in > slicingpublic2014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000807: sliced program does not terminate (csmith)
Descriptionsame conditions as bug 806.

Compile the original with gcc -m32 -D__FRAMAC -I runtime show_each.c noterm.c (executable terminates) and the sliced program with gcc -m32 show_each.c noterm.s.c
TagsNo tags attached.
Attached Files
  • c file icon noterm.c (7,874 bytes) 2011-04-28 14:49 -
    /*
     * 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:      3444090867
     */
    
    #include "csmith.h"
    
    
    long __undefined;
    
    /* --- Struct/Union Declarations --- */
    struct S0 {
       int16_t  f0;
    };
    
    /* --- GLOBAL VARIABLES --- */
    int32_t g_5 = 0x4543BEB7L;
    struct S0 g_39 = {0x6AE4L};
    int64_t g_62 = 0xA59A03C9L;
    
    
    /* --- FORWARD DECLARATIONS --- */
    uint64_t  func_1(void);
    
    
    /* --- FUNCTIONS --- */
    /* ------------------------------------------ */
    /* 
     * reads : g_5 g_39 g_62
     * writes: g_5 g_39 g_62
     */
    uint64_t  func_1(void)
    { /* block id: 0 */
        uint64_t l_4 = 18446744073709551614U;
        uint32_t l_6 = 0x292C5EB2L;
        int16_t l_9[7] = {(-3L), (-1L), (-3L), (-1L), (-3L), (-1L), (-3L)};
        int32_t l_38 = 1L;
        uint64_t l_79 = 0x4F512441L;
        uint8_t l_108 = 7U;
        uint8_t l_115 = 0xB8L;
        int16_t l_116 = (-1L);
        int i;
        if ((((safe_sub_func_int32_t_s_s(l_4, (g_5 <= ((l_4 != g_5) < (l_6 || l_6))))) || 4294967295U) && (l_6 >= ((((g_5 > l_4) ^ (g_5 < l_4)) & (4U < 4U)) ^ 0x78F1L))))
        { /* block id: 1 */
            int32_t l_74 = 0xB9066996L;
            uint16_t l_112 = 0xFA02L;
            int i;
            for (l_4 = 0; l_4 < 7; l_4 += 1)
            { /* block id: 2 */
                int16_t l_14 = 0x943AL;
                struct S0 l_63[9] = {{0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}, {0x2B18L}};
                int i;
                if ((safe_add_func_int16_t_s_s((safe_add_func_int64_t_s_s(l_14, (safe_mul_func_int8_t_s_s(g_5, ((l_9[((l_4 + 4)) % 7] > g_5) != (g_5 != g_5)))))), (safe_lshift_func_int16_t_s_s(0x018EL, 13)))))
                { /* block id: 3 */
                    uint64_t l_59 = 0x828C20713981DC8ALL;
                    int i;
                    for (g_5 = (-30); (g_5 != 21); g_5 = safe_add_func_int32_t_s_s(g_5, 3))
                    { /* block id: 6 */
                        int32_t l_31 = 6L;
                        uint8_t l_42 = 0x47L;
                        struct S0 l_64 = {0xE4C1L};
                        if ((safe_mod_func_uint32_t_u_u(((safe_mul_func_uint16_t_u_u((l_9[((l_4 + 6)) % 7] ^ ((safe_mod_func_uint8_t_u_u(l_9[((l_4 + 6)) % 7], l_9[(l_4) % 7])) <= (g_5 != g_5))), ((g_5 && (safe_lshift_func_uint8_t_u_s(l_9[3], l_9[((l_4 + 6)) % 7]))) != (18446744073709551614U < (g_5 & l_4))))) ^ (((0xA8D6L == (g_5 && g_5)) != ((safe_lshift_func_uint8_t_u_u(g_5, g_5)) | (l_31 || g_5))) ^ (safe_mod_func_int32_t_s_s((safe_sub_func_int8_t_s_s((g_5 > l_31), (-5L))), (g_5 || (safe_div_func_uint8_t_u_u(g_5, l_31))))))), 0xAF02C199L)))
                        { /* block id: 7 */
                            l_38 = ((l_14 < 0U) == (-7L));
                        }
                        else
                        { /* block id: 9 */
                            uint16_t l_52 = 0xDBC5L;
                            g_39 = g_39;
                            l_42 = (safe_div_func_uint32_t_u_u(4294967295U, 3U));
                            g_62 &= (safe_mul_func_uint16_t_u_u((g_5 & (safe_sub_func_int64_t_s_s((safe_sub_func_uint64_t_u_u((safe_unary_minus_func_int8_t_s((l_14 < l_9[(l_4) % 7]))), ((l_9[(l_4) % 7] ^ l_14) && (l_42 >= l_9[((l_4 + 6)) % 7])))), (safe_mul_func_uint8_t_u_u(g_5, ((l_52 <= l_14) != (safe_div_func_int32_t_s_s(l_9[(l_4) % 7], g_39.f0)))))))), (safe_rshift_func_int8_t_s_u((safe_lshift_func_int8_t_s_u((~l_59), 0)), (safe_mul_func_int16_t_s_s(l_6, (-3L)))))));
                            l_64 = l_63[8];
                        }
                        if (l_9[((l_4 + 6)) % 7])
                            continue;
                        return l_59;
                    }
                    g_5 |= l_38;
                    for (l_38 = 7; l_38 < 9; l_38 += 7)
                    { /* block id: 19 */
                        return g_5;
                    }
                    for (l_59 = 0; l_59 < 7; l_59 += 1)
                    {
                        l_9[l_59] = 0xADB0L;
                    }
                }
                else
                { /* block id: 23 */
                    l_38 &= (((-9L) <= g_39.f0) && (safe_sub_func_int32_t_s_s((safe_unary_minus_func_uint32_t_u((safe_sub_func_int16_t_s_s(g_39.f0, 0x3980L)))), ((g_39.f0 != (l_9[((l_4 + 4)) % 7] >= (g_39.f0 | l_9[1]))) | g_39.f0))));
                    l_74 = (safe_rshift_func_int16_t_s_s((l_9[(l_4) % 7] != ((safe_mul_func_int8_t_s_s(l_38, 0x3AL)) ^ (g_62 >= l_9[((l_4 + 6)) % 7]))), l_63[8].f0));
                    for (l_38 = 0; l_38 < 9; l_38 += 1)
                    {
                        struct S0 tmp = {-10L};
                        l_63[l_38] = tmp;
                    }
                    g_5 = ((l_9[(l_4) % 7] == g_5) < ((safe_mod_func_uint16_t_u_u(((safe_div_func_int16_t_s_s(l_9[(l_4) % 7], (l_9[4] && l_9[((l_4 + 6)) % 7]))) == (l_79 >= (g_39.f0 || g_62))), g_62)) < (safe_div_func_uint8_t_u_u((g_62 <= l_74), (((safe_mod_func_int64_t_s_s(l_9[(l_4) % 7], l_9[((l_4 + 6)) % 7])) <= (g_62 <= l_38)) && (safe_sub_func_int8_t_s_s((safe_div_func_int64_t_s_s(g_5, l_79)), l_9[((l_4 + 6)) % 7])))))));
                }
                g_5 = l_9[(l_4) % 7];
            }
            for (l_74 = 0; (l_74 != (-20)); l_74 = safe_sub_func_uint8_t_u_u(l_74, 2))
            { /* block id: 33 */
                return g_62;
            }
            for (g_39.f0 = (-23); (g_39.f0 >= (-7)); g_39.f0 = safe_add_func_int32_t_s_s(g_39.f0, 1))
            { /* block id: 38 */
                uint8_t l_109 = 252U;
                if (g_5)
                { /* block id: 39 */
                    int32_t l_92 = 0x0FE7B970L;
                    if (l_92)
                        break;
                }
                else
                { /* block id: 41 */
                    const int64_t l_97 = (-1L);
                    if (l_79)
                    { /* block id: 42 */
                        int i;
                        g_5 = 0L;
                        for (l_4 = 0; l_4 < 7; l_4 += 1)
                        { /* block id: 44 */
                            g_5 = ((safe_rshift_func_uint16_t_u_u((safe_add_func_int8_t_s_s(0xC4L, 0x96L)), ((-8L) || (l_74 != l_97)))) | (safe_mod_func_uint32_t_u_u(g_5, 8U)));
                            g_5 = l_38;
                        }
                        g_5 = (safe_add_func_int16_t_s_s((0xE65B8C0B7B9EACEELL ^ (g_62 >= (((safe_mod_func_uint16_t_u_u(l_9[5], l_97)) > (l_97 ^ g_39.f0)) || ((l_108 && l_109) != (safe_div_func_uint8_t_u_u(l_112, g_62)))))), (((+g_5) >= 4L) >= g_62)));
                    }
                    else
                    { /* block id: 49 */
                        g_5 = g_62;
                    }
                }
                l_115 = (safe_mod_func_uint32_t_u_u((~l_38), g_5));
            }
        }
        else
        { /* block id: 55 */
            return l_116;
        }
        g_5 &= l_6;
        return l_9[3];
    }
    
    
    
    
    /* ---------------------------------------- */
    int main (void)
    {
        int print_hash_value = 0;
        platform_main_begin();
        crc32_gentab();
        func_1();
        transparent_crc(g_5, "g_5", print_hash_value);
        transparent_crc(g_39.f0, "g_39.f0", print_hash_value);
        transparent_crc(g_62, "g_62", print_hash_value);
        platform_main_end(crc32_context ^ 0xFFFFFFFFUL);
        return 0;
    }
    
    /************************ statistics *************************
    XXX max struct depth: 1
    breakdown:
       depth: 0, occurrence: 19
       depth: 1, occurrence: 3
    
    XXX max expression depth: 2
    breakdown:
       depth: 0, occurrence: 24
       depth: 1, occurrence: 2
       depth: 2, occurrence: 1
    
    XXX total number of pointers: 0
    
    XXX times a non-volatile is read: 118
    XXX times a non-volatile is write: 20
    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: 0
    XXX backward jumps: 0
    
    XXX stmts: 60
    
    XXX percentage a fresh-made variable is used: 18.3
    XXX percentage an existing variable is used: 81.7
    ********************* end of statistics **********************/
    
    
    c file icon noterm.c (7,874 bytes) 2011-04-28 14:49 +

-Relationships
+Relationships

-Notes

~0001826

Anne (reporter)

I managed to reduce the problem to :
frama-c -slice-calls printf toto.c \
        -then-on 'Slicing export' -print -ocode toto.s.c

with toto.c :

#include <stdio.h>
int G;
void f (void) {
  int b = 7; int a = 2;
  if ((( a || 42) && b)) {
    while (1) { G = 21; return; }
  }
}
int main (void) {
  f();
  printf ("RES = %d\n", G);
  return 0;
}

but now, I have to see what's going wrong...

~0001827

Anne (reporter)

What I really don't understand is that if I put the internal form of the condition in the source code :
  if (a) { goto _LOR; }
  else {
    _LOR: /* internal */ ;
    if (b) { while (1) { ... } }
    }
It works !

~0001828

Anne (reporter)

Ok : in the generated internal form, there is a statement block in the else branch. This statement is unreachable since [a = 2] and the label is inside the block. That might be the reason why it doesn't work. Anyway, this is at least the difference between the 2 examples.

To be continued...

~0001831

Anne (reporter)

This is a problem with the lexical successor computation when there are unreachable statements. Will be fixed soon...

~0004800

Anne (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-04-28 14:49 pascal New Issue
2011-04-28 14:49 pascal Status new => assigned
2011-04-28 14:49 pascal Assigned To => Anne
2011-04-28 14:49 pascal File Added: noterm.c
2011-04-28 14:54 pascal Summary sliced program does not terminate => sliced program does not terminate (csmith)
2011-04-28 17:12 Anne Note Added: 0001826
2011-04-28 17:22 Anne Note Added: 0001827
2011-04-28 18:01 Anne Note Added: 0001828
2011-04-29 10:16 Anne Note Added: 0001831
2011-04-29 10:41 svn
2011-04-29 10:41 svn Status assigned => resolved
2011-04-29 10:41 svn 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
2013-12-19 01:12 Anne Source_changeset_attached => framac master 2c930d6e
2014-02-12 16:54 Anne Source_changeset_attached => framac stable/neon 2c930d6e
2014-02-12 16:59 Anne Note Added: 0004800
2014-02-12 16:59 Anne Status closed => resolved
+Issue History