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_spec4_product29_safe.cil.c |
Line in file: | 3893 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
3863 } 3864 } 3865 } 3866 } 3867 } 3868 } 3869 } 3870 } 3871 } 3872 } 3873 } 3874 } 3875 while_3_break: /* CIL Label */ ; 3876 } 3877 { 3878#line 60 3879 bobToRjh(); 3880 } 3881#line 167 "scenario.c" 3882 return; 3883} 3884} 3885#line 1 "wsllib_check.o" 3886#pragma merger(0,"wsllib_check.i","") 3887#line 3 "wsllib_check.c" 3888void __automaton_fail(void) 3889{ 3890 3891 { 3892 goto ERROR; 3893 ERROR: ; 3894#line 53 "wsllib_check.c" 3895 return; 3896} 3897} 3898#line 1 "SignForward_spec.o" 3899#pragma merger(0,"SignForward_spec.i","") 3900#line 13 "SignForward_spec.c" 3901__inline void __utac_acc__SignForward_spec__1(int client , int msg ) 3902{ int tmp ; 3903 int tmp___0 ;