Showing error 1408

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/sizeofparameters_test.c_safe.i
Line in file: 840
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

  1# 1 "files/sizeofparameters_test.c"
  2# 1 "<built-in>"
  3# 1 "<command-line>"
  4# 1 "files/sizeofparameters_test.c"
  5# 1 "/usr/include/stdio.h" 1 3 4
  6# 28 "/usr/include/stdio.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# 29 "/usr/include/stdio.h" 2 3 4
 29
 30
 31
 32
 33
 34# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 1 3 4
 35# 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 3 4
 36typedef long unsigned int size_t;
 37# 35 "/usr/include/stdio.h" 2 3 4
 38
 39# 1 "/usr/include/bits/types.h" 1 3 4
 40# 28 "/usr/include/bits/types.h" 3 4
 41# 1 "/usr/include/bits/wordsize.h" 1 3 4
 42# 29 "/usr/include/bits/types.h" 2 3 4
 43
 44
 45typedef unsigned char __u_char;
 46typedef unsigned short int __u_short;
 47typedef unsigned int __u_int;
 48typedef unsigned long int __u_long;
 49
 50
 51typedef signed char __int8_t;
 52typedef unsigned char __uint8_t;
 53typedef signed short int __int16_t;
 54typedef unsigned short int __uint16_t;
 55typedef signed int __int32_t;
 56typedef unsigned int __uint32_t;
 57
 58typedef signed long int __int64_t;
 59typedef unsigned long int __uint64_t;
 60
 61
 62
 63
 64
 65
 66
 67typedef long int __quad_t;
 68typedef unsigned long int __u_quad_t;
 69# 131 "/usr/include/bits/types.h" 3 4
 70# 1 "/usr/include/bits/typesizes.h" 1 3 4
 71# 132 "/usr/include/bits/types.h" 2 3 4
 72
 73
 74typedef unsigned long int __dev_t;
 75typedef unsigned int __uid_t;
 76typedef unsigned int __gid_t;
 77typedef unsigned long int __ino_t;
 78typedef unsigned long int __ino64_t;
 79typedef unsigned int __mode_t;
 80typedef unsigned long int __nlink_t;
 81typedef long int __off_t;
 82typedef long int __off64_t;
 83typedef int __pid_t;
 84typedef struct { int __val[2]; } __fsid_t;
 85typedef long int __clock_t;
 86typedef unsigned long int __rlim_t;
 87typedef unsigned long int __rlim64_t;
 88typedef unsigned int __id_t;
 89typedef long int __time_t;
 90typedef unsigned int __useconds_t;
 91typedef long int __suseconds_t;
 92
 93typedef int __daddr_t;
 94typedef long int __swblk_t;
 95typedef int __key_t;
 96
 97
 98typedef int __clockid_t;
 99
100
101typedef void * __timer_t;
102
103
104typedef long int __blksize_t;
105
106
107
108
109typedef long int __blkcnt_t;
110typedef long int __blkcnt64_t;
111
112
113typedef unsigned long int __fsblkcnt_t;
114typedef unsigned long int __fsblkcnt64_t;
115
116
117typedef unsigned long int __fsfilcnt_t;
118typedef unsigned long int __fsfilcnt64_t;
119
120typedef long int __ssize_t;
121
122
123
124typedef __off64_t __loff_t;
125typedef __quad_t *__qaddr_t;
126typedef char *__caddr_t;
127
128
129typedef long int __intptr_t;
130
131
132typedef unsigned int __socklen_t;
133# 37 "/usr/include/stdio.h" 2 3 4
134# 45 "/usr/include/stdio.h" 3 4
135struct _IO_FILE;
136
137
138
139typedef struct _IO_FILE FILE;
140
141
142
143
144
145# 65 "/usr/include/stdio.h" 3 4
146typedef struct _IO_FILE __FILE;
147# 75 "/usr/include/stdio.h" 3 4
148# 1 "/usr/include/libio.h" 1 3 4
149# 32 "/usr/include/libio.h" 3 4
150# 1 "/usr/include/_G_config.h" 1 3 4
151# 15 "/usr/include/_G_config.h" 3 4
152# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h" 1 3 4
153# 16 "/usr/include/_G_config.h" 2 3 4
154
155
156
157
158# 1 "/usr/include/wchar.h" 1 3 4
159# 83 "/usr/include/wchar.h" 3 4
160typedef struct
161{
162  int __count;
163  union
164  {
165
166    unsigned int __wch;
167
168
169
170    char __wchb[4];
171  } __value;
172} __mbstate_t;
173# 21 "/usr/include/_G_config.h" 2 3 4
174
175typedef struct
176{
177  __off_t __pos;
178  __mbstate_t __state;
179} _G_fpos_t;
180typedef struct
181{
182  __off64_t __pos;
183  __mbstate_t __state;
184} _G_fpos64_t;
185# 53 "/usr/include/_G_config.h" 3 4
186typedef int _G_int16_t __attribute__ ((__mode__ (__HI__)));
187typedef int _G_int32_t __attribute__ ((__mode__ (__SI__)));
188typedef unsigned int _G_uint16_t __attribute__ ((__mode__ (__HI__)));
189typedef unsigned int _G_uint32_t __attribute__ ((__mode__ (__SI__)));
190# 33 "/usr/include/libio.h" 2 3 4
191# 53 "/usr/include/libio.h" 3 4
192# 1 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stdarg.h" 1 3 4
193# 40 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stdarg.h" 3 4
194typedef __builtin_va_list __gnuc_va_list;
195# 54 "/usr/include/libio.h" 2 3 4
196# 170 "/usr/include/libio.h" 3 4
197struct _IO_jump_t; struct _IO_FILE;
198# 180 "/usr/include/libio.h" 3 4
199typedef void _IO_lock_t;
200
201
202
203
204
205struct _IO_marker {
206  struct _IO_marker *_next;
207  struct _IO_FILE *_sbuf;
208
209
210
211  int _pos;
212# 203 "/usr/include/libio.h" 3 4
213};
214
215
216enum __codecvt_result
217{
218  __codecvt_ok,
219  __codecvt_partial,
220  __codecvt_error,
221  __codecvt_noconv
222};
223# 271 "/usr/include/libio.h" 3 4
224struct _IO_FILE {
225  int _flags;
226
227
228
229
230  char* _IO_read_ptr;
231  char* _IO_read_end;
232  char* _IO_read_base;
233  char* _IO_write_base;
234  char* _IO_write_ptr;
235  char* _IO_write_end;
236  char* _IO_buf_base;
237  char* _IO_buf_end;
238
239  char *_IO_save_base;
240  char *_IO_backup_base;
241  char *_IO_save_end;
242
243  struct _IO_marker *_markers;
244
245  struct _IO_FILE *_chain;
246
247  int _fileno;
248
249
250
251  int _flags2;
252
253  __off_t _old_offset;
254
255
256
257  unsigned short _cur_column;
258  signed char _vtable_offset;
259  char _shortbuf[1];
260
261
262
263  _IO_lock_t *_lock;
264# 319 "/usr/include/libio.h" 3 4
265  __off64_t _offset;
266# 328 "/usr/include/libio.h" 3 4
267  void *__pad1;
268  void *__pad2;
269  void *__pad3;
270  void *__pad4;
271  size_t __pad5;
272
273  int _mode;
274
275  char _unused2[15 * sizeof (int) - 4 * sizeof (void *) - sizeof (size_t)];
276
277};
278
279
280typedef struct _IO_FILE _IO_FILE;
281
282
283struct _IO_FILE_plus;
284
285extern struct _IO_FILE_plus _IO_2_1_stdin_;
286extern struct _IO_FILE_plus _IO_2_1_stdout_;
287extern struct _IO_FILE_plus _IO_2_1_stderr_;
288# 364 "/usr/include/libio.h" 3 4
289typedef __ssize_t __io_read_fn (void *__cookie, char *__buf, size_t __nbytes);
290
291
292
293
294
295
296
297typedef __ssize_t __io_write_fn (void *__cookie, __const char *__buf,
298     size_t __n);
299
300
301
302
303
304
305
306typedef int __io_seek_fn (void *__cookie, __off64_t *__pos, int __w);
307
308
309typedef int __io_close_fn (void *__cookie);
310# 416 "/usr/include/libio.h" 3 4
311extern int __underflow (_IO_FILE *);
312extern int __uflow (_IO_FILE *);
313extern int __overflow (_IO_FILE *, int);
314# 460 "/usr/include/libio.h" 3 4
315extern int _IO_getc (_IO_FILE *__fp);
316extern int _IO_putc (int __c, _IO_FILE *__fp);
317extern int _IO_feof (_IO_FILE *__fp) __attribute__ ((__nothrow__));
318extern int _IO_ferror (_IO_FILE *__fp) __attribute__ ((__nothrow__));
319
320extern int _IO_peekc_locked (_IO_FILE *__fp);
321
322
323
324
325
326extern void _IO_flockfile (_IO_FILE *) __attribute__ ((__nothrow__));
327extern void _IO_funlockfile (_IO_FILE *) __attribute__ ((__nothrow__));
328extern int _IO_ftrylockfile (_IO_FILE *) __attribute__ ((__nothrow__));
329# 490 "/usr/include/libio.h" 3 4
330extern int _IO_vfscanf (_IO_FILE * __restrict, const char * __restrict,
331   __gnuc_va_list, int *__restrict);
332extern int _IO_vfprintf (_IO_FILE *__restrict, const char *__restrict,
333    __gnuc_va_list);
334extern __ssize_t _IO_padn (_IO_FILE *, int, __ssize_t);
335extern size_t _IO_sgetn (_IO_FILE *, void *, size_t);
336
337extern __off64_t _IO_seekoff (_IO_FILE *, __off64_t, int, int);
338extern __off64_t _IO_seekpos (_IO_FILE *, __off64_t, int);
339
340extern void _IO_free_backup_area (_IO_FILE *) __attribute__ ((__nothrow__));
341# 76 "/usr/include/stdio.h" 2 3 4
342# 89 "/usr/include/stdio.h" 3 4
343
344
345typedef _G_fpos_t fpos_t;
346
347
348
349
350# 141 "/usr/include/stdio.h" 3 4
351# 1 "/usr/include/bits/stdio_lim.h" 1 3 4
352# 142 "/usr/include/stdio.h" 2 3 4
353
354
355
356extern struct _IO_FILE *stdin;
357extern struct _IO_FILE *stdout;
358extern struct _IO_FILE *stderr;
359
360
361
362
363
364
365
366
367
368extern int remove (__const char *__filename) __attribute__ ((__nothrow__));
369
370extern int rename (__const char *__old, __const char *__new) __attribute__ ((__nothrow__));
371
372
373
374
375extern int renameat (int __oldfd, __const char *__old, int __newfd,
376       __const char *__new) __attribute__ ((__nothrow__));
377
378
379
380
381
382
383
384
385extern FILE *tmpfile (void) ;
386# 188 "/usr/include/stdio.h" 3 4
387extern char *tmpnam (char *__s) __attribute__ ((__nothrow__)) ;
388
389
390
391
392
393extern char *tmpnam_r (char *__s) __attribute__ ((__nothrow__)) ;
394# 206 "/usr/include/stdio.h" 3 4
395extern char *tempnam (__const char *__dir, __const char *__pfx)
396     __attribute__ ((__nothrow__)) __attribute__ ((__malloc__)) ;
397
398
399
400
401
402
403
404
405extern int fclose (FILE *__stream);
406
407
408
409
410extern int fflush (FILE *__stream);
411
412# 231 "/usr/include/stdio.h" 3 4
413extern int fflush_unlocked (FILE *__stream);
414# 245 "/usr/include/stdio.h" 3 4
415
416
417
418
419
420
421extern FILE *fopen (__const char *__restrict __filename,
422      __const char *__restrict __modes) ;
423
424
425
426
427extern FILE *freopen (__const char *__restrict __filename,
428        __const char *__restrict __modes,
429        FILE *__restrict __stream) ;
430# 274 "/usr/include/stdio.h" 3 4
431
432# 285 "/usr/include/stdio.h" 3 4
433extern FILE *fdopen (int __fd, __const char *__modes) __attribute__ ((__nothrow__)) ;
434# 298 "/usr/include/stdio.h" 3 4
435extern FILE *fmemopen (void *__s, size_t __len, __const char *__modes)
436  __attribute__ ((__nothrow__)) ;
437
438
439
440
441extern FILE *open_memstream (char **__bufloc, size_t *__sizeloc) __attribute__ ((__nothrow__)) ;
442
443
444
445
446
447
448extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __attribute__ ((__nothrow__));
449
450
451
452extern int setvbuf (FILE *__restrict __stream, char *__restrict __buf,
453      int __modes, size_t __n) __attribute__ ((__nothrow__));
454
455
456
457
458
459extern void setbuffer (FILE *__restrict __stream, char *__restrict __buf,
460         size_t __size) __attribute__ ((__nothrow__));
461
462
463extern void setlinebuf (FILE *__stream) __attribute__ ((__nothrow__));
464
465
466
467
468
469
470
471
472extern int fprintf (FILE *__restrict __stream,
473      __const char *__restrict __format, ...);
474
475
476
477
478extern int printf (__const char *__restrict __format, ...);
479
480extern int sprintf (char *__restrict __s,
481      __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
482
483
484
485
486
487extern int vfprintf (FILE *__restrict __s, __const char *__restrict __format,
488       __gnuc_va_list __arg);
489
490
491
492
493extern int vprintf (__const char *__restrict __format, __gnuc_va_list __arg);
494
495extern int vsprintf (char *__restrict __s, __const char *__restrict __format,
496       __gnuc_va_list __arg) __attribute__ ((__nothrow__));
497
498
499
500
501
502extern int snprintf (char *__restrict __s, size_t __maxlen,
503       __const char *__restrict __format, ...)
504     __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 4)));
505
506extern int vsnprintf (char *__restrict __s, size_t __maxlen,
507        __const char *__restrict __format, __gnuc_va_list __arg)
508     __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__printf__, 3, 0)));
509
510# 396 "/usr/include/stdio.h" 3 4
511extern int vdprintf (int __fd, __const char *__restrict __fmt,
512       __gnuc_va_list __arg)
513     __attribute__ ((__format__ (__printf__, 2, 0)));
514extern int dprintf (int __fd, __const char *__restrict __fmt, ...)
515     __attribute__ ((__format__ (__printf__, 2, 3)));
516
517
518
519
520
521
522
523
524extern int fscanf (FILE *__restrict __stream,
525     __const char *__restrict __format, ...) ;
526
527
528
529
530extern int scanf (__const char *__restrict __format, ...) ;
531
532extern int sscanf (__const char *__restrict __s,
533     __const char *__restrict __format, ...) __attribute__ ((__nothrow__));
534# 427 "/usr/include/stdio.h" 3 4
535extern int fscanf (FILE *__restrict __stream, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_fscanf")
536
537                               ;
538extern int scanf (__const char *__restrict __format, ...) __asm__ ("" "__isoc99_scanf")
539                              ;
540extern int sscanf (__const char *__restrict __s, __const char *__restrict __format, ...) __asm__ ("" "__isoc99_sscanf") __attribute__ ((__nothrow__))
541
542                      ;
543# 447 "/usr/include/stdio.h" 3 4
544
545
546
547
548
549
550
551
552extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format,
553      __gnuc_va_list __arg)
554     __attribute__ ((__format__ (__scanf__, 2, 0))) ;
555
556
557
558
559
560extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg)
561     __attribute__ ((__format__ (__scanf__, 1, 0))) ;
562
563
564extern int vsscanf (__const char *__restrict __s,
565      __const char *__restrict __format, __gnuc_va_list __arg)
566     __attribute__ ((__nothrow__)) __attribute__ ((__format__ (__scanf__, 2, 0)));
567# 478 "/usr/include/stdio.h" 3 4
568extern int vfscanf (FILE *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vfscanf")
569
570
571
572     __attribute__ ((__format__ (__scanf__, 2, 0))) ;
573extern int vscanf (__const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vscanf")
574
575     __attribute__ ((__format__ (__scanf__, 1, 0))) ;
576extern int vsscanf (__const char *__restrict __s, __const char *__restrict __format, __gnuc_va_list __arg) __asm__ ("" "__isoc99_vsscanf") __attribute__ ((__nothrow__))
577
578
579
580     __attribute__ ((__format__ (__scanf__, 2, 0)));
581# 506 "/usr/include/stdio.h" 3 4
582
583
584
585
586
587
588
589
590
591extern int fgetc (FILE *__stream);
592extern int getc (FILE *__stream);
593
594
595
596
597
598extern int getchar (void);
599
600# 534 "/usr/include/stdio.h" 3 4
601extern int getc_unlocked (FILE *__stream);
602extern int getchar_unlocked (void);
603# 545 "/usr/include/stdio.h" 3 4
604extern int fgetc_unlocked (FILE *__stream);
605
606
607
608
609
610
611
612
613
614
615
616extern int fputc (int __c, FILE *__stream);
617extern int putc (int __c, FILE *__stream);
618
619
620
621
622
623extern int putchar (int __c);
624
625# 578 "/usr/include/stdio.h" 3 4
626extern int fputc_unlocked (int __c, FILE *__stream);
627
628
629
630
631
632
633
634extern int putc_unlocked (int __c, FILE *__stream);
635extern int putchar_unlocked (int __c);
636
637
638
639
640
641
642extern int getw (FILE *__stream);
643
644
645extern int putw (int __w, FILE *__stream);
646
647
648
649
650
651
652
653
654extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream)
655     ;
656
657
658
659
660
661
662extern char *gets (char *__s) ;
663
664# 640 "/usr/include/stdio.h" 3 4
665extern __ssize_t __getdelim (char **__restrict __lineptr,
666          size_t *__restrict __n, int __delimiter,
667          FILE *__restrict __stream) ;
668extern __ssize_t getdelim (char **__restrict __lineptr,
669        size_t *__restrict __n, int __delimiter,
670        FILE *__restrict __stream) ;
671
672
673
674
675
676
677
678extern __ssize_t getline (char **__restrict __lineptr,
679       size_t *__restrict __n,
680       FILE *__restrict __stream) ;
681
682
683
684
685
686
687
688
689extern int fputs (__const char *__restrict __s, FILE *__restrict __stream);
690
691
692
693
694
695extern int puts (__const char *__s);
696
697
698
699
700
701
702extern int ungetc (int __c, FILE *__stream);
703
704
705
706
707
708
709extern size_t fread (void *__restrict __ptr, size_t __size,
710       size_t __n, FILE *__restrict __stream) ;
711
712
713
714
715extern size_t fwrite (__const void *__restrict __ptr, size_t __size,
716        size_t __n, FILE *__restrict __s) ;
717
718# 712 "/usr/include/stdio.h" 3 4
719extern size_t fread_unlocked (void *__restrict __ptr, size_t __size,
720         size_t __n, FILE *__restrict __stream) ;
721extern size_t fwrite_unlocked (__const void *__restrict __ptr, size_t __size,
722          size_t __n, FILE *__restrict __stream) ;
723
724
725
726
727
728
729
730
731extern int fseek (FILE *__stream, long int __off, int __whence);
732
733
734
735
736extern long int ftell (FILE *__stream) ;
737
738
739
740
741extern void rewind (FILE *__stream);
742
743# 748 "/usr/include/stdio.h" 3 4
744extern int fseeko (FILE *__stream, __off_t __off, int __whence);
745
746
747
748
749extern __off_t ftello (FILE *__stream) ;
750# 767 "/usr/include/stdio.h" 3 4
751
752
753
754
755
756
757extern int fgetpos (FILE *__restrict __stream, fpos_t *__restrict __pos);
758
759
760
761
762extern int fsetpos (FILE *__stream, __const fpos_t *__pos);
763# 790 "/usr/include/stdio.h" 3 4
764
765# 799 "/usr/include/stdio.h" 3 4
766
767
768extern void clearerr (FILE *__stream) __attribute__ ((__nothrow__));
769
770extern int feof (FILE *__stream) __attribute__ ((__nothrow__)) ;
771
772extern int ferror (FILE *__stream) __attribute__ ((__nothrow__)) ;
773
774
775
776
777extern void clearerr_unlocked (FILE *__stream) __attribute__ ((__nothrow__));
778extern int feof_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
779extern int ferror_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
780
781
782
783
784
785
786
787
788extern void perror (__const char *__s);
789
790
791
792
793
794
795# 1 "/usr/include/bits/sys_errlist.h" 1 3 4
796# 27 "/usr/include/bits/sys_errlist.h" 3 4
797extern int sys_nerr;
798extern __const char *__const sys_errlist[];
799# 829 "/usr/include/stdio.h" 2 3 4
800
801
802
803
804extern int fileno (FILE *__stream) __attribute__ ((__nothrow__)) ;
805
806
807
808
809extern int fileno_unlocked (FILE *__stream) __attribute__ ((__nothrow__)) ;
810# 848 "/usr/include/stdio.h" 3 4
811extern FILE *popen (__const char *__command, __const char *__modes) ;
812
813
814
815
816
817extern int pclose (FILE *__stream);
818
819
820
821
822
823extern char *ctermid (char *__s) __attribute__ ((__nothrow__));
824# 888 "/usr/include/stdio.h" 3 4
825extern void flockfile (FILE *__stream) __attribute__ ((__nothrow__));
826
827
828
829extern int ftrylockfile (FILE *__stream) __attribute__ ((__nothrow__)) ;
830
831
832extern void funlockfile (FILE *__stream) __attribute__ ((__nothrow__));
833# 918 "/usr/include/stdio.h" 3 4
834
835# 2 "files/sizeofparameters_test.c" 2
836# 1 "./assert.h" 1
837
838void __blast_assert()
839{
840 ERROR: goto ERROR;
841}
842# 3 "files/sizeofparameters_test.c" 2
843
844
845
846void foo();
847
848int globalSize;
849
850int
851main(int argc, char* argv[]) {
852 long int a;
853 globalSize=sizeof(a);
854 foo(a);
855 return 0;
856}
857
858void foo(int a) {
859 ((sizeof(a)==globalSize) ? (0) : __blast_assert ());
860}