Showing error 2107

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_spec5_product07_safe.cil.c
Line in file: 698
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

 668}
 669}
 670#line 66 "MinePump.c"
 671void stopSystem(void) 
 672{ 
 673
 674  {
 675#line 71
 676  if (pumpRunning) {
 677    {
 678#line 68
 679    deactivatePump();
 680    }
 681  } else {
 682
 683  }
 684#line 71
 685  systemActive = 0;
 686#line 318 "MinePump.c"
 687  return;
 688}
 689}
 690#line 1 "wsllib_check.o"
 691#pragma merger(0,"wsllib_check.i","")
 692#line 3 "wsllib_check.c"
 693void __automaton_fail(void) 
 694{ 
 695
 696  {
 697  goto ERROR;
 698  ERROR: ;
 699#line 53 "wsllib_check.c"
 700  return;
 701}
 702}
 703#line 1 "featureselect.o"
 704#pragma merger(0,"featureselect.i","")
 705#line 8 "featureselect.h"
 706int select_one(void) ;
 707#line 8 "featureselect.c"
 708int select_one(void) 
Show full sources