[csmith-dev] version 7d6fae9: x = x = …;

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

Hello,

the attached program was generated after updating Csmith from Git today.
I offer that that program is defined only if the program below is defined:

int x;
int main(int argc, char **argv) {
  x = x = 2;
  return x;
}

But both Frama-C's value analysis and KCC's June version
seem to think that the short version,
and therefore the long version, are undefined.

KCC's error message is "Unsequenced side effect on scalar
object with side effect of same object". Frama-C's error message
is that you should only reach the assignment with memory states
in which you can prove "\separated(& x,& x)". That formula
is equivalent to false, meaning that the value analysis thinks
there is a definite problem at the assignment.

I am pretty certain they are worried about the same thing,
although I wouldn't like to commit myself on whether
they are both right or both wrong.

Pascal

/*
 * This is a RANDOMLY GENERATED PROGRAM.
 *
 * Generator: csmith 2.1.0
 * Git version: 7d6fae9
 * Options:   --max-pointer-depth 3 --max-funcs 3 --max-array-dim 2 --max-array-len-per-dim 3 --max-struct-fields 3 --no-volatiles --no-argc --no-unions
 * Seed:      3180327032
 */

#include "csmith.h"


static long __undefined;

/* --- Struct/Union Declarations --- */
/* --- GLOBAL VARIABLES --- */
static uint8_t g_4[2] = {0x57L, 0x57L};
static int32_t g_6[2] = {0x67FA5C62L, 0x67FA5C62L};


/* --- FORWARD DECLARATIONS --- */
static uint32_t  func_1(void);


/* --- FUNCTIONS --- */
/* ------------------------------------------ */
/* 
 * reads : g_4 g_6
 * writes: g_6
 */
static uint32_t  func_1(void)
{ /* block id: 0 */
    int32_t *l_5 = &g_6[1];
    (*l_5) = ((*l_5) = ((*l_5) = ((*l_5) |= (safe_rshift_func_uint16_t_u_u(g_4[0], g_4[0])))));
    return (*l_5);
}




/* ---------------------------------------- */
int main (void)
{
    int i;
    int print_hash_value = 0;
    platform_main_begin();
    crc32_gentab();
    func_1();
    for (i = 0; i < 2; i++)
    {
        transparent_crc(g_4[i], "g_4[i]", print_hash_value);
        if (print_hash_value) printf("index = [%d]\n", i);

    }
    for (i = 0; i < 2; i++)
    {
        transparent_crc(g_6[i], "g_6[i]", print_hash_value);
        if (print_hash_value) printf("index = [%d]\n", i);

    }
    platform_main_end(crc32_context ^ 0xFFFFFFFFUL, print_hash_value);
    return 0;
}

/************************ statistics *************************
XXX max struct depth: 0
breakdown:
   depth: 0, occurrence: 1
XXX total union variables: 0

XXX max expression depth: 0
breakdown:
   depth: 0, occurrence: 5

XXX total number of pointers: 1

XXX times a variable address is taken: 1
XXX times a pointer is dereferenced on RHS: 1
breakdown:
   depth: 1, occurrence: 1
XXX times a pointer is dereferenced on LHS: 4
breakdown:
   depth: 1, occurrence: 4
XXX times a pointer is compared with null: 0
XXX times a pointer is compared with address of another variable: 0
XXX times a pointer is compared with another pointer: 0
XXX times a pointer is qualified to be dereferenced: 4

XXX max dereference level: 1
breakdown:
   level: 0, occurrence: 0
   level: 1, occurrence: 10
XXX number of pointers point to pointers: 0
XXX number of pointers point to scalars: 1
XXX number of pointers point to structs: 0
XXX percent of pointers has null in alias set: 0
XXX average alias set size: 1

XXX times a non-volatile is read: 4
XXX times a non-volatile is write: 8
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: 6

XXX percentage a fresh-made variable is used: 25
XXX percentage an existing variable is used: 75
********************* end of statistics **********************/