769#line 10 "EncryptVerify_spec.c"
770__inline void __utac_acc__EncryptVerify_spec__1(int msg )
771{ int tmp ;
772
773 {
774 {
775#line 16
776 tmp = isReadable(msg);
777 }
778#line 16
779 if (tmp) {
780
781 } else {
782 {
783#line 13
784 __automaton_fail();
785 }
786 }
787#line 13
788 return;
789}
790}
791#line 1 "wsllib_check.o"
792#pragma merger(0,"wsllib_check.i","")
793#line 3 "wsllib_check.c"
794void __automaton_fail(void)
795{
796
797 {
798 goto ERROR;
799 ERROR: ;
800#line 53 "wsllib_check.c"
801 return;
802}
803}
804#line 1 "libacc.o"
805#pragma merger(0,"libacc.i","")
806#line 73 "/usr/include/assert.h"
807extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
808 char const *__file ,
809 unsigned int __line ,