[csmith-dev] Generated programs do not satify 6.5.16.1:3

[Pascal Cuoq <pascal.cuoq@gmail.com>]

Hello,

The following paragraph comes from a private discussion between
John, Chucky and me (Chucky is writing):

> There are plenty of union errors to be had.  Derek sent me this
> program, which kcc fails to catch:
> union { int i; char c; } ic;
> int main(void){ ic.c = ic.i; }
> The semantics 6.5.16.1:3 says "If the value being stored in an object
> is read from another object that overlaps in any way the storage of
> the first object, then the overlap shall be exact..."

I am not convinced I want to warn for the quoted
example, where both memory accesses are atomic
and where there is a conversion between the read
access and the write access anyway. But, for assignment
of structs, the possibility of overlap between source and
destination clearly is a concern. The compiler may implement
the struct assignment with memcpy() or an inlined,
specialized version of memcpy().

Based on the example below, it seems to me that
Csmith may generate programs that do not respect the above
rule.

/*
 * This is a RANDOMLY GENERATED PROGRAM.
 *
 * Generator: csmith 2.1.0
 * Git version: ea4762b
 * Options:   --max-pointer-depth 2 --max-funcs 4 --max-array-dim 2 --max-array-len-per-dim 4 --max-struct-fields 15 --max-union-fields 15 --no-volatiles --no-bitfields --no-argc --unions
 * Seed:      199711046
 */

That example contains:

/* ------------------------------------------ */
/* 
 * reads :
 * writes: g_44
 */
static uint32_t  func_24(int8_t ** p_25, int8_t ** p_26, union U2  p_27)
{ /* block id: 132 */
    struct S0 *l_235[1];
    int32_t l_236 = (-1L);
    int i;
    for (i = 0; i < 1; i++)
        l_235[i] = &g_103[0].f3;
    g_44 = (p_27.f2.f3 = p_27.f0);
    return l_236;
}

In this function, the assignment p_27.f2.f3 = p_27.f0 seems to violate 
the quoted rule, and indeed, I get different results with different
meaning-giving systems for C programs (the clang compiler on
the one hand and Frama-C on the other hand).
Besides, clang also gives different results between
-O0 and -O2.

Frama-C does not implement the "no partial overlap" rule yet —I examined
this example because of results mismatches, not because it had
emitted an alarm— but it seems it will have to in order to be as correct
as we want it to be.

Pascal