Showing error 1787

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


Source:

 820int prompt(char *msg ) ;
 821#line 9 "Util.c"
 822int prompt(char *msg ) 
 823{ int retValue_acc ;
 824  int retval ;
 825  char const   * __restrict  __cil_tmp4 ;
 826
 827  {
 828  {
 829#line 10
 830  __cil_tmp4 = (char const   * __restrict  )"%s\n";
 831#line 10
 832  printf(__cil_tmp4, msg);
 833#line 518 "Util.c"
 834  retValue_acc = retval;
 835  }
 836#line 520
 837  return (retValue_acc);
 838#line 527
 839  return (retValue_acc);
 840}
 841}
 842#line 1 "wsllib_check.o"
 843#pragma merger(0,"wsllib_check.i","")
 844#line 3 "wsllib_check.c"
 845void __automaton_fail(void) 
 846{ 
 847
 848  {
 849  goto ERROR;
 850  ERROR: ;
 851#line 53 "wsllib_check.c"
 852  return;
 853}
 854}
 855#line 1 "libacc.o"
 856#pragma merger(0,"libacc.i","")
 857#line 73 "/usr/include/assert.h"
 858extern  __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const   *__assertion ,
 859                                                                      char const   *__file ,
 860                                                                      unsigned int __line ,
Show full sources