2021-02-24 19:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000717Frama-CPlug-in > Evapublic2014-02-12 16:59
Reporterregehr 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000717: possible unsoundness bug
DescriptionThis is on Ubuntu 10.10 on x86.

Analyzing the attached program like this:

  toplevel.opt -val -slevel 24 foo_pp.c

Gives output including:

  *(unsigned char*)((unsigned char*)&g_8+30) == 0

However, running the program leaves the value 243 in this byte.
TagsNo tags attached.
Attached Files
  • c file icon foo_pp.c (38,138 bytes) 2011-02-12 20:05 -
    # 1 "foo.c"
    # 1 "foo.c" 1
    # 1 "<built-in>" 1
    # 1 "<built-in>" 3
    # 128 "<built-in>" 3
    # 1 "<command line>" 1
    # 1 "<built-in>" 2
    # 1 "foo.c" 2
    # 10 "foo.c"
    # 1 "/mnt/z/csmith/runtime/random_inc.h" 1
    # 51 "/mnt/z/csmith/runtime/random_inc.h"
    # 1 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/limits.h" 1 3 4
    # 38 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/limits.h" 3 4
    # 1 "/usr/include/limits.h" 1 3 4
    # 27 "/usr/include/limits.h" 3 4
    # 1 "/usr/include/features.h" 1 3 4
    # 322 "/usr/include/features.h" 3 4
    # 1 "/usr/include/bits/predefs.h" 1 3 4
    # 323 "/usr/include/features.h" 2 3 4
    # 355 "/usr/include/features.h" 3 4
    # 1 "/usr/include/sys/cdefs.h" 1 3 4
    # 353 "/usr/include/sys/cdefs.h" 3 4
    # 1 "/usr/include/bits/wordsize.h" 1 3 4
    # 354 "/usr/include/sys/cdefs.h" 2 3 4
    # 356 "/usr/include/features.h" 2 3 4
    # 387 "/usr/include/features.h" 3 4
    # 1 "/usr/include/gnu/stubs.h" 1 3 4
    
    
    
    # 1 "/usr/include/bits/wordsize.h" 1 3 4
    # 5 "/usr/include/gnu/stubs.h" 2 3 4
    
    
    # 1 "/usr/include/gnu/stubs-32.h" 1 3 4
    # 8 "/usr/include/gnu/stubs.h" 2 3 4
    # 388 "/usr/include/features.h" 2 3 4
    # 28 "/usr/include/limits.h" 2 3 4
    # 145 "/usr/include/limits.h" 3 4
    # 1 "/usr/include/bits/posix1_lim.h" 1 3 4
    # 157 "/usr/include/bits/posix1_lim.h" 3 4
    # 1 "/usr/include/bits/local_lim.h" 1 3 4
    # 39 "/usr/include/bits/local_lim.h" 3 4
    # 1 "/usr/include/linux/limits.h" 1 3 4
    # 40 "/usr/include/bits/local_lim.h" 2 3 4
    # 158 "/usr/include/bits/posix1_lim.h" 2 3 4
    # 146 "/usr/include/limits.h" 2 3 4
    
    
    
    # 1 "/usr/include/bits/posix2_lim.h" 1 3 4
    # 150 "/usr/include/limits.h" 2 3 4
    # 39 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/limits.h" 2 3 4
    # 52 "/mnt/z/csmith/runtime/random_inc.h" 2
    
    
    
    # 1 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdint.h" 1 3 4
    # 33 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdint.h" 3 4
    # 1 "/usr/include/stdint.h" 1 3 4
    # 27 "/usr/include/stdint.h" 3 4
    # 1 "/usr/include/bits/wchar.h" 1 3 4
    # 28 "/usr/include/stdint.h" 2 3 4
    # 1 "/usr/include/bits/wordsize.h" 1 3 4
    # 29 "/usr/include/stdint.h" 2 3 4
    
    
    
    
    
    
    
    
    typedef signed char int8_t;
    typedef short int int16_t;
    typedef int int32_t;
    
    
    
    __extension__
    typedef long long int int64_t;
    
    
    
    
    typedef unsigned char uint8_t;
    typedef unsigned short int uint16_t;
    
    typedef unsigned int uint32_t;
    
    
    
    
    
    __extension__
    typedef unsigned long long int uint64_t;
    
    
    
    
    
    
    typedef signed char int_least8_t;
    typedef short int int_least16_t;
    typedef int int_least32_t;
    
    
    
    __extension__
    typedef long long int int_least64_t;
    
    
    
    typedef unsigned char uint_least8_t;
    typedef unsigned short int uint_least16_t;
    typedef unsigned int uint_least32_t;
    
    
    
    __extension__
    typedef unsigned long long int uint_least64_t;
    
    
    
    
    
    
    typedef signed char int_fast8_t;
    
    
    
    
    
    typedef int int_fast16_t;
    typedef int int_fast32_t;
    __extension__
    typedef long long int int_fast64_t;
    
    
    
    typedef unsigned char uint_fast8_t;
    
    
    
    
    
    typedef unsigned int uint_fast16_t;
    typedef unsigned int uint_fast32_t;
    __extension__
    typedef unsigned long long int uint_fast64_t;
    # 126 "/usr/include/stdint.h" 3 4
    typedef int intptr_t;
    
    
    typedef unsigned int uintptr_t;
    # 138 "/usr/include/stdint.h" 3 4
    __extension__
    typedef long long int intmax_t;
    __extension__
    typedef unsigned long long int uintmax_t;
    # 34 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdint.h" 2 3 4
    # 56 "/mnt/z/csmith/runtime/random_inc.h" 2
    
    
    
    
    # 1 "/usr/include/assert.h" 1 3 4
    # 71 "/usr/include/assert.h" 3 4
    extern void __assert_fail (__const char *__assertion, __const char *__file,
          unsigned int __line, __const char *__function)
         __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
    
    
    extern void __assert_perror_fail (int __errnum, __const char *__file,
          unsigned int __line,
          __const char *__function)
         __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
    
    
    
    
    extern void __assert (const char *__assertion, const char *__file, int __line)
         __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
    # 61 "/mnt/z/csmith/runtime/random_inc.h" 2
    # 78 "/mnt/z/csmith/runtime/random_inc.h"
    # 1 "/mnt/z/csmith/runtime/platform_generic.h" 1
    # 40 "/mnt/z/csmith/runtime/platform_generic.h"
    # 1 "/usr/include/stdio.h" 1 3 4
    # 34 "/usr/include/stdio.h" 3 4
    # 1 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stddef.h" 1 3 4
    # 29 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stddef.h" 3 4
    typedef __typeof__(((int*)0)-((int*)0)) ptrdiff_t;
    
    
    typedef __typeof__(sizeof(int)) size_t;
    
    
    
    
    typedef int wchar_t;
    # 35 "/usr/include/stdio.h" 2 3 4
    
    # 1 "/usr/include/bits/types.h" 1 3 4
    # 28 "/usr/include/bits/types.h" 3 4
    # 1 "/usr/include/bits/wordsize.h" 1 3 4
    # 29 "/usr/include/bits/types.h" 2 3 4
    
    
    typedef unsigned char __u_char;
    typedef unsigned short int __u_short;
    typedef unsigned int __u_int;
    typedef unsigned long int __u_long;
    
    
    typedef signed char __int8_t;
    typedef unsigned char __uint8_t;
    typedef signed short int __int16_t;
    typedef unsigned short int __uint16_t;
    typedef signed int __int32_t;
    typedef unsigned int __uint32_t;
    
    
    
    
    __extension__ typedef signed long long int __int64_t;
    __extension__ typedef unsigned long long int __uint64_t;
    
    
    
    
    
    
    
    __extension__ typedef long long int __quad_t;
    __extension__ typedef unsigned long long int __u_quad_t;
    # 131 "/usr/include/bits/types.h" 3 4
    # 1 "/usr/include/bits/typesizes.h" 1 3 4
    # 132 "/usr/include/bits/types.h" 2 3 4
    
    
    __extension__ typedef __u_quad_t __dev_t;
    __extension__ typedef unsigned int __uid_t;
    __extension__ typedef unsigned int __gid_t;
    __extension__ typedef unsigned long int __ino_t;
    __extension__ typedef __u_quad_t __ino64_t;
    __extension__ typedef unsigned int __mode_t;
    __extension__ typedef unsigned int __nlink_t;
    __extension__ typedef long int __off_t;
    __extension__ typedef __quad_t __off64_t;
    __extension__ typedef int __pid_t;
    __extension__ typedef struct { int __val[2]; } __fsid_t;
    __extension__ typedef long int __clock_t;
    __extension__ typedef unsigned long int __rlim_t;
    __extension__ typedef __u_quad_t __rlim64_t;
    __extension__ typedef unsigned int __id_t;
    __extension__ typedef long int __time_t;
    __extension__ typedef unsigned int __useconds_t;
    __extension__ typedef long int __suseconds_t;
    
    __extension__ typedef int __daddr_t;
    __extension__ typedef long int __swblk_t;
    __extension__ typedef int __key_t;
    
    
    __extension__ typedef int __clockid_t;
    
    
    __extension__ typedef void * __timer_t;
    
    
    __extension__ typedef long int __blksize_t;
    
    
    
    
    __extension__ typedef long int __blkcnt_t;
    __extension__ typedef __quad_t __blkcnt64_t;
    
    
    __extension__ typedef unsigned long int __fsblkcnt_t;
    __extension__ typedef __u_quad_t __fsblkcnt64_t;
    
    
    __extension__ typedef unsigned long int __fsfilcnt_t;
    __extension__ typedef __u_quad_t __fsfilcnt64_t;
    
    __extension__ typedef int __ssize_t;
    
    
    
    typedef __off64_t __loff_t;
    typedef __quad_t *__qaddr_t;
    typedef char *__caddr_t;
    
    
    __extension__ typedef int __intptr_t;
    
    
    __extension__ typedef unsigned int __socklen_t;
    # 37 "/usr/include/stdio.h" 2 3 4
    
    
    
    
    
    
    
    
    struct _IO_FILE;
    
    
    
    typedef struct _IO_FILE FILE;
    # 65 "/usr/include/stdio.h" 3 4
    typedef struct _IO_FILE __FILE;
    # 75 "/usr/include/stdio.h" 3 4
    # 1 "/usr/include/libio.h" 1 3 4
    # 32 "/usr/include/libio.h" 3 4
    # 1 "/usr/include/_G_config.h" 1 3 4
    # 15 "/usr/include/_G_config.h" 3 4
    # 1 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stddef.h" 1 3 4
    # 16 "/usr/include/_G_config.h" 2 3 4
    
    
    
    
    # 1 "/usr/include/wchar.h" 1 3 4
    # 83 "/usr/include/wchar.h" 3 4
    typedef struct
    {
      int __count;
      union
      {
    
        unsigned int __wch;
    
    
    
        char __wchb[4];
      } __value;
    } __mbstate_t;
    # 21 "/usr/include/_G_config.h" 2 3 4
    
    typedef struct
    {
      __off_t __pos;
      __mbstate_t __state;
    } _G_fpos_t;
    typedef struct
    {
      __off64_t __pos;
      __mbstate_t __state;
    } _G_fpos64_t;
    # 53 "/usr/include/_G_config.h" 3 4
    typedef int _G_int16_t __attribute__ ((__mode__ (__HI__)));
    typedef int _G_int32_t __attribute__ ((__mode__ (__SI__)));
    typedef unsigned int _G_uint16_t __attribute__ ((__mode__ (__HI__)));
    typedef unsigned int _G_uint32_t __attribute__ ((__mode__ (__SI__)));
    # 33 "/usr/include/libio.h" 2 3 4
    # 53 "/usr/include/libio.h" 3 4
    # 1 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdarg.h" 1 3 4
    # 30 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdarg.h" 3 4
    typedef __builtin_va_list va_list;
    # 48 "/mnt/z/z/compiler-install/llvm-gcc-r125433-install/bin/../lib/clang/2.9/include/stdarg.h" 3 4
    typedef __builtin_va_list __gnuc_va_list;
    # 54 "/usr/include/libio.h" 2 3 4
    # 170 "/usr/include/libio.h" 3 4
    struct _IO_jump_t; struct _IO_FILE;
    # 180 "/usr/include/libio.h" 3 4
    typedef void _IO_lock_t;
    
    
    
    
    
    struct _IO_marker {
      struct _IO_marker *_next;
      struct _IO_FILE *_sbuf;
    
    
    
      int _pos;
    # 203 "/usr/include/libio.h" 3 4
    };
    
    
    enum __codecvt_result
    {
      __codecvt_ok,
      __codecvt_partial,
      __codecvt_error,
      __codecvt_noconv
    };
    # 271 "/usr/include/libio.h" 3 4
    struct _IO_FILE {
      int _flags;
    
    
    
    
      char* _IO_read_ptr;
      char* _IO_read_end;
      char* _IO_read_base;
      char* _IO_write_base;
      char* _IO_write_ptr;
      char* _IO_write_end;
      char* _IO_buf_base;
      char* _IO_buf_end;
    
      char *_IO_save_base;
      char *_IO_backup_base;
      char *_IO_save_end;
    
      struct _IO_marker *_markers;
    
      struct _IO_FILE *_chain;
    
      int _fileno;
    
    
    
      int _flags2;
    
      __off_t _old_offset;
    
    
    
      unsigned short _cur_column;
      signed char _vtable_offset;
      char _shortbuf[1];
    
    
    
      _IO_lock_t *_lock;
    # 319 "/usr/include/libio.h" 3 4
      __off64_t _offset;
    # 328 "/usr/include/libio.h" 3 4
      void *__pad1;
      void *__pad2;
      void *__pad3;
      void *__pad4;
      size_t __pad5;
    
      int _mode;
    
      char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
    
    };
    
    
    typedef struct _IO_FILE _IO_FILE;
    
    
    struct _IO_FILE_plus;
    
    extern struct _IO_FILE_plus _IO_2_1_stdin_;
    extern struct _IO_FILE_plus _IO_2_1_stdout_;
    extern struct _IO_FILE_plus _IO_2_1_stderr_;
    # 364 "/usr/include/libio.h" 3 4
    typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
    
    
    
    
    
    
    
    typedef __ssize_t __io_write_fn (void *__cookie, __const char *__buf,
         size_t __n);
    
    
    
    
    
    
    
    typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
    
    
    typedef int __io_close_fn (void *__cookie);
    # 416 "/usr/include/libio.h" 3 4
    extern int __underflow (_IO_FILE *);
    extern int __uflow (_IO_FILE *);
    extern int __overflow (_IO_FILE *, int);
    # 460 "/usr/include/libio.h" 3 4
    extern int _IO_getc (_IO_FILE *__fp);
    extern int _IO_putc (int __c, _IO_FILE *__fp);
    extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__));
    extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__));
    
    extern int _IO_peekc_locked (_IO_FILE *__fp);
    
    
    
    
    
    extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__));
    extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__));
    extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__));
    # 490 "/usr/include/libio.h" 3 4
    extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
       __gnuc_va_list, int *__restrict);
    extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
        __gnuc_va_list);
    extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
    extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
    
    extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
    extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
    
    extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__));
    # 76 "/usr/include/stdio.h" 2 3 4
    
    
    
    
    typedef __gnuc_va_list va_list;
    # 91 "/usr/include/stdio.h" 3 4
    typedef __off_t off_t;
    # 103 "/usr/include/stdio.h" 3 4
    typedef __ssize_t ssize_t;
    
    
    
    
    
    
    
    typedef _G_fpos_t fpos_t;
    # 161 "/usr/include/stdio.h" 3 4
    # 1 "/usr/include/bits/stdio_lim.h" 1 3 4
    # 162 "/usr/include/stdio.h" 2 3 4
    
    
    
    extern struct _IO_FILE *stdin;
    extern struct _IO_FILE *stdout;
    extern struct _IO_FILE *stderr;
    
    
    
    
    
    
    
    extern int remove (__const char *__filename) __attribute__ ((__nothrow__));
    
    extern int rename (__const char *__old, __const char *__new) __attribute__ ((__nothrow__));
    
    
    
    
    extern int renameat (int __oldfd, __const char *__old, int __newfd,
           __const char *__new) __attribute__ ((__nothrow__));
    # 192 "/usr/include/stdio.h" 3 4
    extern FILE *tmpfile (void) ;
    # 206 "/usr/include/stdio.h" 3 4
    extern char *tmpnam (char *__s) __attribute__ ((__nothrow__)) ;
    
    
    
    
    
    extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__)) ;
    # 224 "/usr/include/stdio.h" 3 4
    extern char *tempnam (__const char *__dir, __const char *__pfx)
         __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
    # 234 "/usr/include/stdio.h" 3 4
    extern int fclose (FILE *__stream);
    
    
    
    
    extern int fflush (FILE *__stream);
    # 249 "/usr/include/stdio.h" 3 4
    extern int fflush_unlocked (FILE *__stream);
    # 269 "/usr/include/stdio.h" 3 4
    extern FILE *fopen (__const char *__restrict __filename,
          __const char *__restrict __modes) ;
    
    
    
    
    extern FILE *freopen (__const char *__restrict __filename,
            __const char *__restrict __modes,
            FILE *__restrict __stream) ;
    # 303 "/usr/include/stdio.h" 3 4
    extern FILE *fdopen (int __fd, __const char *__modes) __attribute__ ((__nothrow__)) ;
    # 316 "/usr/include/stdio.h" 3 4
    extern FILE *fmemopen (void *__s, size_t __len, __const char *__modes)
      __attribute__ ((__nothrow__)) ;
    
    
    
    
    extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__)) ;
    
    
    
    
    
    
    extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__));
    
    
    
    extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
          int __modes, size_t __n) __attribute__ ((__nothrow__));
    
    
    
    
    
    extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
             size_t __size) __attribute__ ((__nothrow__));
    
    
    extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__));
    # 353 "/usr/include/stdio.h" 3 4
    extern int fprintf (FILE *__restrict __stream,
          __const char *__restrict __format, ...);
    
    
    
    
    extern int printf (__const char *__restrict __format, ...);
    
    extern int sprintf (char *__restrict __s,
          __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
    
    
    
    
    
    extern int vfprintf (FILE *__restrict __s, __const char *__restrict __format,
           __gnuc_va_list __arg);
    
    
    
    
    extern int vprintf (__const char *__restrict __format, __gnuc_va_list __arg);
    
    extern int vsprintf (char *__restrict __s, __const char *__restrict __format,
           __gnuc_va_list __arg) __attribute__ ((__nothrow__));
    
    
    
    
    
    extern int snprintf (char *__restrict __s, size_t __maxlen,
           __const char *__restrict __format, ...)
         __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
    
    extern int vsnprintf (char *__restrict __s, size_t __maxlen,
            __const char *__restrict __format, __gnuc_va_list __arg)
         __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
    # 414 "/usr/include/stdio.h" 3 4
    extern int vdprintf (int __fd, __const char *__restrict __fmt,
           __gnuc_va_list __arg)
         __attribute__ ((__format__ (__printf__, 2, 0)));
    extern int dprintf (int __fd, __const char *__restrict __fmt, ...)
         __attribute__ ((__format__ (__printf__, 2, 3)));
    # 427 "/usr/include/stdio.h" 3 4
    extern int fscanf (FILE *__restrict __stream,
         __const char *__restrict __format, ...) ;
    
    
    
    
    extern int scanf (__const char *__restrict __format, ...) ;
    
    extern int sscanf (__const char *__restrict __s,
         __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
    # 445 "/usr/include/stdio.h" 3 4
    extern int fscanf (FILE *__restrict __stream, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf") ;
    
    
    extern int scanf (__const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf") ;
    
    extern int sscanf (__const char *__restrict __s, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__));
    # 473 "/usr/include/stdio.h" 3 4
    extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format,
          __gnuc_va_list __arg)
         __attribute__ ((__format__ (__scanf__, 2, 0))) ;
    
    
    
    
    
    extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg)
         __attribute__ ((__format__ (__scanf__, 1, 0))) ;
    
    
    extern int vsscanf (__const char *__restrict __s,
          __const char *__restrict __format, __gnuc_va_list __arg)
         __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
    # 496 "/usr/include/stdio.h" 3 4
    extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
    
    
    
         __attribute__ ((__format__ (__scanf__, 2, 0))) ;
    extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
    
         __attribute__ ((__format__ (__scanf__, 1, 0))) ;
    extern int vsscanf (__const char *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__))
    
    
    
         __attribute__ ((__format__ (__scanf__, 2, 0)));
    # 533 "/usr/include/stdio.h" 3 4
    extern int fgetc (FILE *__stream);
    extern int getc (FILE *__stream);
    
    
    
    
    
    extern int getchar (void);
    # 552 "/usr/include/stdio.h" 3 4
    extern int getc_unlocked (FILE *__stream);
    extern int getchar_unlocked (void);
    # 563 "/usr/include/stdio.h" 3 4
    extern int fgetc_unlocked (FILE *__stream);
    # 575 "/usr/include/stdio.h" 3 4
    extern int fputc (int __c, FILE *__stream);
    extern int putc (int __c, FILE *__stream);
    
    
    
    
    
    extern int putchar (int __c);
    # 596 "/usr/include/stdio.h" 3 4
    extern int fputc_unlocked (int __c, FILE *__stream);
    
    
    
    
    
    
    
    extern int putc_unlocked (int __c, FILE *__stream);
    extern int putchar_unlocked (int __c);
    
    
    
    
    
    
    extern int getw (FILE *__stream);
    
    
    extern int putw (int __w, FILE *__stream);
    # 624 "/usr/include/stdio.h" 3 4
    extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
              ;
    
    
    
    
    
    
    extern char *gets (char *__s) ;
    # 658 "/usr/include/stdio.h" 3 4
    extern __ssize_t __getdelim (char **__restrict __lineptr,
              size_t *__restrict __n, int __delimiter,
              FILE *__restrict __stream) ;
    extern __ssize_t getdelim (char **__restrict __lineptr,
            size_t *__restrict __n, int __delimiter,
            FILE *__restrict __stream) ;
    
    
    
    
    
    
    
    extern __ssize_t getline (char **__restrict __lineptr,
           size_t *__restrict __n,
           FILE *__restrict __stream) ;
    # 682 "/usr/include/stdio.h" 3 4
    extern int fputs (__const char *__restrict __s, FILE *__restrict __stream);
    
    
    
    
    
    extern int puts (__const char *__s);
    
    
    
    
    
    
    extern int ungetc (int __c, FILE *__stream);
    
    
    
    
    
    
    extern size_t fread (void *__restrict __ptr, size_t __size,
           size_t __n, FILE *__restrict __stream) ;
    
    
    
    
    extern size_t fwrite (__const void *__restrict __ptr, size_t __size,
            size_t __n, FILE *__restrict __s);
    # 730 "/usr/include/stdio.h" 3 4
    extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
             size_t __n, FILE *__restrict __stream) ;
    extern size_t fwrite_unlocked (__const void *__restrict __ptr, size_t __size,
              size_t __n, FILE *__restrict __stream);
    # 742 "/usr/include/stdio.h" 3 4
    extern int fseek (FILE *__stream, long int __off, int __whence);
    
    
    
    
    extern long int ftell (FILE *__stream) ;
    
    
    
    
    extern void rewind (FILE *__stream);
    # 766 "/usr/include/stdio.h" 3 4
    extern int fseeko (FILE *__stream, __off_t __off, int __whence);
    
    
    
    
    extern __off_t ftello (FILE *__stream) ;
    # 791 "/usr/include/stdio.h" 3 4
    extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
    
    
    
    
    extern int fsetpos (FILE *__stream, __const fpos_t *__pos);
    # 819 "/usr/include/stdio.h" 3 4
    extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__));
    
    extern int feof (FILE *__stream) __attribute__ ((__nothrow__)) ;
    
    extern int ferror (FILE *__stream) __attribute__ ((__nothrow__)) ;
    
    
    
    
    extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__));
    extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
    extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
    # 839 "/usr/include/stdio.h" 3 4
    extern void perror (__const char *__s);
    
    
    
    
    
    
    
    # 1 "/usr/include/bits/sys_errlist.h" 1 3 4
    # 27 "/usr/include/bits/sys_errlist.h" 3 4
    extern int sys_nerr;
    extern __const char *__const sys_errlist[];
    # 847 "/usr/include/stdio.h" 2 3 4
    
    
    
    
    extern int fileno (FILE *__stream) __attribute__ ((__nothrow__)) ;
    
    
    
    
    extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
    # 866 "/usr/include/stdio.h" 3 4
    extern FILE *popen (__const char *__command, __const char *__modes) ;
    
    
    
    
    
    extern int pclose (FILE *__stream);
    
    
    
    
    
    extern char *ctermid (char *__s) __attribute__ ((__nothrow__));
    # 906 "/usr/include/stdio.h" 3 4
    extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__));
    
    
    
    extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__)) ;
    
    
    extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__));
    # 41 "/mnt/z/csmith/runtime/platform_generic.h" 2
    
    
    static void
    platform_main_begin(void)
    {
    
    }
    
    static void
    platform_main_end(uint32_t crc)
    {
    
        Frama_C_dump_assert_each();
    
     printf ("checksum = %X\n", crc);
    }
    # 79 "/mnt/z/csmith/runtime/random_inc.h" 2
    # 96 "/mnt/z/csmith/runtime/random_inc.h"
    # 1 "/mnt/z/csmith/runtime/safe_math.h" 1
    # 13 "/mnt/z/csmith/runtime/safe_math.h"
    static int8_t
    (safe_unary_minus_func_int8_t_s)(int8_t si)
    {
      return
    
    
    
    
    
    
        -si;
    }
    
    static int8_t
    (safe_add_func_int8_t_s_s)(int8_t si1, int8_t si2)
    {
      return
    
    
    
    
    
    
        (si1 + si2);
    }
    
    static int8_t
    (safe_sub_func_int8_t_s_s)(int8_t si1, int8_t si2)
    {
      return
    
    
    
    
    
    
        (si1 - si2);
    }
    
    static int8_t
    (safe_mul_func_int8_t_s_s)(int8_t si1, int8_t si2)
    {
      return
    
    
    
    
    
    
        si1 * si2;
    }
    
    static int8_t
    (safe_mod_func_int8_t_s_s)(int8_t si1, int8_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-128)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 % si2);
    }
    
    static int8_t
    (safe_div_func_int8_t_s_s)(int8_t si1, int8_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-128)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 / si2);
    }
    
    static int8_t
    (safe_lshift_func_int8_t_s_s)(int8_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32) || (left > ((127) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static int8_t
    (safe_lshift_func_int8_t_s_u)(int8_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32) || (left > ((127) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static int8_t
    (safe_rshift_func_int8_t_s_s)(int8_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32))?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static int8_t
    (safe_rshift_func_int8_t_s_u)(int8_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    static int16_t
    (safe_unary_minus_func_int16_t_s)(int16_t si)
    {
      return
    
    
    
    
    
    
        -si;
    }
    
    static int16_t
    (safe_add_func_int16_t_s_s)(int16_t si1, int16_t si2)
    {
      return
    
    
    
    
    
    
        (si1 + si2);
    }
    
    static int16_t
    (safe_sub_func_int16_t_s_s)(int16_t si1, int16_t si2)
    {
      return
    
    
    
    
    
    
        (si1 - si2);
    }
    
    static int16_t
    (safe_mul_func_int16_t_s_s)(int16_t si1, int16_t si2)
    {
      return
    
    
    
    
    
    
        si1 * si2;
    }
    
    static int16_t
    (safe_mod_func_int16_t_s_s)(int16_t si1, int16_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-32767 -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 % si2);
    }
    
    static int16_t
    (safe_div_func_int16_t_s_s)(int16_t si1, int16_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-32767 -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 / si2);
    }
    
    static int16_t
    (safe_lshift_func_int16_t_s_s)(int16_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32) || (left > ((32767) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static int16_t
    (safe_lshift_func_int16_t_s_u)(int16_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32) || (left > ((32767) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static int16_t
    (safe_rshift_func_int16_t_s_s)(int16_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32))?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static int16_t
    (safe_rshift_func_int16_t_s_u)(int16_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    static int32_t
    (safe_unary_minus_func_int32_t_s)(int32_t si)
    {
      return
    
    
        (si==(-2147483647 -1)) ?
        ((si)) :
    
    
        -si;
    }
    
    static int32_t
    (safe_add_func_int32_t_s_s)(int32_t si1, int32_t si2)
    {
      return
    
    
        (((si1>0) && (si2>0) && (si1 > ((2147483647)-si2))) || ((si1<0) && (si2<0) && (si1 < ((-2147483647 -1)-si2)))) ?
        ((si1)) :
    
    
        (si1 + si2);
    }
    
    static int32_t
    (safe_sub_func_int32_t_s_s)(int32_t si1, int32_t si2)
    {
      return
    
    
        (((si1^si2) & (((si1 ^ ((si1^si2) & (~(2147483647))))-si2)^si2)) < 0) ?
        ((si1)) :
    
    
        (si1 - si2);
    }
    
    static int32_t
    (safe_mul_func_int32_t_s_s)(int32_t si1, int32_t si2)
    {
      return
    
    
        (((si1 > 0) && (si2 > 0) && (si1 > ((2147483647) / si2))) || ((si1 > 0) && (si2 <= 0) && (si2 < ((-2147483647 -1) / si1))) || ((si1 <= 0) && (si2 > 0) && (si1 < ((-2147483647 -1) / si2))) || ((si1 <= 0) && (si2 <= 0) && (si1 != 0) && (si2 < ((2147483647) / si1)))) ?
        ((si1)) :
    
    
        si1 * si2;
    }
    
    static int32_t
    (safe_mod_func_int32_t_s_s)(int32_t si1, int32_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-2147483647 -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 % si2);
    }
    
    static int32_t
    (safe_div_func_int32_t_s_s)(int32_t si1, int32_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-2147483647 -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 / si2);
    }
    
    static int32_t
    (safe_lshift_func_int32_t_s_s)(int32_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32) || (left > ((2147483647) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static int32_t
    (safe_lshift_func_int32_t_s_u)(int32_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32) || (left > ((2147483647) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static int32_t
    (safe_rshift_func_int32_t_s_s)(int32_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32))?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static int32_t
    (safe_rshift_func_int32_t_s_u)(int32_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    
    static int64_t
    (safe_unary_minus_func_int64_t_s)(int64_t si)
    {
      return
    
    
        (si==(-9223372036854775807LL -1)) ?
        ((si)) :
    
    
        -si;
    }
    
    static int64_t
    (safe_add_func_int64_t_s_s)(int64_t si1, int64_t si2)
    {
      return
    
    
        (((si1>0) && (si2>0) && (si1 > ((9223372036854775807LL)-si2))) || ((si1<0) && (si2<0) && (si1 < ((-9223372036854775807LL -1)-si2)))) ?
        ((si1)) :
    
    
        (si1 + si2);
    }
    
    static int64_t
    (safe_sub_func_int64_t_s_s)(int64_t si1, int64_t si2)
    {
      return
    
    
        (((si1^si2) & (((si1 ^ ((si1^si2) & (~(9223372036854775807LL))))-si2)^si2)) < 0) ?
        ((si1)) :
    
    
        (si1 - si2);
    }
    
    static int64_t
    (safe_mul_func_int64_t_s_s)(int64_t si1, int64_t si2)
    {
      return
    
    
        (((si1 > 0) && (si2 > 0) && (si1 > ((9223372036854775807LL) / si2))) || ((si1 > 0) && (si2 <= 0) && (si2 < ((-9223372036854775807LL -1) / si1))) || ((si1 <= 0) && (si2 > 0) && (si1 < ((-9223372036854775807LL -1) / si2))) || ((si1 <= 0) && (si2 <= 0) && (si1 != 0) && (si2 < ((9223372036854775807LL) / si1)))) ?
        ((si1)) :
    
    
        si1 * si2;
    }
    
    static int64_t
    (safe_mod_func_int64_t_s_s)(int64_t si1, int64_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-9223372036854775807LL -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 % si2);
    }
    
    static int64_t
    (safe_div_func_int64_t_s_s)(int64_t si1, int64_t si2)
    {
      return
    
        ((si2 == 0) || ((si1 == (-9223372036854775807LL -1)) && (si2 == (-1)))) ?
        ((si1)) :
    
        (si1 / si2);
    }
    
    static int64_t
    (safe_lshift_func_int64_t_s_s)(int64_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32) || (left > ((9223372036854775807LL) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static int64_t
    (safe_lshift_func_int64_t_s_u)(int64_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32) || (left > ((9223372036854775807LL) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static int64_t
    (safe_rshift_func_int64_t_s_s)(int64_t left, int right)
    {
      return
    
        ((left < 0) || (((int)right) < 0) || (((int)right) >= 32))?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static int64_t
    (safe_rshift_func_int64_t_s_u)(int64_t left, unsigned int right)
    {
      return
    
        ((left < 0) || (((unsigned int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    
    
    
    
    static uint8_t
    (safe_unary_minus_func_uint8_t_u)(uint8_t ui)
    {
      return -ui;
    }
    
    static uint8_t
    (safe_add_func_uint8_t_u_u)(uint8_t ui1, uint8_t ui2)
    {
      return ui1 + ui2;
    }
    
    static uint8_t
    (safe_sub_func_uint8_t_u_u)(uint8_t ui1, uint8_t ui2)
    {
      return ui1 - ui2;
    }
    
    static uint8_t
    (safe_mul_func_uint8_t_u_u)(uint8_t ui1, uint8_t ui2)
    {
      return ((unsigned int)ui1) * ((unsigned int)ui2);
    }
    
    static uint8_t
    (safe_mod_func_uint8_t_u_u)(uint8_t ui1, uint8_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 % ui2);
    }
    
    static uint8_t
    (safe_div_func_uint8_t_u_u)(uint8_t ui1, uint8_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 / ui2);
    }
    
    static uint8_t
    (safe_lshift_func_uint8_t_u_s)(uint8_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32) || (left > ((255) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static uint8_t
    (safe_lshift_func_uint8_t_u_u)(uint8_t left, unsigned int right)
    {
      return
    
        ((((unsigned int)right) >= 32) || (left > ((255) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static uint8_t
    (safe_rshift_func_uint8_t_u_s)(uint8_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static uint8_t
    (safe_rshift_func_uint8_t_u_u)(uint8_t left, unsigned int right)
    {
      return
    
        (((unsigned int)right) >= 32) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    static uint16_t
    (safe_unary_minus_func_uint16_t_u)(uint16_t ui)
    {
      return -ui;
    }
    
    static uint16_t
    (safe_add_func_uint16_t_u_u)(uint16_t ui1, uint16_t ui2)
    {
      return ui1 + ui2;
    }
    
    static uint16_t
    (safe_sub_func_uint16_t_u_u)(uint16_t ui1, uint16_t ui2)
    {
      return ui1 - ui2;
    }
    
    static uint16_t
    (safe_mul_func_uint16_t_u_u)(uint16_t ui1, uint16_t ui2)
    {
      return ((unsigned int)ui1) * ((unsigned int)ui2);
    }
    
    static uint16_t
    (safe_mod_func_uint16_t_u_u)(uint16_t ui1, uint16_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 % ui2);
    }
    
    static uint16_t
    (safe_div_func_uint16_t_u_u)(uint16_t ui1, uint16_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 / ui2);
    }
    
    static uint16_t
    (safe_lshift_func_uint16_t_u_s)(uint16_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32) || (left > ((65535) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static uint16_t
    (safe_lshift_func_uint16_t_u_u)(uint16_t left, unsigned int right)
    {
      return
    
        ((((unsigned int)right) >= 32) || (left > ((65535) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static uint16_t
    (safe_rshift_func_uint16_t_u_s)(uint16_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static uint16_t
    (safe_rshift_func_uint16_t_u_u)(uint16_t left, unsigned int right)
    {
      return
    
        (((unsigned int)right) >= 32) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    static uint32_t
    (safe_unary_minus_func_uint32_t_u)(uint32_t ui)
    {
      return -ui;
    }
    
    static uint32_t
    (safe_add_func_uint32_t_u_u)(uint32_t ui1, uint32_t ui2)
    {
      return ui1 + ui2;
    }
    
    static uint32_t
    (safe_sub_func_uint32_t_u_u)(uint32_t ui1, uint32_t ui2)
    {
      return ui1 - ui2;
    }
    
    static uint32_t
    (safe_mul_func_uint32_t_u_u)(uint32_t ui1, uint32_t ui2)
    {
      return ((unsigned int)ui1) * ((unsigned int)ui2);
    }
    
    static uint32_t
    (safe_mod_func_uint32_t_u_u)(uint32_t ui1, uint32_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 % ui2);
    }
    
    static uint32_t
    (safe_div_func_uint32_t_u_u)(uint32_t ui1, uint32_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 / ui2);
    }
    
    static uint32_t
    (safe_lshift_func_uint32_t_u_s)(uint32_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32) || (left > ((4294967295U) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static uint32_t
    (safe_lshift_func_uint32_t_u_u)(uint32_t left, unsigned int right)
    {
      return
    
        ((((unsigned int)right) >= 32) || (left > ((4294967295U) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static uint32_t
    (safe_rshift_func_uint32_t_u_s)(uint32_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static uint32_t
    (safe_rshift_func_uint32_t_u_u)(uint32_t left, unsigned int right)
    {
      return
    
        (((unsigned int)right) >= 32) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    
    
    
    
    static uint64_t
    (safe_unary_minus_func_uint64_t_u)(uint64_t ui)
    {
      return -ui;
    }
    
    static uint64_t
    (safe_add_func_uint64_t_u_u)(uint64_t ui1, uint64_t ui2)
    {
      return ui1 + ui2;
    }
    
    static uint64_t
    (safe_sub_func_uint64_t_u_u)(uint64_t ui1, uint64_t ui2)
    {
      return ui1 - ui2;
    }
    
    static uint64_t
    (safe_mul_func_uint64_t_u_u)(uint64_t ui1, uint64_t ui2)
    {
      return ((unsigned long long int)ui1) * ((unsigned long long int)ui2);
    }
    
    static uint64_t
    (safe_mod_func_uint64_t_u_u)(uint64_t ui1, uint64_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 % ui2);
    }
    
    static uint64_t
    (safe_div_func_uint64_t_u_u)(uint64_t ui1, uint64_t ui2)
    {
      return
    
        (ui2 == 0) ?
        ((ui1)) :
    
        (ui1 / ui2);
    }
    
    static uint64_t
    (safe_lshift_func_uint64_t_u_s)(uint64_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32) || (left > ((18446744073709551615ULL) >> ((int)right)))) ?
        ((left)) :
    
        (left << ((int)right));
    }
    
    static uint64_t
    (safe_lshift_func_uint64_t_u_u)(uint64_t left, unsigned int right)
    {
      return
    
        ((((unsigned int)right) >= 32) || (left > ((18446744073709551615ULL) >> ((unsigned int)right)))) ?
        ((left)) :
    
        (left << ((unsigned int)right));
    }
    
    static uint64_t
    (safe_rshift_func_uint64_t_u_s)(uint64_t left, int right)
    {
      return
    
        ((((int)right) < 0) || (((int)right) >= 32)) ?
        ((left)) :
    
        (left >> ((int)right));
    }
    
    static uint64_t
    (safe_rshift_func_uint64_t_u_u)(uint64_t left, unsigned int right)
    {
      return
    
        (((unsigned int)right) >= 32) ?
        ((left)) :
    
        (left >> ((unsigned int)right));
    }
    # 97 "/mnt/z/csmith/runtime/random_inc.h" 2
    # 11 "foo.c" 2
    
    volatile uint64_t csmith_sink_ = 0;
    
    long __undefined;
    
    
    struct S0 {
       int8_t f0;
       int16_t f1;
       int64_t f2;
       uint16_t f3;
       int8_t f4;
       int32_t f5;
       int16_t f6;
       int32_t f7;
       int16_t f8;
    };
    
    struct S2 {
       int8_t f0;
        const int16_t f1;
       int16_t f2;
       int32_t f3;
       uint8_t f4;
       struct S0 f5;
       int64_t f6;
       int8_t f7;
       int16_t f8;
    };
    
    struct S1 {
       int32_t f0;
       uint8_t f1;
    };
    
    struct S3 {
       struct S2 f0;
        const uint32_t f1;
        const uint32_t f2;
       int64_t f3;
       struct S0 f4;
        const struct S1 f5;
       int8_t f6;
        const int8_t f7;
    };
    
    
    struct S0 g_3 = {-1L,0x4B54L,6L,7L,0xFFL,1L,-10L,0x67457993L,0x3C7DL};
    struct S3 g_8 = {{0xD5L,-10L,0L,0x900B0881L,0xDAL,{0xDBL,0x846BL,1L,-7L,0xF3L,0xFC0336AEL,6L,0x52E4A6B2L,0x4EB0L},0x117216709E149CFFLL,0x9CL,-1L},0x1636717BL,-4L,4L,{0xE3L,0xECDCL,0xF1FA6F63EEDA781BLL,0xF7A0L,0x7CL,0L,0xA77DL,0x7FC7DF39L,0x3C5AL},{0xA104ACD6L,0xA8L},0xADL,8L};
    
    
    
    struct S3 func_1(void);
    # 72 "foo.c"
    struct S3 func_1(void)
    {
        struct S0 l_2 = {0x2AL,-9L,0x26EC17E5C285CE96LL,0x779CL,0L,1L,0x58F9L,0x25B054DBL,0xE568L};
        g_3 = l_2;
        g_3.f7 = (safe_sub_func_uint32_t_u_u (g_3.f6, (safe_mul_func_int8_t_s_s (l_2.f7, l_2.f3))));
        return g_8;
    }
    
    
    
    
    
    int main()
    {
        int print_hash_value = 0;
        platform_main_begin();
        func_1();
        csmith_sink_ = g_3.f0;
        csmith_sink_ = g_3.f1;
        csmith_sink_ = g_3.f2;
        csmith_sink_ = g_3.f3;
        csmith_sink_ = g_3.f4;
        csmith_sink_ = g_3.f5;
        csmith_sink_ = g_3.f6;
        csmith_sink_ = g_3.f7;
        csmith_sink_ = g_3.f8;
        csmith_sink_ = g_8.f0.f0;
        csmith_sink_ = g_8.f0.f1;
        csmith_sink_ = g_8.f0.f2;
        csmith_sink_ = g_8.f0.f3;
        csmith_sink_ = g_8.f0.f4;
        csmith_sink_ = g_8.f0.f5.f0;
        csmith_sink_ = g_8.f0.f5.f1;
        csmith_sink_ = g_8.f0.f5.f2;
        csmith_sink_ = g_8.f0.f5.f3;
        csmith_sink_ = g_8.f0.f5.f4;
        csmith_sink_ = g_8.f0.f5.f5;
        csmith_sink_ = g_8.f0.f5.f6;
        csmith_sink_ = g_8.f0.f5.f7;
        csmith_sink_ = g_8.f0.f5.f8;
        csmith_sink_ = g_8.f0.f6;
        csmith_sink_ = g_8.f0.f7;
        csmith_sink_ = g_8.f0.f8;
        csmith_sink_ = g_8.f1;
        csmith_sink_ = g_8.f2;
        csmith_sink_ = g_8.f3;
        csmith_sink_ = g_8.f4.f0;
        csmith_sink_ = g_8.f4.f1;
        csmith_sink_ = g_8.f4.f2;
        csmith_sink_ = g_8.f4.f3;
        csmith_sink_ = g_8.f4.f4;
        csmith_sink_ = g_8.f4.f5;
        csmith_sink_ = g_8.f4.f6;
        csmith_sink_ = g_8.f4.f7;
        csmith_sink_ = g_8.f4.f8;
        csmith_sink_ = g_8.f5.f0;
        csmith_sink_ = g_8.f5.f1;
        csmith_sink_ = g_8.f6;
        csmith_sink_ = g_8.f7;
        platform_main_end(0);
        printf ("%d\n", *(unsigned char*)((unsigned char*)&g_8+30));
        return 0;
    }
    
    c file icon foo_pp.c (38,138 bytes) 2011-02-12 20:05 +

-Relationships
+Relationships

-Notes

~0001480

regehr (reporter)

Forgot to say this is seen in r11865

~0001481

pascal (reporter)

The field at offset 30 is g_8.f0.f5.f4. This should indeed contain 243, or 0xF3L. g_8 is not even modified during execution.

~0004835

pascal (reporter)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2011-02-12 20:05 regehr New Issue
2011-02-12 20:05 regehr Status new => assigned
2011-02-12 20:05 regehr Assigned To => pascal
2011-02-12 20:05 regehr File Added: foo_pp.c
2011-02-12 20:22 regehr Note Added: 0001480
2011-02-12 20:39 pascal Note Added: 0001481
2011-02-12 20:39 pascal Status assigned => confirmed
2011-02-12 22:01 svn
2011-02-12 22:01 svn Status confirmed => resolved
2011-02-12 22:01 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 pascal Source_changeset_attached => framac master 958171cd
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon 958171cd
2014-02-12 16:59 pascal Note Added: 0004835
2014-02-12 16:59 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History