520#line 10 "EncryptVerify_spec.c"
521__inline void __utac_acc__EncryptVerify_spec__1(int msg )
522{ int tmp ;
523
524 {
525 {
526#line 16
527 tmp = isReadable(msg);
528 }
529#line 16
530 if (tmp) {
531
532 } else {
533 {
534#line 13
535 __automaton_fail();
536 }
537 }
538#line 13
539 return;
540}
541}
542#line 1 "wsllib_check.o"
543#pragma merger(0,"wsllib_check.i","")
544#line 3 "wsllib_check.c"
545void __automaton_fail(void)
546{
547
548 {
549 goto ERROR;
550 ERROR: ;
551#line 53 "wsllib_check.c"
552 return;
553}
554}
555#line 1 "Client.o"
556#pragma merger(0,"Client.i","")
557#line 4 "ClientLib.h"
558int initClient(void) ;
559#line 33
560int getClientPrivateKey(int handle ) ;