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