3813int prompt(char *msg ) ;
3814#line 9 "Util.c"
3815int prompt(char *msg )
3816{ int retValue_acc ;
3817 int retval ;
3818 char const * __restrict __cil_tmp4 ;
3819
3820 {
3821 {
3822#line 10
3823 __cil_tmp4 = (char const * __restrict )"%s\n";
3824#line 10
3825 printf(__cil_tmp4, msg);
3826#line 518 "Util.c"
3827 retValue_acc = retval;
3828 }
3829#line 520
3830 return (retValue_acc);
3831#line 527
3832 return (retValue_acc);
3833}
3834}
3835#line 1 "wsllib_check.o"
3836#pragma merger(0,"wsllib_check.i","")
3837#line 3 "wsllib_check.c"
3838void __automaton_fail(void)
3839{
3840
3841 {
3842 goto ERROR;
3843 ERROR: ;
3844#line 53 "wsllib_check.c"
3845 return;
3846}
3847}
3848#line 1 "DecryptForward_spec.o"
3849#pragma merger(0,"DecryptForward_spec.i","")
3850#line 11 "DecryptForward_spec.c"
3851void __utac_acc__DecryptForward_spec__1(int msg )
3852{ int tmp ;
3853