Showing error 1368

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/fo_test.c_unsafe.i
Line in file: 1077
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1# 1 "files/fo_test.c"
   2# 1 "<built-in>"
   3# 1 "<command-line>"
   4# 1 "files/fo_test.c"
   5# 1 "/usr/include/stdlib.h" 1 3 4
   6# 25 "/usr/include/stdlib.h" 3 4
   7# 1 "/usr/include/features.h" 1 3 4
   8# 347 "/usr/include/features.h" 3 4
   9# 1 "/usr/include/sys/cdefs.h" 1 3 4
  10# 353 "/usr/include/sys/cdefs.h" 3 4
  11# 1 "/usr/include/bits/wordsize.h" 1 3 4
  12# 354 "/usr/include/sys/cdefs.h" 2 3 4
  13# 348 "/usr/include/features.h" 2 3 4
  14# 371 "/usr/include/features.h" 3 4
  15# 1 "/usr/include/gnu/stubs.h" 1 3 4
  16
  17
  18
  19# 1 "/usr/include/bits/wordsize.h" 1 3 4
  20# 5 "/usr/include/gnu/stubs.h" 2 3 4
  21
  22
  23
  24
  25# 1 "/usr/include/gnu/stubs-64.h" 1 3 4
  26# 10 "/usr/include/gnu/stubs.h" 2 3 4
  27# 372 "/usr/include/features.h" 2 3 4
  28# 26 "/usr/include/stdlib.h" 2 3 4
  29
  30
  31
  32
  33
  34
  35
  36# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 1 3 4
  37# 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 3 4
  38typedef long unsigned int size_t;
  39# 323 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 3 4
  40typedef int wchar_t;
  41# 34 "/usr/include/stdlib.h" 2 3 4
  42
  43
  44# 96 "/usr/include/stdlib.h" 3 4
  45
  46
  47typedef struct
  48  {
  49    int quot;
  50    int rem;
  51  } div_t;
  52
  53
  54
  55typedef struct
  56  {
  57    long int quot;
  58    long int rem;
  59  } ldiv_t;
  60
  61
  62
  63
  64
  65
  66
  67__extension__ typedef struct
  68  {
  69    long long int quot;
  70    long long int rem;
  71  } lldiv_t;
  72
  73
  74# 140 "/usr/include/stdlib.h" 3 4
  75extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__)) ;
  76
  77
  78
  79
  80extern double atof (__const char *__nptr)
  81     __attribute__ ((__nothrow__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
  82
  83extern int atoi (__const char *__nptr)
  84     __attribute__ ((__nothrow__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
  85
  86extern long int atol (__const char *__nptr)
  87     __attribute__ ((__nothrow__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
  88
  89
  90
  91
  92
  93__extension__ extern long long int atoll (__const char *__nptr)
  94     __attribute__ ((__nothrow__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
  95
  96
  97
  98
  99
 100extern double strtod (__const char *__restrict __nptr,
 101        char **__restrict __endptr)
 102     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 103
 104
 105
 106
 107
 108extern float strtof (__const char *__restrict __nptr,
 109       char **__restrict __endptr) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 110
 111extern long double strtold (__const char *__restrict __nptr,
 112       char **__restrict __endptr)
 113     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 114
 115
 116
 117
 118
 119extern long int strtol (__const char *__restrict __nptr,
 120   char **__restrict __endptr, int __base)
 121     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 122
 123extern unsigned long int strtoul (__const char *__restrict __nptr,
 124      char **__restrict __endptr, int __base)
 125     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 126
 127
 128
 129
 130__extension__
 131extern long long int strtoq (__const char *__restrict __nptr,
 132        char **__restrict __endptr, int __base)
 133     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 134
 135__extension__
 136extern unsigned long long int strtouq (__const char *__restrict __nptr,
 137           char **__restrict __endptr, int __base)
 138     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 139
 140
 141
 142
 143
 144__extension__
 145extern long long int strtoll (__const char *__restrict __nptr,
 146         char **__restrict __endptr, int __base)
 147     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 148
 149__extension__
 150extern unsigned long long int strtoull (__const char *__restrict __nptr,
 151     char **__restrict __endptr, int __base)
 152     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 153
 154# 311 "/usr/include/stdlib.h" 3 4
 155extern char *l64a (long int __n) __attribute__ ((__nothrow__)) ;
 156
 157
 158extern long int a64l (__const char *__s)
 159     __attribute__ ((__nothrow__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;
 160
 161
 162
 163
 164# 1 "/usr/include/sys/types.h" 1 3 4
 165# 29 "/usr/include/sys/types.h" 3 4
 166
 167
 168# 1 "/usr/include/bits/types.h" 1 3 4
 169# 28 "/usr/include/bits/types.h" 3 4
 170# 1 "/usr/include/bits/wordsize.h" 1 3 4
 171# 29 "/usr/include/bits/types.h" 2 3 4
 172
 173
 174typedef unsigned char __u_char;
 175typedef unsigned short int __u_short;
 176typedef unsigned int __u_int;
 177typedef unsigned long int __u_long;
 178
 179
 180typedef signed char __int8_t;
 181typedef unsigned char __uint8_t;
 182typedef signed short int __int16_t;
 183typedef unsigned short int __uint16_t;
 184typedef signed int __int32_t;
 185typedef unsigned int __uint32_t;
 186
 187typedef signed long int __int64_t;
 188typedef unsigned long int __uint64_t;
 189
 190
 191
 192
 193
 194
 195
 196typedef long int __quad_t;
 197typedef unsigned long int __u_quad_t;
 198# 131 "/usr/include/bits/types.h" 3 4
 199# 1 "/usr/include/bits/typesizes.h" 1 3 4
 200# 132 "/usr/include/bits/types.h" 2 3 4
 201
 202
 203typedef unsigned long int __dev_t;
 204typedef unsigned int __uid_t;
 205typedef unsigned int __gid_t;
 206typedef unsigned long int __ino_t;
 207typedef unsigned long int __ino64_t;
 208typedef unsigned int __mode_t;
 209typedef unsigned long int __nlink_t;
 210typedef long int __off_t;
 211typedef long int __off64_t;
 212typedef int __pid_t;
 213typedef struct { int __val[2]; } __fsid_t;
 214typedef long int __clock_t;
 215typedef unsigned long int __rlim_t;
 216typedef unsigned long int __rlim64_t;
 217typedef unsigned int __id_t;
 218typedef long int __time_t;
 219typedef unsigned int __useconds_t;
 220typedef long int __suseconds_t;
 221
 222typedef int __daddr_t;
 223typedef long int __swblk_t;
 224typedef int __key_t;
 225
 226
 227typedef int __clockid_t;
 228
 229
 230typedef void * __timer_t;
 231
 232
 233typedef long int __blksize_t;
 234
 235
 236
 237
 238typedef long int __blkcnt_t;
 239typedef long int __blkcnt64_t;
 240
 241
 242typedef unsigned long int __fsblkcnt_t;
 243typedef unsigned long int __fsblkcnt64_t;
 244
 245
 246typedef unsigned long int __fsfilcnt_t;
 247typedef unsigned long int __fsfilcnt64_t;
 248
 249typedef long int __ssize_t;
 250
 251
 252
 253typedef __off64_t __loff_t;
 254typedef __quad_t *__qaddr_t;
 255typedef char *__caddr_t;
 256
 257
 258typedef long int __intptr_t;
 259
 260
 261typedef unsigned int __socklen_t;
 262# 32 "/usr/include/sys/types.h" 2 3 4
 263
 264
 265
 266typedef __u_char u_char;
 267typedef __u_short u_short;
 268typedef __u_int u_int;
 269typedef __u_long u_long;
 270typedef __quad_t quad_t;
 271typedef __u_quad_t u_quad_t;
 272typedef __fsid_t fsid_t;
 273
 274
 275
 276
 277typedef __loff_t loff_t;
 278
 279
 280
 281typedef __ino_t ino_t;
 282# 62 "/usr/include/sys/types.h" 3 4
 283typedef __dev_t dev_t;
 284
 285
 286
 287
 288typedef __gid_t gid_t;
 289
 290
 291
 292
 293typedef __mode_t mode_t;
 294
 295
 296
 297
 298typedef __nlink_t nlink_t;
 299
 300
 301
 302
 303typedef __uid_t uid_t;
 304
 305
 306
 307
 308
 309typedef __off_t off_t;
 310# 100 "/usr/include/sys/types.h" 3 4
 311typedef __pid_t pid_t;
 312
 313
 314
 315
 316typedef __id_t id_t;
 317
 318
 319
 320
 321typedef __ssize_t ssize_t;
 322
 323
 324
 325
 326
 327typedef __daddr_t daddr_t;
 328typedef __caddr_t caddr_t;
 329
 330
 331
 332
 333
 334typedef __key_t key_t;
 335# 133 "/usr/include/sys/types.h" 3 4
 336# 1 "/usr/include/time.h" 1 3 4
 337# 74 "/usr/include/time.h" 3 4
 338
 339
 340typedef __time_t time_t;
 341
 342
 343
 344# 92 "/usr/include/time.h" 3 4
 345typedef __clockid_t clockid_t;
 346# 104 "/usr/include/time.h" 3 4
 347typedef __timer_t timer_t;
 348# 134 "/usr/include/sys/types.h" 2 3 4
 349# 147 "/usr/include/sys/types.h" 3 4
 350# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 1 3 4
 351# 148 "/usr/include/sys/types.h" 2 3 4
 352
 353
 354
 355typedef unsigned long int ulong;
 356typedef unsigned short int ushort;
 357typedef unsigned int uint;
 358# 195 "/usr/include/sys/types.h" 3 4
 359typedef int int8_t __attribute__ ((__mode__ (__QI__)));
 360typedef int int16_t __attribute__ ((__mode__ (__HI__)));
 361typedef int int32_t __attribute__ ((__mode__ (__SI__)));
 362typedef int int64_t __attribute__ ((__mode__ (__DI__)));
 363
 364
 365typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));
 366typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));
 367typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));
 368typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));
 369
 370typedef int register_t __attribute__ ((__mode__ (__word__)));
 371# 217 "/usr/include/sys/types.h" 3 4
 372# 1 "/usr/include/endian.h" 1 3 4
 373# 37 "/usr/include/endian.h" 3 4
 374# 1 "/usr/include/bits/endian.h" 1 3 4
 375# 38 "/usr/include/endian.h" 2 3 4
 376# 61 "/usr/include/endian.h" 3 4
 377# 1 "/usr/include/bits/byteswap.h" 1 3 4
 378# 28 "/usr/include/bits/byteswap.h" 3 4
 379# 1 "/usr/include/bits/wordsize.h" 1 3 4
 380# 29 "/usr/include/bits/byteswap.h" 2 3 4
 381# 62 "/usr/include/endian.h" 2 3 4
 382# 218 "/usr/include/sys/types.h" 2 3 4
 383
 384
 385# 1 "/usr/include/sys/select.h" 1 3 4
 386# 31 "/usr/include/sys/select.h" 3 4
 387# 1 "/usr/include/bits/select.h" 1 3 4
 388# 23 "/usr/include/bits/select.h" 3 4
 389# 1 "/usr/include/bits/wordsize.h" 1 3 4
 390# 24 "/usr/include/bits/select.h" 2 3 4
 391# 32 "/usr/include/sys/select.h" 2 3 4
 392
 393
 394# 1 "/usr/include/bits/sigset.h" 1 3 4
 395# 24 "/usr/include/bits/sigset.h" 3 4
 396typedef int __sig_atomic_t;
 397
 398
 399
 400
 401typedef struct
 402  {
 403    unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];
 404  } __sigset_t;
 405# 35 "/usr/include/sys/select.h" 2 3 4
 406
 407
 408
 409typedef __sigset_t sigset_t;
 410
 411
 412
 413
 414
 415# 1 "/usr/include/time.h" 1 3 4
 416# 120 "/usr/include/time.h" 3 4
 417struct timespec
 418  {
 419    __time_t tv_sec;
 420    long int tv_nsec;
 421  };
 422# 45 "/usr/include/sys/select.h" 2 3 4
 423
 424# 1 "/usr/include/bits/time.h" 1 3 4
 425# 69 "/usr/include/bits/time.h" 3 4
 426struct timeval
 427  {
 428    __time_t tv_sec;
 429    __suseconds_t tv_usec;
 430  };
 431# 47 "/usr/include/sys/select.h" 2 3 4
 432
 433
 434typedef __suseconds_t suseconds_t;
 435
 436
 437
 438
 439
 440typedef long int __fd_mask;
 441# 67 "/usr/include/sys/select.h" 3 4
 442typedef struct
 443  {
 444
 445
 446
 447
 448
 449
 450    __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];
 451
 452
 453  } fd_set;
 454
 455
 456
 457
 458
 459
 460typedef __fd_mask fd_mask;
 461# 99 "/usr/include/sys/select.h" 3 4
 462
 463# 109 "/usr/include/sys/select.h" 3 4
 464extern int select (int __nfds, fd_set *__restrict __readfds,
 465     fd_set *__restrict __writefds,
 466     fd_set *__restrict __exceptfds,
 467     struct timeval *__restrict __timeout);
 468# 121 "/usr/include/sys/select.h" 3 4
 469extern int pselect (int __nfds, fd_set *__restrict __readfds,
 470      fd_set *__restrict __writefds,
 471      fd_set *__restrict __exceptfds,
 472      const struct timespec *__restrict __timeout,
 473      const __sigset_t *__restrict __sigmask);
 474
 475
 476
 477# 221 "/usr/include/sys/types.h" 2 3 4
 478
 479
 480# 1 "/usr/include/sys/sysmacros.h" 1 3 4
 481# 30 "/usr/include/sys/sysmacros.h" 3 4
 482__extension__
 483extern unsigned int gnu_dev_major (unsigned long long int __dev)
 484     __attribute__ ((__nothrow__));
 485__extension__
 486extern unsigned int gnu_dev_minor (unsigned long long int __dev)
 487     __attribute__ ((__nothrow__));
 488__extension__
 489extern unsigned long long int gnu_dev_makedev (unsigned int __major,
 490            unsigned int __minor)
 491     __attribute__ ((__nothrow__));
 492# 224 "/usr/include/sys/types.h" 2 3 4
 493# 235 "/usr/include/sys/types.h" 3 4
 494typedef __blkcnt_t blkcnt_t;
 495
 496
 497
 498typedef __fsblkcnt_t fsblkcnt_t;
 499
 500
 501
 502typedef __fsfilcnt_t fsfilcnt_t;
 503# 270 "/usr/include/sys/types.h" 3 4
 504# 1 "/usr/include/bits/pthreadtypes.h" 1 3 4
 505# 23 "/usr/include/bits/pthreadtypes.h" 3 4
 506# 1 "/usr/include/bits/wordsize.h" 1 3 4
 507# 24 "/usr/include/bits/pthreadtypes.h" 2 3 4
 508# 50 "/usr/include/bits/pthreadtypes.h" 3 4
 509typedef unsigned long int pthread_t;
 510
 511
 512typedef union
 513{
 514  char __size[56];
 515  long int __align;
 516} pthread_attr_t;
 517
 518
 519
 520typedef struct __pthread_internal_list
 521{
 522  struct __pthread_internal_list *__prev;
 523  struct __pthread_internal_list *__next;
 524} __pthread_list_t;
 525# 76 "/usr/include/bits/pthreadtypes.h" 3 4
 526typedef union
 527{
 528  struct __pthread_mutex_s
 529  {
 530    int __lock;
 531    unsigned int __count;
 532    int __owner;
 533
 534    unsigned int __nusers;
 535
 536
 537
 538    int __kind;
 539
 540    int __spins;
 541    __pthread_list_t __list;
 542# 101 "/usr/include/bits/pthreadtypes.h" 3 4
 543  } __data;
 544  char __size[40];
 545  long int __align;
 546} pthread_mutex_t;
 547
 548typedef union
 549{
 550  char __size[4];
 551  int __align;
 552} pthread_mutexattr_t;
 553
 554
 555
 556
 557typedef union
 558{
 559  struct
 560  {
 561    int __lock;
 562    unsigned int __futex;
 563    __extension__ unsigned long long int __total_seq;
 564    __extension__ unsigned long long int __wakeup_seq;
 565    __extension__ unsigned long long int __woken_seq;
 566    void *__mutex;
 567    unsigned int __nwaiters;
 568    unsigned int __broadcast_seq;
 569  } __data;
 570  char __size[48];
 571  __extension__ long long int __align;
 572} pthread_cond_t;
 573
 574typedef union
 575{
 576  char __size[4];
 577  int __align;
 578} pthread_condattr_t;
 579
 580
 581
 582typedef unsigned int pthread_key_t;
 583
 584
 585
 586typedef int pthread_once_t;
 587
 588
 589
 590
 591
 592typedef union
 593{
 594
 595  struct
 596  {
 597    int __lock;
 598    unsigned int __nr_readers;
 599    unsigned int __readers_wakeup;
 600    unsigned int __writer_wakeup;
 601    unsigned int __nr_readers_queued;
 602    unsigned int __nr_writers_queued;
 603    int __writer;
 604    int __shared;
 605    unsigned long int __pad1;
 606    unsigned long int __pad2;
 607
 608
 609    unsigned int __flags;
 610  } __data;
 611# 187 "/usr/include/bits/pthreadtypes.h" 3 4
 612  char __size[56];
 613  long int __align;
 614} pthread_rwlock_t;
 615
 616typedef union
 617{
 618  char __size[8];
 619  long int __align;
 620} pthread_rwlockattr_t;
 621
 622
 623
 624
 625
 626typedef volatile int pthread_spinlock_t;
 627
 628
 629
 630
 631typedef union
 632{
 633  char __size[32];
 634  long int __align;
 635} pthread_barrier_t;
 636
 637typedef union
 638{
 639  char __size[4];
 640  int __align;
 641} pthread_barrierattr_t;
 642# 271 "/usr/include/sys/types.h" 2 3 4
 643
 644
 645
 646# 321 "/usr/include/stdlib.h" 2 3 4
 647
 648
 649
 650
 651
 652
 653extern long int random (void) __attribute__ ((__nothrow__));
 654
 655
 656extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__));
 657
 658
 659
 660
 661
 662extern char *initstate (unsigned int __seed, char *__statebuf,
 663   size_t __statelen) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
 664
 665
 666
 667extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 668
 669
 670
 671
 672
 673
 674
 675struct random_data
 676  {
 677    int32_t *fptr;
 678    int32_t *rptr;
 679    int32_t *state;
 680    int rand_type;
 681    int rand_deg;
 682    int rand_sep;
 683    int32_t *end_ptr;
 684  };
 685
 686extern int random_r (struct random_data *__restrict __buf,
 687       int32_t *__restrict __result) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 688
 689extern int srandom_r (unsigned int __seed, struct random_data *__buf)
 690     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
 691
 692extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,
 693   size_t __statelen,
 694   struct random_data *__restrict __buf)
 695     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 4)));
 696
 697extern int setstate_r (char *__restrict __statebuf,
 698         struct random_data *__restrict __buf)
 699     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 700
 701
 702
 703
 704
 705
 706extern int rand (void) __attribute__ ((__nothrow__));
 707
 708extern void srand (unsigned int __seed) __attribute__ ((__nothrow__));
 709
 710
 711
 712
 713extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__));
 714
 715
 716
 717
 718
 719
 720
 721extern double drand48 (void) __attribute__ ((__nothrow__));
 722extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 723
 724
 725extern long int lrand48 (void) __attribute__ ((__nothrow__));
 726extern long int nrand48 (unsigned short int __xsubi[3])
 727     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 728
 729
 730extern long int mrand48 (void) __attribute__ ((__nothrow__));
 731extern long int jrand48 (unsigned short int __xsubi[3])
 732     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 733
 734
 735extern void srand48 (long int __seedval) __attribute__ ((__nothrow__));
 736extern unsigned short int *seed48 (unsigned short int __seed16v[3])
 737     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 738extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 739
 740
 741
 742
 743
 744struct drand48_data
 745  {
 746    unsigned short int __x[3];
 747    unsigned short int __old_x[3];
 748    unsigned short int __c;
 749    unsigned short int __init;
 750    unsigned long long int __a;
 751  };
 752
 753
 754extern int drand48_r (struct drand48_data *__restrict __buffer,
 755        double *__restrict __result) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 756extern int erand48_r (unsigned short int __xsubi[3],
 757        struct drand48_data *__restrict __buffer,
 758        double *__restrict __result) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 759
 760
 761extern int lrand48_r (struct drand48_data *__restrict __buffer,
 762        long int *__restrict __result)
 763     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 764extern int nrand48_r (unsigned short int __xsubi[3],
 765        struct drand48_data *__restrict __buffer,
 766        long int *__restrict __result)
 767     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 768
 769
 770extern int mrand48_r (struct drand48_data *__restrict __buffer,
 771        long int *__restrict __result)
 772     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 773extern int jrand48_r (unsigned short int __xsubi[3],
 774        struct drand48_data *__restrict __buffer,
 775        long int *__restrict __result)
 776     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 777
 778
 779extern int srand48_r (long int __seedval, struct drand48_data *__buffer)
 780     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
 781
 782extern int seed48_r (unsigned short int __seed16v[3],
 783       struct drand48_data *__buffer) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 784
 785extern int lcong48_r (unsigned short int __param[7],
 786        struct drand48_data *__buffer)
 787     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
 788
 789
 790
 791
 792
 793
 794
 795
 796
 797extern void *malloc (size_t __size) __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
 798
 799extern void *calloc (size_t __nmemb, size_t __size)
 800     __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
 801
 802
 803
 804
 805
 806
 807
 808
 809
 810
 811extern void *realloc (void *__ptr, size_t __size)
 812     __attribute__ ((__nothrow__)) __attribute__ ((__warn_unused_result__));
 813
 814extern void free (void *__ptr) __attribute__ ((__nothrow__));
 815
 816
 817
 818
 819extern void cfree (void *__ptr) __attribute__ ((__nothrow__));
 820
 821
 822
 823# 1 "/usr/include/alloca.h" 1 3 4
 824# 25 "/usr/include/alloca.h" 3 4
 825# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 1 3 4
 826# 26 "/usr/include/alloca.h" 2 3 4
 827
 828
 829
 830
 831
 832
 833
 834extern void *alloca (size_t __size) __attribute__ ((__nothrow__));
 835
 836
 837
 838
 839
 840
 841# 498 "/usr/include/stdlib.h" 2 3 4
 842
 843
 844
 845
 846extern void *valloc (size_t __size) __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
 847
 848
 849
 850
 851extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)
 852     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 853
 854
 855
 856
 857extern void abort (void) __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
 858
 859
 860
 861extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 862# 530 "/usr/include/stdlib.h" 3 4
 863
 864
 865
 866
 867
 868extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)
 869     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 870
 871
 872
 873
 874
 875
 876extern void exit (int __status) __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
 877# 553 "/usr/include/stdlib.h" 3 4
 878
 879
 880
 881
 882
 883
 884extern void _Exit (int __status) __attribute__ ((__nothrow__)) __attribute__ ((__noreturn__));
 885
 886
 887
 888
 889
 890
 891extern char *getenv (__const char *__name) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 892
 893
 894
 895
 896extern char *__secure_getenv (__const char *__name)
 897     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 898
 899
 900
 901
 902
 903extern int putenv (char *__string) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
 904
 905
 906
 907
 908
 909extern int setenv (__const char *__name, __const char *__value, int __replace)
 910     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
 911
 912
 913extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__));
 914
 915
 916
 917
 918
 919
 920extern int clearenv (void) __attribute__ ((__nothrow__));
 921# 604 "/usr/include/stdlib.h" 3 4
 922extern char *mktemp (char *__template) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 923# 615 "/usr/include/stdlib.h" 3 4
 924extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;
 925# 637 "/usr/include/stdlib.h" 3 4
 926extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;
 927# 658 "/usr/include/stdlib.h" 3 4
 928extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
 929# 707 "/usr/include/stdlib.h" 3 4
 930
 931
 932
 933
 934
 935extern int system (__const char *__command) ;
 936
 937# 729 "/usr/include/stdlib.h" 3 4
 938extern char *realpath (__const char *__restrict __name,
 939         char *__restrict __resolved) __attribute__ ((__nothrow__)) ;
 940
 941
 942
 943
 944
 945
 946typedef int (*__compar_fn_t) (__const void *, __const void *);
 947# 747 "/usr/include/stdlib.h" 3 4
 948
 949
 950
 951extern void *bsearch (__const void *__key, __const void *__base,
 952        size_t __nmemb, size_t __size, __compar_fn_t __compar)
 953     __attribute__ ((__nonnull__ (1, 2, 5))) ;
 954
 955
 956
 957extern void qsort (void *__base, size_t __nmemb, size_t __size,
 958     __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));
 959# 766 "/usr/include/stdlib.h" 3 4
 960extern int abs (int __x) __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 961extern long int labs (long int __x) __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 962
 963
 964
 965__extension__ extern long long int llabs (long long int __x)
 966     __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 967
 968
 969
 970
 971
 972
 973
 974extern div_t div (int __numer, int __denom)
 975     __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 976extern ldiv_t ldiv (long int __numer, long int __denom)
 977     __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 978
 979
 980
 981
 982__extension__ extern lldiv_t lldiv (long long int __numer,
 983        long long int __denom)
 984     __attribute__ ((__nothrow__)) __attribute__ ((__const__)) ;
 985
 986# 802 "/usr/include/stdlib.h" 3 4
 987extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,
 988     int *__restrict __sign) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4))) ;
 989
 990
 991
 992
 993extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,
 994     int *__restrict __sign) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4))) ;
 995
 996
 997
 998
 999extern char *gcvt (double __value, int __ndigit, char *__buf)
1000     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3))) ;
1001
1002
1003
1004
1005extern char *qecvt (long double __value, int __ndigit,
1006      int *__restrict __decpt, int *__restrict __sign)
1007     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4))) ;
1008extern char *qfcvt (long double __value, int __ndigit,
1009      int *__restrict __decpt, int *__restrict __sign)
1010     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4))) ;
1011extern char *qgcvt (long double __value, int __ndigit, char *__buf)
1012     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3))) ;
1013
1014
1015
1016
1017extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,
1018     int *__restrict __sign, char *__restrict __buf,
1019     size_t __len) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4, 5)));
1020extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,
1021     int *__restrict __sign, char *__restrict __buf,
1022     size_t __len) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4, 5)));
1023
1024extern int qecvt_r (long double __value, int __ndigit,
1025      int *__restrict __decpt, int *__restrict __sign,
1026      char *__restrict __buf, size_t __len)
1027     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4, 5)));
1028extern int qfcvt_r (long double __value, int __ndigit,
1029      int *__restrict __decpt, int *__restrict __sign,
1030      char *__restrict __buf, size_t __len)
1031     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4, 5)));
1032
1033
1034
1035
1036
1037
1038
1039extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__)) ;
1040
1041
1042extern int mbtowc (wchar_t *__restrict __pwc,
1043     __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__)) ;
1044
1045
1046extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__)) ;
1047
1048
1049
1050extern size_t mbstowcs (wchar_t *__restrict __pwcs,
1051   __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__));
1052
1053extern size_t wcstombs (char *__restrict __s,
1054   __const wchar_t *__restrict __pwcs, size_t __n)
1055     __attribute__ ((__nothrow__));
1056
1057
1058
1059
1060
1061
1062
1063
1064extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1))) ;
1065# 907 "/usr/include/stdlib.h" 3 4
1066extern int posix_openpt (int __oflag) ;
1067# 942 "/usr/include/stdlib.h" 3 4
1068extern int getloadavg (double __loadavg[], int __nelem)
1069     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1070# 958 "/usr/include/stdlib.h" 3 4
1071
1072# 2 "files/fo_test.c" 2
1073# 1 "./assert.h" 1
1074
1075void __blast_assert()
1076{
1077 ERROR: goto ERROR;
1078}
1079# 3 "files/fo_test.c" 2
1080
1081# 1 "/usr/include/sys/stat.h" 1 3 4
1082# 39 "/usr/include/sys/stat.h" 3 4
1083# 1 "/usr/include/time.h" 1 3 4
1084# 40 "/usr/include/sys/stat.h" 2 3 4
1085# 105 "/usr/include/sys/stat.h" 3 4
1086
1087
1088# 1 "/usr/include/bits/stat.h" 1 3 4
1089# 43 "/usr/include/bits/stat.h" 3 4
1090struct stat
1091  {
1092    __dev_t st_dev;
1093
1094
1095
1096
1097    __ino_t st_ino;
1098
1099
1100
1101
1102
1103
1104
1105    __nlink_t st_nlink;
1106    __mode_t st_mode;
1107
1108    __uid_t st_uid;
1109    __gid_t st_gid;
1110
1111    int __pad0;
1112
1113    __dev_t st_rdev;
1114
1115
1116
1117
1118    __off_t st_size;
1119
1120
1121
1122    __blksize_t st_blksize;
1123
1124    __blkcnt_t st_blocks;
1125# 88 "/usr/include/bits/stat.h" 3 4
1126    struct timespec st_atim;
1127    struct timespec st_mtim;
1128    struct timespec st_ctim;
1129# 103 "/usr/include/bits/stat.h" 3 4
1130    long int __unused[3];
1131# 112 "/usr/include/bits/stat.h" 3 4
1132  };
1133# 108 "/usr/include/sys/stat.h" 2 3 4
1134# 209 "/usr/include/sys/stat.h" 3 4
1135extern int stat (__const char *__restrict __file,
1136   struct stat *__restrict __buf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
1137
1138
1139
1140extern int fstat (int __fd, struct stat *__buf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
1141# 238 "/usr/include/sys/stat.h" 3 4
1142extern int fstatat (int __fd, __const char *__restrict __file,
1143      struct stat *__restrict __buf, int __flag)
1144     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 3)));
1145# 263 "/usr/include/sys/stat.h" 3 4
1146extern int lstat (__const char *__restrict __file,
1147    struct stat *__restrict __buf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1, 2)));
1148# 284 "/usr/include/sys/stat.h" 3 4
1149extern int chmod (__const char *__file, __mode_t __mode)
1150     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1151
1152
1153
1154
1155
1156extern int lchmod (__const char *__file, __mode_t __mode)
1157     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1158
1159
1160
1161
1162extern int fchmod (int __fd, __mode_t __mode) __attribute__ ((__nothrow__));
1163
1164
1165
1166
1167
1168extern int fchmodat (int __fd, __const char *__file, __mode_t __mode,
1169       int __flag)
1170     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2))) ;
1171
1172
1173
1174
1175
1176
1177extern __mode_t umask (__mode_t __mask) __attribute__ ((__nothrow__));
1178# 321 "/usr/include/sys/stat.h" 3 4
1179extern int mkdir (__const char *__path, __mode_t __mode)
1180     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1181
1182
1183
1184
1185
1186extern int mkdirat (int __fd, __const char *__path, __mode_t __mode)
1187     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
1188
1189
1190
1191
1192
1193
1194extern int mknod (__const char *__path, __mode_t __mode, __dev_t __dev)
1195     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1196
1197
1198
1199
1200
1201extern int mknodat (int __fd, __const char *__path, __mode_t __mode,
1202      __dev_t __dev) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
1203
1204
1205
1206
1207
1208extern int mkfifo (__const char *__path, __mode_t __mode)
1209     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (1)));
1210
1211
1212
1213
1214
1215extern int mkfifoat (int __fd, __const char *__path, __mode_t __mode)
1216     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
1217
1218
1219
1220
1221
1222extern int utimensat (int __fd, __const char *__path,
1223        __const struct timespec __times[2],
1224        int __flags)
1225     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2)));
1226
1227
1228
1229
1230extern int futimens (int __fd, __const struct timespec __times[2]) __attribute__ ((__nothrow__));
1231# 399 "/usr/include/sys/stat.h" 3 4
1232extern int __fxstat (int __ver, int __fildes, struct stat *__stat_buf)
1233     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3)));
1234extern int __xstat (int __ver, __const char *__filename,
1235      struct stat *__stat_buf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 3)));
1236extern int __lxstat (int __ver, __const char *__filename,
1237       struct stat *__stat_buf) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 3)));
1238extern int __fxstatat (int __ver, int __fildes, __const char *__filename,
1239         struct stat *__stat_buf, int __flag)
1240     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 4)));
1241# 442 "/usr/include/sys/stat.h" 3 4
1242extern int __xmknod (int __ver, __const char *__path, __mode_t __mode,
1243       __dev_t *__dev) __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (2, 4)));
1244
1245extern int __xmknodat (int __ver, int __fd, __const char *__path,
1246         __mode_t __mode, __dev_t *__dev)
1247     __attribute__ ((__nothrow__)) __attribute__ ((__nonnull__ (3, 5)));
1248# 534 "/usr/include/sys/stat.h" 3 4
1249
1250# 5 "files/fo_test.c" 2
1251# 1 "/usr/include/fcntl.h" 1 3 4
1252# 30 "/usr/include/fcntl.h" 3 4
1253
1254
1255
1256
1257# 1 "/usr/include/bits/fcntl.h" 1 3 4
1258# 25 "/usr/include/bits/fcntl.h" 3 4
1259# 1 "/usr/include/bits/wordsize.h" 1 3 4
1260# 26 "/usr/include/bits/fcntl.h" 2 3 4
1261# 160 "/usr/include/bits/fcntl.h" 3 4
1262struct flock
1263  {
1264    short int l_type;
1265    short int l_whence;
1266
1267    __off_t l_start;
1268    __off_t l_len;
1269
1270
1271
1272
1273    __pid_t l_pid;
1274  };
1275# 244 "/usr/include/bits/fcntl.h" 3 4
1276
1277# 289 "/usr/include/bits/fcntl.h" 3 4
1278
1279# 35 "/usr/include/fcntl.h" 2 3 4
1280# 78 "/usr/include/fcntl.h" 3 4
1281extern int fcntl (int __fd, int __cmd, ...);
1282# 87 "/usr/include/fcntl.h" 3 4
1283extern int open (__const char *__file, int __oflag, ...) __attribute__ ((__nonnull__ (1)));
1284# 111 "/usr/include/fcntl.h" 3 4
1285extern int openat (int __fd, __const char *__file, int __oflag, ...)
1286     __attribute__ ((__nonnull__ (2)));
1287# 122 "/usr/include/fcntl.h" 3 4
1288extern int openat64 (int __fd, __const char *__file, int __oflag, ...)
1289     __attribute__ ((__nonnull__ (2)));
1290# 132 "/usr/include/fcntl.h" 3 4
1291extern int creat (__const char *__file, __mode_t __mode) __attribute__ ((__nonnull__ (1)));
1292# 161 "/usr/include/fcntl.h" 3 4
1293extern int lockf (int __fd, int __cmd, __off_t __len);
1294# 178 "/usr/include/fcntl.h" 3 4
1295extern int posix_fadvise (int __fd, __off_t __offset, __off_t __len,
1296     int __advise) __attribute__ ((__nothrow__));
1297# 200 "/usr/include/fcntl.h" 3 4
1298extern int posix_fallocate (int __fd, __off_t __offset, __off_t __len);
1299# 222 "/usr/include/fcntl.h" 3 4
1300
1301# 6 "files/fo_test.c" 2
1302
1303extern int __VERIFIER_nondet_int(void);
1304int open(char const   *__file, int __oflag, ...)
1305{
1306    return __VERIFIER_nondet_int();
1307}
1308
1309int globalState = 0;
1310ssize_t l_read(int,char*,size_t);
1311int l_open(char*,int);
1312
1313int
1314main(int argc, char* argv[]) {
1315 int file = l_open("unknown",00);
1316 void* cbuf = (void*) malloc(sizeof(char)*100);
1317 int a = l_read(file,cbuf,99);
1318 return 0;
1319}
1320
1321ssize_t l_read(int fd, char* cbuf, size_t count) {
1322 ((globalState == 1) ? (0) : __blast_assert ());
1323 return read(fd,cbuf,count);
1324}
1325
1326int l_open(char* file, int flags) {
1327 int fd = open(file,flags);
1328 if(fd>0) globalState = 1;
1329 return fd;
1330}