Showing error 1922

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: product-lines/minepump_spec2_product17_safe.cil.c
Line in file: 552
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 522#line 20 "featureselect.c"
 523void select_helpers(void) 
 524{ 
 525
 526  {
 527#line 111 "featureselect.c"
 528  return;
 529}
 530}
 531#line 25 "featureselect.c"
 532int valid_product(void) 
 533{ int retValue_acc ;
 534
 535  {
 536#line 129 "featureselect.c"
 537  retValue_acc = 1;
 538#line 131
 539  return (retValue_acc);
 540#line 138
 541  return (retValue_acc);
 542}
 543}
 544#line 1 "wsllib_check.o"
 545#pragma merger(0,"wsllib_check.i","")
 546#line 3 "wsllib_check.c"
 547void __automaton_fail(void) 
 548{ 
 549
 550  {
 551  goto ERROR;
 552  ERROR: ;
 553#line 53 "wsllib_check.c"
 554  return;
 555}
 556}
 557#line 1 "libacc.o"
 558#pragma merger(0,"libacc.i","")
 559#line 73 "/usr/include/assert.h"
 560extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 561                                                                      char const   *__file ,
 562                                                                      unsigned int __line ,
Show full sources