Showing error 1701

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

Source: 

1454{ int tmp ;
1455
1456  {
1457  {
1458#line 13
1459  puts("before autoRespond\n");
1460#line 14
1461  tmp = isReadable(msg);
1462  }
1463#line 14
1464  if (tmp) {
1465
1466  } else {
1467    {
1468#line 15
1469    __automaton_fail();
1470    }
1471  }
1472#line 15
1473  return;
1474}
1475}
1476#line 1 "wsllib_check.o"
1477#pragma merger(0,"wsllib_check.i","")
1478#line 3 "wsllib_check.c"
1479void __automaton_fail(void) 
1480{ 
1481
1482  {
1483  goto ERROR;
1484  ERROR: ;
1485#line 53 "wsllib_check.c"
1486  return;
1487}
1488}
1489#line 1 "Util.o"
1490#pragma merger(0,"Util.i","")
1491#line 1 "Util.h"
1492int prompt(char *msg ) ;
1493#line 9 "Util.c"
1494int prompt(char *msg )
Show full sources
↑