1extern int __VERIFIER_nondet_int(void);
2
3
4
5#line 2 "libacc.c"
6struct JoinPoint {
7 void **(*fp)(struct JoinPoint * ) ;
8 void **args ;
9 int argsCount ;
10 char const **argsType ;
11 void *(*arg)(int , struct JoinPoint * ) ;
12 char const *(*argType)(int , struct JoinPoint * ) ;
13 void **retValue ;
14 char const *retType ;
15 char const *funcName ;
16 char const *targetName ;
17 char const *fileName ;
18 char const *kind ;
19 void *excep_return ;
20};
21#line 18 "libacc.c"
22struct __UTAC__CFLOW_FUNC {
23 int (*func)(int , int ) ;
24 int val ;
25 struct __UTAC__CFLOW_FUNC *next ;
26};
27#line 18 "libacc.c"
28struct __UTAC__EXCEPTION {
29 void *jumpbuf ;
30 unsigned long long prtValue ;
31 int pops ;
32 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
33};
34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
35typedef unsigned long size_t;
36#line 76 "libacc.c"
37struct __ACC__ERR {
38 void *v ;
39 struct __ACC__ERR *next ;
40};
41#line 1 "Email.o"
42#pragma merger(0,"Email.i","")
43#line 359 "/usr/include/stdio.h"
44extern int printf(char const * __restrict __format , ...) ;
45#line 8 "featureselect.h"
46int __SELECTED_FEATURE_Base ;
47#line 11 "featureselect.h"
48int __SELECTED_FEATURE_Keys ;
49#line 14 "featureselect.h"
50int __SELECTED_FEATURE_Encrypt ;
51#line 17 "featureselect.h"
52int __SELECTED_FEATURE_AutoResponder ;
53#line 20 "featureselect.h"
54int __SELECTED_FEATURE_AddressBook ;
55#line 23 "featureselect.h"
56int __SELECTED_FEATURE_Sign ;
57#line 26 "featureselect.h"
58int __SELECTED_FEATURE_Forward ;
59#line 29 "featureselect.h"
60int __SELECTED_FEATURE_Verify ;
61#line 32 "featureselect.h"
62int __SELECTED_FEATURE_Decrypt ;
63#line 35 "featureselect.h"
64int __GUIDSL_ROOT_PRODUCTION ;
65#line 37 "featureselect.h"
66int __GUIDSL_NON_TERMINAL_main ;
67#line 6 "EmailLib.h"
68int getEmailId(int handle ) ;
69#line 10
70int getEmailFrom(int handle ) ;
71#line 12
72void setEmailFrom(int handle , int value ) ;
73#line 14
74int getEmailTo(int handle ) ;
75#line 16
76void setEmailTo(int handle , int value ) ;
77#line 26
78int isEncrypted(int handle ) ;
79#line 30
80int getEmailEncryptionKey(int handle ) ;
81#line 34
82int isSigned(int handle ) ;
83#line 38
84int getEmailSignKey(int handle ) ;
85#line 42
86int isVerified(int handle ) ;
87#line 6 "Email.h"
88void printMail(int msg ) ;
89#line 9
90int isReadable(int msg ) ;
91#line 12
92int createEmail(int from , int to ) ;
93#line 15
94int cloneEmail(int msg ) ;
95#line 9 "Email.c"
96void printMail__wrappee__Keys(int msg )
97{ int tmp ;
98 int tmp___0 ;
99 int tmp___1 ;
100 int tmp___2 ;
101 char const * __restrict __cil_tmp6 ;
102 char const * __restrict __cil_tmp7 ;
103 char const * __restrict __cil_tmp8 ;
104 char const * __restrict __cil_tmp9 ;
105
106 {
107 {
108#line 10
109 tmp = getEmailId(msg);
110#line 10
111 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
112#line 10
113 printf(__cil_tmp6, tmp);
114#line 11
115 tmp___0 = getEmailFrom(msg);
116#line 11
117 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
118#line 11
119 printf(__cil_tmp7, tmp___0);
120#line 12
121 tmp___1 = getEmailTo(msg);
122#line 12
123 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
124#line 12
125 printf(__cil_tmp8, tmp___1);
126#line 13
127 tmp___2 = isReadable(msg);
128#line 13
129 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
130#line 13
131 printf(__cil_tmp9, tmp___2);
132 }
133#line 601 "Email.c"
134 return;
135}
136}
137#line 17 "Email.c"
138void printMail__wrappee__AddressBook(int msg )
139{ int tmp ;
140 int tmp___0 ;
141 char const * __restrict __cil_tmp4 ;
142 char const * __restrict __cil_tmp5 ;
143
144 {
145 {
146#line 18
147 printMail__wrappee__Keys(msg);
148#line 19
149 tmp = isEncrypted(msg);
150#line 19
151 __cil_tmp4 = (char const * __restrict )"ENCRYPTED\n %d\n";
152#line 19
153 printf(__cil_tmp4, tmp);
154#line 20
155 tmp___0 = getEmailEncryptionKey(msg);
156#line 20
157 __cil_tmp5 = (char const * __restrict )"ENCRYPTION KEY\n %d\n";
158#line 20
159 printf(__cil_tmp5, tmp___0);
160 }
161#line 625 "Email.c"
162 return;
163}
164}
165#line 26 "Email.c"
166void printMail__wrappee__Forward(int msg )
167{ int tmp ;
168 int tmp___0 ;
169 char const * __restrict __cil_tmp4 ;
170 char const * __restrict __cil_tmp5 ;
171
172 {
173 {
174#line 27
175 printMail__wrappee__AddressBook(msg);
176#line 28
177 tmp = isSigned(msg);
178#line 28
179 __cil_tmp4 = (char const * __restrict )"SIGNED\n %i\n";
180#line 28
181 printf(__cil_tmp4, tmp);
182#line 29
183 tmp___0 = getEmailSignKey(msg);
184#line 29
185 __cil_tmp5 = (char const * __restrict )"SIGNATURE\n %i\n";
186#line 29
187 printf(__cil_tmp5, tmp___0);
188 }
189#line 649 "Email.c"
190 return;
191}
192}
193#line 33 "Email.c"
194void printMail(int msg )
195{ int tmp ;
196 char const * __restrict __cil_tmp3 ;
197
198 {
199 {
200#line 34
201 printMail__wrappee__Forward(msg);
202#line 35
203 tmp = isVerified(msg);
204#line 35
205 __cil_tmp3 = (char const * __restrict )"SIGNATURE VERIFIED\n %d\n";
206#line 35
207 printf(__cil_tmp3, tmp);
208 }
209#line 671 "Email.c"
210 return;
211}
212}
213#line 41 "Email.c"
214int isReadable__wrappee__Keys(int msg )
215{ int retValue_acc ;
216
217 {
218#line 689 "Email.c"
219 retValue_acc = 1;
220#line 691
221 return (retValue_acc);
222#line 698
223 return (retValue_acc);
224}
225}
226#line 49 "Email.c"
227int isReadable(int msg )
228{ int retValue_acc ;
229 int tmp ;
230
231 {
232 {
233#line 53
234 tmp = isEncrypted(msg);
235 }
236#line 53 "Email.c"
237 if (tmp) {
238#line 727
239 retValue_acc = 0;
240#line 729
241 return (retValue_acc);
242 } else {
243 {
244#line 721 "Email.c"
245 retValue_acc = isReadable__wrappee__Keys(msg);
246 }
247#line 723
248 return (retValue_acc);
249 }
250#line 736 "Email.c"
251 return (retValue_acc);
252}
253}
254#line 57 "Email.c"
255int cloneEmail(int msg )
256{ int retValue_acc ;
257
258 {
259#line 758 "Email.c"
260 retValue_acc = msg;
261#line 760
262 return (retValue_acc);
263#line 767
264 return (retValue_acc);
265}
266}
267#line 62 "Email.c"
268int createEmail(int from , int to )
269{ int retValue_acc ;
270 int msg ;
271
272 {
273 {
274#line 63
275 msg = 1;
276#line 64
277 setEmailFrom(msg, from);
278#line 65
279 setEmailTo(msg, to);
280#line 797 "Email.c"
281 retValue_acc = msg;
282 }
283#line 799
284 return (retValue_acc);
285#line 806
286 return (retValue_acc);
287}
288}
289#line 1 "Util.o"
290#pragma merger(0,"Util.i","")
291#line 1 "Util.h"
292int prompt(char *msg ) ;
293#line 9 "Util.c"
294int prompt(char *msg )
295{ int retValue_acc ;
296 int retval ;
297 char const * __restrict __cil_tmp4 ;
298
299 {
300 {
301#line 10
302 __cil_tmp4 = (char const * __restrict )"%s\n";
303#line 10
304 printf(__cil_tmp4, msg);
305#line 518 "Util.c"
306 retValue_acc = retval;
307 }
308#line 520
309 return (retValue_acc);
310#line 527
311 return (retValue_acc);
312}
313}
314#line 1 "ClientLib.o"
315#pragma merger(0,"ClientLib.i","")
316#line 4 "ClientLib.h"
317int initClient(void) ;
318#line 6
319char *getClientName(int handle ) ;
320#line 8
321void setClientName(int handle , char *value ) ;
322#line 10
323int getClientOutbuffer(int handle ) ;
324#line 12
325void setClientOutbuffer(int handle , int value ) ;
326#line 14
327int getClientAddressBookSize(int handle ) ;
328#line 16
329void setClientAddressBookSize(int handle , int value ) ;
330#line 18
331int createClientAddressBookEntry(int handle ) ;
332#line 20
333int getClientAddressBookAlias(int handle , int index ) ;
334#line 22
335void setClientAddressBookAlias(int handle , int index , int value ) ;
336#line 24
337int getClientAddressBookAddress(int handle , int index ) ;
338#line 26
339void setClientAddressBookAddress(int handle , int index , int value ) ;
340#line 29
341int getClientAutoResponse(int handle ) ;
342#line 31
343void setClientAutoResponse(int handle , int value ) ;
344#line 33
345int getClientPrivateKey(int handle ) ;
346#line 35
347void setClientPrivateKey(int handle , int value ) ;
348#line 37
349int getClientKeyringSize(int handle ) ;
350#line 39
351int createClientKeyringEntry(int handle ) ;
352#line 41
353int getClientKeyringUser(int handle , int index ) ;
354#line 43
355void setClientKeyringUser(int handle , int index , int value ) ;
356#line 45
357int getClientKeyringPublicKey(int handle , int index ) ;
358#line 47
359void setClientKeyringPublicKey(int handle , int index , int value ) ;
360#line 49
361int getClientForwardReceiver(int handle ) ;
362#line 51
363void setClientForwardReceiver(int handle , int value ) ;
364#line 53
365int getClientId(int handle ) ;
366#line 55
367void setClientId(int handle , int value ) ;
368#line 57
369int findPublicKey(int handle , int userid ) ;
370#line 59
371int findClientAddressBookAlias(int handle , int userid ) ;
372#line 5 "ClientLib.c"
373int __ste_Client_counter = 0;
374#line 7 "ClientLib.c"
375int initClient(void)
376{ int retValue_acc ;
377
378 {
379#line 12 "ClientLib.c"
380 if (__ste_Client_counter < 3) {
381#line 684
382 __ste_Client_counter = __ste_Client_counter + 1;
383#line 684
384 retValue_acc = __ste_Client_counter;
385#line 686
386 return (retValue_acc);
387 } else {
388#line 692 "ClientLib.c"
389 retValue_acc = -1;
390#line 694
391 return (retValue_acc);
392 }
393#line 701 "ClientLib.c"
394 return (retValue_acc);
395}
396}
397#line 15 "ClientLib.c"
398char *__ste_client_name0 = (char *)0;
399#line 17 "ClientLib.c"
400char *__ste_client_name1 = (char *)0;
401#line 19 "ClientLib.c"
402char *__ste_client_name2 = (char *)0;
403#line 22 "ClientLib.c"
404char *getClientName(int handle )
405{ char *retValue_acc ;
406 void *__cil_tmp3 ;
407
408 {
409#line 31 "ClientLib.c"
410 if (handle == 1) {
411#line 732
412 retValue_acc = __ste_client_name0;
413#line 734
414 return (retValue_acc);
415 } else {
416#line 736
417 if (handle == 2) {
418#line 741
419 retValue_acc = __ste_client_name1;
420#line 743
421 return (retValue_acc);
422 } else {
423#line 745
424 if (handle == 3) {
425#line 750
426 retValue_acc = __ste_client_name2;
427#line 752
428 return (retValue_acc);
429 } else {
430#line 758 "ClientLib.c"
431 __cil_tmp3 = (void *)0;
432#line 758
433 retValue_acc = (char *)__cil_tmp3;
434#line 760
435 return (retValue_acc);
436 }
437 }
438 }
439#line 767 "ClientLib.c"
440 return (retValue_acc);
441}
442}
443#line 34 "ClientLib.c"
444void setClientName(int handle , char *value )
445{
446
447 {
448#line 42
449 if (handle == 1) {
450#line 36
451 __ste_client_name0 = value;
452 } else {
453#line 37
454 if (handle == 2) {
455#line 38
456 __ste_client_name1 = value;
457 } else {
458#line 39
459 if (handle == 3) {
460#line 40
461 __ste_client_name2 = value;
462 } else {
463
464 }
465 }
466 }
467#line 802 "ClientLib.c"
468 return;
469}
470}
471#line 44 "ClientLib.c"
472int __ste_client_outbuffer0 = 0;
473#line 46 "ClientLib.c"
474int __ste_client_outbuffer1 = 0;
475#line 48 "ClientLib.c"
476int __ste_client_outbuffer2 = 0;
477#line 50 "ClientLib.c"
478int __ste_client_outbuffer3 = 0;
479#line 53 "ClientLib.c"
480int getClientOutbuffer(int handle )
481{ int retValue_acc ;
482
483 {
484#line 62 "ClientLib.c"
485 if (handle == 1) {
486#line 831
487 retValue_acc = __ste_client_outbuffer0;
488#line 833
489 return (retValue_acc);
490 } else {
491#line 835
492 if (handle == 2) {
493#line 840
494 retValue_acc = __ste_client_outbuffer1;
495#line 842
496 return (retValue_acc);
497 } else {
498#line 844
499 if (handle == 3) {
500#line 849
501 retValue_acc = __ste_client_outbuffer2;
502#line 851
503 return (retValue_acc);
504 } else {
505#line 857 "ClientLib.c"
506 retValue_acc = 0;
507#line 859
508 return (retValue_acc);
509 }
510 }
511 }
512#line 866 "ClientLib.c"
513 return (retValue_acc);
514}
515}
516#line 65 "ClientLib.c"
517void setClientOutbuffer(int handle , int value )
518{
519
520 {
521#line 73
522 if (handle == 1) {
523#line 67
524 __ste_client_outbuffer0 = value;
525 } else {
526#line 68
527 if (handle == 2) {
528#line 69
529 __ste_client_outbuffer1 = value;
530 } else {
531#line 70
532 if (handle == 3) {
533#line 71
534 __ste_client_outbuffer2 = value;
535 } else {
536
537 }
538 }
539 }
540#line 901 "ClientLib.c"
541 return;
542}
543}
544#line 77 "ClientLib.c"
545int __ste_ClientAddressBook_size0 = 0;
546#line 79 "ClientLib.c"
547int __ste_ClientAddressBook_size1 = 0;
548#line 81 "ClientLib.c"
549int __ste_ClientAddressBook_size2 = 0;
550#line 84 "ClientLib.c"
551int getClientAddressBookSize(int handle )
552{ int retValue_acc ;
553
554 {
555#line 93 "ClientLib.c"
556 if (handle == 1) {
557#line 928
558 retValue_acc = __ste_ClientAddressBook_size0;
559#line 930
560 return (retValue_acc);
561 } else {
562#line 932
563 if (handle == 2) {
564#line 937
565 retValue_acc = __ste_ClientAddressBook_size1;
566#line 939
567 return (retValue_acc);
568 } else {
569#line 941
570 if (handle == 3) {
571#line 946
572 retValue_acc = __ste_ClientAddressBook_size2;
573#line 948
574 return (retValue_acc);
575 } else {
576#line 954 "ClientLib.c"
577 retValue_acc = 0;
578#line 956
579 return (retValue_acc);
580 }
581 }
582 }
583#line 963 "ClientLib.c"
584 return (retValue_acc);
585}
586}
587#line 96 "ClientLib.c"
588void setClientAddressBookSize(int handle , int value )
589{
590
591 {
592#line 104
593 if (handle == 1) {
594#line 98
595 __ste_ClientAddressBook_size0 = value;
596 } else {
597#line 99
598 if (handle == 2) {
599#line 100
600 __ste_ClientAddressBook_size1 = value;
601 } else {
602#line 101
603 if (handle == 3) {
604#line 102
605 __ste_ClientAddressBook_size2 = value;
606 } else {
607
608 }
609 }
610 }
611#line 998 "ClientLib.c"
612 return;
613}
614}
615#line 106 "ClientLib.c"
616int createClientAddressBookEntry(int handle )
617{ int retValue_acc ;
618 int size ;
619 int tmp ;
620 int __cil_tmp5 ;
621
622 {
623 {
624#line 107
625 tmp = getClientAddressBookSize(handle);
626#line 107
627 size = tmp;
628 }
629#line 108 "ClientLib.c"
630 if (size < 3) {
631 {
632#line 109 "ClientLib.c"
633 __cil_tmp5 = size + 1;
634#line 109
635 setClientAddressBookSize(handle, __cil_tmp5);
636#line 1025 "ClientLib.c"
637 retValue_acc = size + 1;
638 }
639#line 1027
640 return (retValue_acc);
641 } else {
642#line 1031 "ClientLib.c"
643 retValue_acc = -1;
644#line 1033
645 return (retValue_acc);
646 }
647#line 1040 "ClientLib.c"
648 return (retValue_acc);
649}
650}
651#line 115 "ClientLib.c"
652int __ste_Client_AddressBook0_Alias0 = 0;
653#line 117 "ClientLib.c"
654int __ste_Client_AddressBook0_Alias1 = 0;
655#line 119 "ClientLib.c"
656int __ste_Client_AddressBook0_Alias2 = 0;
657#line 121 "ClientLib.c"
658int __ste_Client_AddressBook1_Alias0 = 0;
659#line 123 "ClientLib.c"
660int __ste_Client_AddressBook1_Alias1 = 0;
661#line 125 "ClientLib.c"
662int __ste_Client_AddressBook1_Alias2 = 0;
663#line 127 "ClientLib.c"
664int __ste_Client_AddressBook2_Alias0 = 0;
665#line 129 "ClientLib.c"
666int __ste_Client_AddressBook2_Alias1 = 0;
667#line 131 "ClientLib.c"
668int __ste_Client_AddressBook2_Alias2 = 0;
669#line 134 "ClientLib.c"
670int getClientAddressBookAlias(int handle , int index )
671{ int retValue_acc ;
672
673 {
674#line 167
675 if (handle == 1) {
676#line 144 "ClientLib.c"
677 if (index == 0) {
678#line 1086
679 retValue_acc = __ste_Client_AddressBook0_Alias0;
680#line 1088
681 return (retValue_acc);
682 } else {
683#line 1090
684 if (index == 1) {
685#line 1095
686 retValue_acc = __ste_Client_AddressBook0_Alias1;
687#line 1097
688 return (retValue_acc);
689 } else {
690#line 1099
691 if (index == 2) {
692#line 1104
693 retValue_acc = __ste_Client_AddressBook0_Alias2;
694#line 1106
695 return (retValue_acc);
696 } else {
697#line 1112
698 retValue_acc = 0;
699#line 1114
700 return (retValue_acc);
701 }
702 }
703 }
704 } else {
705#line 1116 "ClientLib.c"
706 if (handle == 2) {
707#line 154 "ClientLib.c"
708 if (index == 0) {
709#line 1124
710 retValue_acc = __ste_Client_AddressBook1_Alias0;
711#line 1126
712 return (retValue_acc);
713 } else {
714#line 1128
715 if (index == 1) {
716#line 1133
717 retValue_acc = __ste_Client_AddressBook1_Alias1;
718#line 1135
719 return (retValue_acc);
720 } else {
721#line 1137
722 if (index == 2) {
723#line 1142
724 retValue_acc = __ste_Client_AddressBook1_Alias2;
725#line 1144
726 return (retValue_acc);
727 } else {
728#line 1150
729 retValue_acc = 0;
730#line 1152
731 return (retValue_acc);
732 }
733 }
734 }
735 } else {
736#line 1154 "ClientLib.c"
737 if (handle == 3) {
738#line 164 "ClientLib.c"
739 if (index == 0) {
740#line 1162
741 retValue_acc = __ste_Client_AddressBook2_Alias0;
742#line 1164
743 return (retValue_acc);
744 } else {
745#line 1166
746 if (index == 1) {
747#line 1171
748 retValue_acc = __ste_Client_AddressBook2_Alias1;
749#line 1173
750 return (retValue_acc);
751 } else {
752#line 1175
753 if (index == 2) {
754#line 1180
755 retValue_acc = __ste_Client_AddressBook2_Alias2;
756#line 1182
757 return (retValue_acc);
758 } else {
759#line 1188
760 retValue_acc = 0;
761#line 1190
762 return (retValue_acc);
763 }
764 }
765 }
766 } else {
767#line 1196 "ClientLib.c"
768 retValue_acc = 0;
769#line 1198
770 return (retValue_acc);
771 }
772 }
773 }
774#line 1205 "ClientLib.c"
775 return (retValue_acc);
776}
777}
778#line 171 "ClientLib.c"
779int findClientAddressBookAlias(int handle , int userid )
780{ int retValue_acc ;
781
782 {
783#line 204
784 if (handle == 1) {
785#line 181 "ClientLib.c"
786 if (userid == __ste_Client_AddressBook0_Alias0) {
787#line 1233
788 retValue_acc = 0;
789#line 1235
790 return (retValue_acc);
791 } else {
792#line 1237
793 if (userid == __ste_Client_AddressBook0_Alias1) {
794#line 1242
795 retValue_acc = 1;
796#line 1244
797 return (retValue_acc);
798 } else {
799#line 1246
800 if (userid == __ste_Client_AddressBook0_Alias2) {
801#line 1251
802 retValue_acc = 2;
803#line 1253
804 return (retValue_acc);
805 } else {
806#line 1259
807 retValue_acc = -1;
808#line 1261
809 return (retValue_acc);
810 }
811 }
812 }
813 } else {
814#line 1263 "ClientLib.c"
815 if (handle == 2) {
816#line 191 "ClientLib.c"
817 if (userid == __ste_Client_AddressBook1_Alias0) {
818#line 1271
819 retValue_acc = 0;
820#line 1273
821 return (retValue_acc);
822 } else {
823#line 1275
824 if (userid == __ste_Client_AddressBook1_Alias1) {
825#line 1280
826 retValue_acc = 1;
827#line 1282
828 return (retValue_acc);
829 } else {
830#line 1284
831 if (userid == __ste_Client_AddressBook1_Alias2) {
832#line 1289
833 retValue_acc = 2;
834#line 1291
835 return (retValue_acc);
836 } else {
837#line 1297
838 retValue_acc = -1;
839#line 1299
840 return (retValue_acc);
841 }
842 }
843 }
844 } else {
845#line 1301 "ClientLib.c"
846 if (handle == 3) {
847#line 201 "ClientLib.c"
848 if (userid == __ste_Client_AddressBook2_Alias0) {
849#line 1309
850 retValue_acc = 0;
851#line 1311
852 return (retValue_acc);
853 } else {
854#line 1313
855 if (userid == __ste_Client_AddressBook2_Alias1) {
856#line 1318
857 retValue_acc = 1;
858#line 1320
859 return (retValue_acc);
860 } else {
861#line 1322
862 if (userid == __ste_Client_AddressBook2_Alias2) {
863#line 1327
864 retValue_acc = 2;
865#line 1329
866 return (retValue_acc);
867 } else {
868#line 1335
869 retValue_acc = -1;
870#line 1337
871 return (retValue_acc);
872 }
873 }
874 }
875 } else {
876#line 1343 "ClientLib.c"
877 retValue_acc = -1;
878#line 1345
879 return (retValue_acc);
880 }
881 }
882 }
883#line 1352 "ClientLib.c"
884 return (retValue_acc);
885}
886}
887#line 208 "ClientLib.c"
888void setClientAddressBookAlias(int handle , int index , int value )
889{
890
891 {
892#line 234
893 if (handle == 1) {
894#line 217
895 if (index == 0) {
896#line 211
897 __ste_Client_AddressBook0_Alias0 = value;
898 } else {
899#line 212
900 if (index == 1) {
901#line 213
902 __ste_Client_AddressBook0_Alias1 = value;
903 } else {
904#line 214
905 if (index == 2) {
906#line 215
907 __ste_Client_AddressBook0_Alias2 = value;
908 } else {
909
910 }
911 }
912 }
913 } else {
914#line 216
915 if (handle == 2) {
916#line 225
917 if (index == 0) {
918#line 219
919 __ste_Client_AddressBook1_Alias0 = value;
920 } else {
921#line 220
922 if (index == 1) {
923#line 221
924 __ste_Client_AddressBook1_Alias1 = value;
925 } else {
926#line 222
927 if (index == 2) {
928#line 223
929 __ste_Client_AddressBook1_Alias2 = value;
930 } else {
931
932 }
933 }
934 }
935 } else {
936#line 224
937 if (handle == 3) {
938#line 233
939 if (index == 0) {
940#line 227
941 __ste_Client_AddressBook2_Alias0 = value;
942 } else {
943#line 228
944 if (index == 1) {
945#line 229
946 __ste_Client_AddressBook2_Alias1 = value;
947 } else {
948#line 230
949 if (index == 2) {
950#line 231
951 __ste_Client_AddressBook2_Alias2 = value;
952 } else {
953
954 }
955 }
956 }
957 } else {
958
959 }
960 }
961 }
962#line 1420 "ClientLib.c"
963 return;
964}
965}
966#line 236 "ClientLib.c"
967int __ste_Client_AddressBook0_Address0 = 0;
968#line 238 "ClientLib.c"
969int __ste_Client_AddressBook0_Address1 = 0;
970#line 240 "ClientLib.c"
971int __ste_Client_AddressBook0_Address2 = 0;
972#line 242 "ClientLib.c"
973int __ste_Client_AddressBook1_Address0 = 0;
974#line 244 "ClientLib.c"
975int __ste_Client_AddressBook1_Address1 = 0;
976#line 246 "ClientLib.c"
977int __ste_Client_AddressBook1_Address2 = 0;
978#line 248 "ClientLib.c"
979int __ste_Client_AddressBook2_Address0 = 0;
980#line 250 "ClientLib.c"
981int __ste_Client_AddressBook2_Address1 = 0;
982#line 252 "ClientLib.c"
983int __ste_Client_AddressBook2_Address2 = 0;
984#line 255 "ClientLib.c"
985int getClientAddressBookAddress(int handle , int index )
986{ int retValue_acc ;
987
988 {
989#line 288
990 if (handle == 1) {
991#line 265 "ClientLib.c"
992 if (index == 0) {
993#line 1462
994 retValue_acc = __ste_Client_AddressBook0_Address0;
995#line 1464
996 return (retValue_acc);
997 } else {
998#line 1466
999 if (index == 1) {
1000#line 1471
1001 retValue_acc = __ste_Client_AddressBook0_Address1;
1002#line 1473
1003 return (retValue_acc);
1004 } else {
1005#line 1475
1006 if (index == 2) {
1007#line 1480
1008 retValue_acc = __ste_Client_AddressBook0_Address2;
1009#line 1482
1010 return (retValue_acc);
1011 } else {
1012#line 1488
1013 retValue_acc = 0;
1014#line 1490
1015 return (retValue_acc);
1016 }
1017 }
1018 }
1019 } else {
1020#line 1492 "ClientLib.c"
1021 if (handle == 2) {
1022#line 275 "ClientLib.c"
1023 if (index == 0) {
1024#line 1500
1025 retValue_acc = __ste_Client_AddressBook1_Address0;
1026#line 1502
1027 return (retValue_acc);
1028 } else {
1029#line 1504
1030 if (index == 1) {
1031#line 1509
1032 retValue_acc = __ste_Client_AddressBook1_Address1;
1033#line 1511
1034 return (retValue_acc);
1035 } else {
1036#line 1513
1037 if (index == 2) {
1038#line 1518
1039 retValue_acc = __ste_Client_AddressBook1_Address2;
1040#line 1520
1041 return (retValue_acc);
1042 } else {
1043#line 1526
1044 retValue_acc = 0;
1045#line 1528
1046 return (retValue_acc);
1047 }
1048 }
1049 }
1050 } else {
1051#line 1530 "ClientLib.c"
1052 if (handle == 3) {
1053#line 285 "ClientLib.c"
1054 if (index == 0) {
1055#line 1538
1056 retValue_acc = __ste_Client_AddressBook2_Address0;
1057#line 1540
1058 return (retValue_acc);
1059 } else {
1060#line 1542
1061 if (index == 1) {
1062#line 1547
1063 retValue_acc = __ste_Client_AddressBook2_Address1;
1064#line 1549
1065 return (retValue_acc);
1066 } else {
1067#line 1551
1068 if (index == 2) {
1069#line 1556
1070 retValue_acc = __ste_Client_AddressBook2_Address2;
1071#line 1558
1072 return (retValue_acc);
1073 } else {
1074#line 1564
1075 retValue_acc = 0;
1076#line 1566
1077 return (retValue_acc);
1078 }
1079 }
1080 }
1081 } else {
1082#line 1572 "ClientLib.c"
1083 retValue_acc = 0;
1084#line 1574
1085 return (retValue_acc);
1086 }
1087 }
1088 }
1089#line 1581 "ClientLib.c"
1090 return (retValue_acc);
1091}
1092}
1093#line 291 "ClientLib.c"
1094void setClientAddressBookAddress(int handle , int index , int value )
1095{
1096
1097 {
1098#line 317
1099 if (handle == 1) {
1100#line 300
1101 if (index == 0) {
1102#line 294
1103 __ste_Client_AddressBook0_Address0 = value;
1104 } else {
1105#line 295
1106 if (index == 1) {
1107#line 296
1108 __ste_Client_AddressBook0_Address1 = value;
1109 } else {
1110#line 297
1111 if (index == 2) {
1112#line 298
1113 __ste_Client_AddressBook0_Address2 = value;
1114 } else {
1115
1116 }
1117 }
1118 }
1119 } else {
1120#line 299
1121 if (handle == 2) {
1122#line 308
1123 if (index == 0) {
1124#line 302
1125 __ste_Client_AddressBook1_Address0 = value;
1126 } else {
1127#line 303
1128 if (index == 1) {
1129#line 304
1130 __ste_Client_AddressBook1_Address1 = value;
1131 } else {
1132#line 305
1133 if (index == 2) {
1134#line 306
1135 __ste_Client_AddressBook1_Address2 = value;
1136 } else {
1137
1138 }
1139 }
1140 }
1141 } else {
1142#line 307
1143 if (handle == 3) {
1144#line 316
1145 if (index == 0) {
1146#line 310
1147 __ste_Client_AddressBook2_Address0 = value;
1148 } else {
1149#line 311
1150 if (index == 1) {
1151#line 312
1152 __ste_Client_AddressBook2_Address1 = value;
1153 } else {
1154#line 313
1155 if (index == 2) {
1156#line 314
1157 __ste_Client_AddressBook2_Address2 = value;
1158 } else {
1159
1160 }
1161 }
1162 }
1163 } else {
1164
1165 }
1166 }
1167 }
1168#line 1649 "ClientLib.c"
1169 return;
1170}
1171}
1172#line 319 "ClientLib.c"
1173int __ste_client_autoResponse0 = 0;
1174#line 321 "ClientLib.c"
1175int __ste_client_autoResponse1 = 0;
1176#line 323 "ClientLib.c"
1177int __ste_client_autoResponse2 = 0;
1178#line 326 "ClientLib.c"
1179int getClientAutoResponse(int handle )
1180{ int retValue_acc ;
1181
1182 {
1183#line 335 "ClientLib.c"
1184 if (handle == 1) {
1185#line 1676
1186 retValue_acc = __ste_client_autoResponse0;
1187#line 1678
1188 return (retValue_acc);
1189 } else {
1190#line 1680
1191 if (handle == 2) {
1192#line 1685
1193 retValue_acc = __ste_client_autoResponse1;
1194#line 1687
1195 return (retValue_acc);
1196 } else {
1197#line 1689
1198 if (handle == 3) {
1199#line 1694
1200 retValue_acc = __ste_client_autoResponse2;
1201#line 1696
1202 return (retValue_acc);
1203 } else {
1204#line 1702 "ClientLib.c"
1205 retValue_acc = -1;
1206#line 1704
1207 return (retValue_acc);
1208 }
1209 }
1210 }
1211#line 1711 "ClientLib.c"
1212 return (retValue_acc);
1213}
1214}
1215#line 338 "ClientLib.c"
1216void setClientAutoResponse(int handle , int value )
1217{
1218
1219 {
1220#line 346
1221 if (handle == 1) {
1222#line 340
1223 __ste_client_autoResponse0 = value;
1224 } else {
1225#line 341
1226 if (handle == 2) {
1227#line 342
1228 __ste_client_autoResponse1 = value;
1229 } else {
1230#line 343
1231 if (handle == 3) {
1232#line 344
1233 __ste_client_autoResponse2 = value;
1234 } else {
1235
1236 }
1237 }
1238 }
1239#line 1746 "ClientLib.c"
1240 return;
1241}
1242}
1243#line 348 "ClientLib.c"
1244int __ste_client_privateKey0 = 0;
1245#line 350 "ClientLib.c"
1246int __ste_client_privateKey1 = 0;
1247#line 352 "ClientLib.c"
1248int __ste_client_privateKey2 = 0;
1249#line 355 "ClientLib.c"
1250int getClientPrivateKey(int handle )
1251{ int retValue_acc ;
1252
1253 {
1254#line 364 "ClientLib.c"
1255 if (handle == 1) {
1256#line 1773
1257 retValue_acc = __ste_client_privateKey0;
1258#line 1775
1259 return (retValue_acc);
1260 } else {
1261#line 1777
1262 if (handle == 2) {
1263#line 1782
1264 retValue_acc = __ste_client_privateKey1;
1265#line 1784
1266 return (retValue_acc);
1267 } else {
1268#line 1786
1269 if (handle == 3) {
1270#line 1791
1271 retValue_acc = __ste_client_privateKey2;
1272#line 1793
1273 return (retValue_acc);
1274 } else {
1275#line 1799 "ClientLib.c"
1276 retValue_acc = 0;
1277#line 1801
1278 return (retValue_acc);
1279 }
1280 }
1281 }
1282#line 1808 "ClientLib.c"
1283 return (retValue_acc);
1284}
1285}
1286#line 367 "ClientLib.c"
1287void setClientPrivateKey(int handle , int value )
1288{
1289
1290 {
1291#line 375
1292 if (handle == 1) {
1293#line 369
1294 __ste_client_privateKey0 = value;
1295 } else {
1296#line 370
1297 if (handle == 2) {
1298#line 371
1299 __ste_client_privateKey1 = value;
1300 } else {
1301#line 372
1302 if (handle == 3) {
1303#line 373
1304 __ste_client_privateKey2 = value;
1305 } else {
1306
1307 }
1308 }
1309 }
1310#line 1843 "ClientLib.c"
1311 return;
1312}
1313}
1314#line 377 "ClientLib.c"
1315int __ste_ClientKeyring_size0 = 0;
1316#line 379 "ClientLib.c"
1317int __ste_ClientKeyring_size1 = 0;
1318#line 381 "ClientLib.c"
1319int __ste_ClientKeyring_size2 = 0;
1320#line 384 "ClientLib.c"
1321int getClientKeyringSize(int handle )
1322{ int retValue_acc ;
1323
1324 {
1325#line 393 "ClientLib.c"
1326 if (handle == 1) {
1327#line 1870
1328 retValue_acc = __ste_ClientKeyring_size0;
1329#line 1872
1330 return (retValue_acc);
1331 } else {
1332#line 1874
1333 if (handle == 2) {
1334#line 1879
1335 retValue_acc = __ste_ClientKeyring_size1;
1336#line 1881
1337 return (retValue_acc);
1338 } else {
1339#line 1883
1340 if (handle == 3) {
1341#line 1888
1342 retValue_acc = __ste_ClientKeyring_size2;
1343#line 1890
1344 return (retValue_acc);
1345 } else {
1346#line 1896 "ClientLib.c"
1347 retValue_acc = 0;
1348#line 1898
1349 return (retValue_acc);
1350 }
1351 }
1352 }
1353#line 1905 "ClientLib.c"
1354 return (retValue_acc);
1355}
1356}
1357#line 396 "ClientLib.c"
1358void setClientKeyringSize(int handle , int value )
1359{
1360
1361 {
1362#line 404
1363 if (handle == 1) {
1364#line 398
1365 __ste_ClientKeyring_size0 = value;
1366 } else {
1367#line 399
1368 if (handle == 2) {
1369#line 400
1370 __ste_ClientKeyring_size1 = value;
1371 } else {
1372#line 401
1373 if (handle == 3) {
1374#line 402
1375 __ste_ClientKeyring_size2 = value;
1376 } else {
1377
1378 }
1379 }
1380 }
1381#line 1940 "ClientLib.c"
1382 return;
1383}
1384}
1385#line 406 "ClientLib.c"
1386int createClientKeyringEntry(int handle )
1387{ int retValue_acc ;
1388 int size ;
1389 int tmp ;
1390 int __cil_tmp5 ;
1391
1392 {
1393 {
1394#line 407
1395 tmp = getClientKeyringSize(handle);
1396#line 407
1397 size = tmp;
1398 }
1399#line 408 "ClientLib.c"
1400 if (size < 2) {
1401 {
1402#line 409 "ClientLib.c"
1403 __cil_tmp5 = size + 1;
1404#line 409
1405 setClientKeyringSize(handle, __cil_tmp5);
1406#line 1967 "ClientLib.c"
1407 retValue_acc = size + 1;
1408 }
1409#line 1969
1410 return (retValue_acc);
1411 } else {
1412#line 1973 "ClientLib.c"
1413 retValue_acc = -1;
1414#line 1975
1415 return (retValue_acc);
1416 }
1417#line 1982 "ClientLib.c"
1418 return (retValue_acc);
1419}
1420}
1421#line 414 "ClientLib.c"
1422int __ste_Client_Keyring0_User0 = 0;
1423#line 416 "ClientLib.c"
1424int __ste_Client_Keyring0_User1 = 0;
1425#line 418 "ClientLib.c"
1426int __ste_Client_Keyring0_User2 = 0;
1427#line 420 "ClientLib.c"
1428int __ste_Client_Keyring1_User0 = 0;
1429#line 422 "ClientLib.c"
1430int __ste_Client_Keyring1_User1 = 0;
1431#line 424 "ClientLib.c"
1432int __ste_Client_Keyring1_User2 = 0;
1433#line 426 "ClientLib.c"
1434int __ste_Client_Keyring2_User0 = 0;
1435#line 428 "ClientLib.c"
1436int __ste_Client_Keyring2_User1 = 0;
1437#line 430 "ClientLib.c"
1438int __ste_Client_Keyring2_User2 = 0;
1439#line 433 "ClientLib.c"
1440int getClientKeyringUser(int handle , int index )
1441{ int retValue_acc ;
1442
1443 {
1444#line 466
1445 if (handle == 1) {
1446#line 443 "ClientLib.c"
1447 if (index == 0) {
1448#line 2028
1449 retValue_acc = __ste_Client_Keyring0_User0;
1450#line 2030
1451 return (retValue_acc);
1452 } else {
1453#line 2032
1454 if (index == 1) {
1455#line 2037
1456 retValue_acc = __ste_Client_Keyring0_User1;
1457#line 2039
1458 return (retValue_acc);
1459 } else {
1460#line 2045
1461 retValue_acc = 0;
1462#line 2047
1463 return (retValue_acc);
1464 }
1465 }
1466 } else {
1467#line 2049 "ClientLib.c"
1468 if (handle == 2) {
1469#line 453 "ClientLib.c"
1470 if (index == 0) {
1471#line 2057
1472 retValue_acc = __ste_Client_Keyring1_User0;
1473#line 2059
1474 return (retValue_acc);
1475 } else {
1476#line 2061
1477 if (index == 1) {
1478#line 2066
1479 retValue_acc = __ste_Client_Keyring1_User1;
1480#line 2068
1481 return (retValue_acc);
1482 } else {
1483#line 2074
1484 retValue_acc = 0;
1485#line 2076
1486 return (retValue_acc);
1487 }
1488 }
1489 } else {
1490#line 2078 "ClientLib.c"
1491 if (handle == 3) {
1492#line 463 "ClientLib.c"
1493 if (index == 0) {
1494#line 2086
1495 retValue_acc = __ste_Client_Keyring2_User0;
1496#line 2088
1497 return (retValue_acc);
1498 } else {
1499#line 2090
1500 if (index == 1) {
1501#line 2095
1502 retValue_acc = __ste_Client_Keyring2_User1;
1503#line 2097
1504 return (retValue_acc);
1505 } else {
1506#line 2103
1507 retValue_acc = 0;
1508#line 2105
1509 return (retValue_acc);
1510 }
1511 }
1512 } else {
1513#line 2111 "ClientLib.c"
1514 retValue_acc = 0;
1515#line 2113
1516 return (retValue_acc);
1517 }
1518 }
1519 }
1520#line 2120 "ClientLib.c"
1521 return (retValue_acc);
1522}
1523}
1524#line 473 "ClientLib.c"
1525void setClientKeyringUser(int handle , int index , int value )
1526{
1527
1528 {
1529#line 499
1530 if (handle == 1) {
1531#line 482
1532 if (index == 0) {
1533#line 476
1534 __ste_Client_Keyring0_User0 = value;
1535 } else {
1536#line 477
1537 if (index == 1) {
1538#line 478
1539 __ste_Client_Keyring0_User1 = value;
1540 } else {
1541
1542 }
1543 }
1544 } else {
1545#line 479
1546 if (handle == 2) {
1547#line 490
1548 if (index == 0) {
1549#line 484
1550 __ste_Client_Keyring1_User0 = value;
1551 } else {
1552#line 485
1553 if (index == 1) {
1554#line 486
1555 __ste_Client_Keyring1_User1 = value;
1556 } else {
1557
1558 }
1559 }
1560 } else {
1561#line 487
1562 if (handle == 3) {
1563#line 498
1564 if (index == 0) {
1565#line 492
1566 __ste_Client_Keyring2_User0 = value;
1567 } else {
1568#line 493
1569 if (index == 1) {
1570#line 494
1571 __ste_Client_Keyring2_User1 = value;
1572 } else {
1573
1574 }
1575 }
1576 } else {
1577
1578 }
1579 }
1580 }
1581#line 2176 "ClientLib.c"
1582 return;
1583}
1584}
1585#line 501 "ClientLib.c"
1586int __ste_Client_Keyring0_PublicKey0 = 0;
1587#line 503 "ClientLib.c"
1588int __ste_Client_Keyring0_PublicKey1 = 0;
1589#line 505 "ClientLib.c"
1590int __ste_Client_Keyring0_PublicKey2 = 0;
1591#line 507 "ClientLib.c"
1592int __ste_Client_Keyring1_PublicKey0 = 0;
1593#line 509 "ClientLib.c"
1594int __ste_Client_Keyring1_PublicKey1 = 0;
1595#line 511 "ClientLib.c"
1596int __ste_Client_Keyring1_PublicKey2 = 0;
1597#line 513 "ClientLib.c"
1598int __ste_Client_Keyring2_PublicKey0 = 0;
1599#line 515 "ClientLib.c"
1600int __ste_Client_Keyring2_PublicKey1 = 0;
1601#line 517 "ClientLib.c"
1602int __ste_Client_Keyring2_PublicKey2 = 0;
1603#line 520 "ClientLib.c"
1604int getClientKeyringPublicKey(int handle , int index )
1605{ int retValue_acc ;
1606
1607 {
1608#line 553
1609 if (handle == 1) {
1610#line 530 "ClientLib.c"
1611 if (index == 0) {
1612#line 2218
1613 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1614#line 2220
1615 return (retValue_acc);
1616 } else {
1617#line 2222
1618 if (index == 1) {
1619#line 2227
1620 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1621#line 2229
1622 return (retValue_acc);
1623 } else {
1624#line 2235
1625 retValue_acc = 0;
1626#line 2237
1627 return (retValue_acc);
1628 }
1629 }
1630 } else {
1631#line 2239 "ClientLib.c"
1632 if (handle == 2) {
1633#line 540 "ClientLib.c"
1634 if (index == 0) {
1635#line 2247
1636 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1637#line 2249
1638 return (retValue_acc);
1639 } else {
1640#line 2251
1641 if (index == 1) {
1642#line 2256
1643 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1644#line 2258
1645 return (retValue_acc);
1646 } else {
1647#line 2264
1648 retValue_acc = 0;
1649#line 2266
1650 return (retValue_acc);
1651 }
1652 }
1653 } else {
1654#line 2268 "ClientLib.c"
1655 if (handle == 3) {
1656#line 550 "ClientLib.c"
1657 if (index == 0) {
1658#line 2276
1659 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1660#line 2278
1661 return (retValue_acc);
1662 } else {
1663#line 2280
1664 if (index == 1) {
1665#line 2285
1666 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1667#line 2287
1668 return (retValue_acc);
1669 } else {
1670#line 2293
1671 retValue_acc = 0;
1672#line 2295
1673 return (retValue_acc);
1674 }
1675 }
1676 } else {
1677#line 2301 "ClientLib.c"
1678 retValue_acc = 0;
1679#line 2303
1680 return (retValue_acc);
1681 }
1682 }
1683 }
1684#line 2310 "ClientLib.c"
1685 return (retValue_acc);
1686}
1687}
1688#line 557 "ClientLib.c"
1689int findPublicKey(int handle , int userid )
1690{ int retValue_acc ;
1691
1692 {
1693#line 591
1694 if (handle == 1) {
1695#line 568 "ClientLib.c"
1696 if (userid == __ste_Client_Keyring0_User0) {
1697#line 2338
1698 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1699#line 2340
1700 return (retValue_acc);
1701 } else {
1702#line 2342
1703 if (userid == __ste_Client_Keyring0_User1) {
1704#line 2347
1705 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1706#line 2349
1707 return (retValue_acc);
1708 } else {
1709#line 2355
1710 retValue_acc = 0;
1711#line 2357
1712 return (retValue_acc);
1713 }
1714 }
1715 } else {
1716#line 2359 "ClientLib.c"
1717 if (handle == 2) {
1718#line 578 "ClientLib.c"
1719 if (userid == __ste_Client_Keyring1_User0) {
1720#line 2367
1721 retValue_acc = __ste_Client_Keyring1_PublicKey0;
1722#line 2369
1723 return (retValue_acc);
1724 } else {
1725#line 2371
1726 if (userid == __ste_Client_Keyring1_User1) {
1727#line 2376
1728 retValue_acc = __ste_Client_Keyring1_PublicKey1;
1729#line 2378
1730 return (retValue_acc);
1731 } else {
1732#line 2384
1733 retValue_acc = 0;
1734#line 2386
1735 return (retValue_acc);
1736 }
1737 }
1738 } else {
1739#line 2388 "ClientLib.c"
1740 if (handle == 3) {
1741#line 588 "ClientLib.c"
1742 if (userid == __ste_Client_Keyring2_User0) {
1743#line 2396
1744 retValue_acc = __ste_Client_Keyring2_PublicKey0;
1745#line 2398
1746 return (retValue_acc);
1747 } else {
1748#line 2400
1749 if (userid == __ste_Client_Keyring2_User1) {
1750#line 2405
1751 retValue_acc = __ste_Client_Keyring2_PublicKey1;
1752#line 2407
1753 return (retValue_acc);
1754 } else {
1755#line 2413
1756 retValue_acc = 0;
1757#line 2415
1758 return (retValue_acc);
1759 }
1760 }
1761 } else {
1762#line 2421 "ClientLib.c"
1763 retValue_acc = 0;
1764#line 2423
1765 return (retValue_acc);
1766 }
1767 }
1768 }
1769#line 2430 "ClientLib.c"
1770 return (retValue_acc);
1771}
1772}
1773#line 595 "ClientLib.c"
1774void setClientKeyringPublicKey(int handle , int index , int value )
1775{
1776
1777 {
1778#line 621
1779 if (handle == 1) {
1780#line 604
1781 if (index == 0) {
1782#line 598
1783 __ste_Client_Keyring0_PublicKey0 = value;
1784 } else {
1785#line 599
1786 if (index == 1) {
1787#line 600
1788 __ste_Client_Keyring0_PublicKey1 = value;
1789 } else {
1790
1791 }
1792 }
1793 } else {
1794#line 601
1795 if (handle == 2) {
1796#line 612
1797 if (index == 0) {
1798#line 606
1799 __ste_Client_Keyring1_PublicKey0 = value;
1800 } else {
1801#line 607
1802 if (index == 1) {
1803#line 608
1804 __ste_Client_Keyring1_PublicKey1 = value;
1805 } else {
1806
1807 }
1808 }
1809 } else {
1810#line 609
1811 if (handle == 3) {
1812#line 620
1813 if (index == 0) {
1814#line 614
1815 __ste_Client_Keyring2_PublicKey0 = value;
1816 } else {
1817#line 615
1818 if (index == 1) {
1819#line 616
1820 __ste_Client_Keyring2_PublicKey1 = value;
1821 } else {
1822
1823 }
1824 }
1825 } else {
1826
1827 }
1828 }
1829 }
1830#line 2486 "ClientLib.c"
1831 return;
1832}
1833}
1834#line 623 "ClientLib.c"
1835int __ste_client_forwardReceiver0 = 0;
1836#line 625 "ClientLib.c"
1837int __ste_client_forwardReceiver1 = 0;
1838#line 627 "ClientLib.c"
1839int __ste_client_forwardReceiver2 = 0;
1840#line 629 "ClientLib.c"
1841int __ste_client_forwardReceiver3 = 0;
1842#line 631 "ClientLib.c"
1843int getClientForwardReceiver(int handle )
1844{ int retValue_acc ;
1845
1846 {
1847#line 640 "ClientLib.c"
1848 if (handle == 1) {
1849#line 2515
1850 retValue_acc = __ste_client_forwardReceiver0;
1851#line 2517
1852 return (retValue_acc);
1853 } else {
1854#line 2519
1855 if (handle == 2) {
1856#line 2524
1857 retValue_acc = __ste_client_forwardReceiver1;
1858#line 2526
1859 return (retValue_acc);
1860 } else {
1861#line 2528
1862 if (handle == 3) {
1863#line 2533
1864 retValue_acc = __ste_client_forwardReceiver2;
1865#line 2535
1866 return (retValue_acc);
1867 } else {
1868#line 2541 "ClientLib.c"
1869 retValue_acc = 0;
1870#line 2543
1871 return (retValue_acc);
1872 }
1873 }
1874 }
1875#line 2550 "ClientLib.c"
1876 return (retValue_acc);
1877}
1878}
1879#line 643 "ClientLib.c"
1880void setClientForwardReceiver(int handle , int value )
1881{
1882
1883 {
1884#line 651
1885 if (handle == 1) {
1886#line 645
1887 __ste_client_forwardReceiver0 = value;
1888 } else {
1889#line 646
1890 if (handle == 2) {
1891#line 647
1892 __ste_client_forwardReceiver1 = value;
1893 } else {
1894#line 648
1895 if (handle == 3) {
1896#line 649
1897 __ste_client_forwardReceiver2 = value;
1898 } else {
1899
1900 }
1901 }
1902 }
1903#line 2585 "ClientLib.c"
1904 return;
1905}
1906}
1907#line 653 "ClientLib.c"
1908int __ste_client_idCounter0 = 0;
1909#line 655 "ClientLib.c"
1910int __ste_client_idCounter1 = 0;
1911#line 657 "ClientLib.c"
1912int __ste_client_idCounter2 = 0;
1913#line 660 "ClientLib.c"
1914int getClientId(int handle )
1915{ int retValue_acc ;
1916
1917 {
1918#line 669 "ClientLib.c"
1919 if (handle == 1) {
1920#line 2612
1921 retValue_acc = __ste_client_idCounter0;
1922#line 2614
1923 return (retValue_acc);
1924 } else {
1925#line 2616
1926 if (handle == 2) {
1927#line 2621
1928 retValue_acc = __ste_client_idCounter1;
1929#line 2623
1930 return (retValue_acc);
1931 } else {
1932#line 2625
1933 if (handle == 3) {
1934#line 2630
1935 retValue_acc = __ste_client_idCounter2;
1936#line 2632
1937 return (retValue_acc);
1938 } else {
1939#line 2638 "ClientLib.c"
1940 retValue_acc = 0;
1941#line 2640
1942 return (retValue_acc);
1943 }
1944 }
1945 }
1946#line 2647 "ClientLib.c"
1947 return (retValue_acc);
1948}
1949}
1950#line 672 "ClientLib.c"
1951void setClientId(int handle , int value )
1952{
1953
1954 {
1955#line 680
1956 if (handle == 1) {
1957#line 674
1958 __ste_client_idCounter0 = value;
1959 } else {
1960#line 675
1961 if (handle == 2) {
1962#line 676
1963 __ste_client_idCounter1 = value;
1964 } else {
1965#line 677
1966 if (handle == 3) {
1967#line 678
1968 __ste_client_idCounter2 = value;
1969 } else {
1970
1971 }
1972 }
1973 }
1974#line 2682 "ClientLib.c"
1975 return;
1976}
1977}
1978#line 1 "libacc.o"
1979#pragma merger(0,"libacc.i","")
1980#line 73 "/usr/include/assert.h"
1981extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
1982 char const *__file ,
1983 unsigned int __line ,
1984 char const *__function ) ;
1985#line 471 "/usr/include/stdlib.h"
1986extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
1987#line 488
1988extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
1989#line 32 "libacc.c"
1990void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
1991 int ) ,
1992 int val )
1993{ struct __UTAC__EXCEPTION *excep ;
1994 struct __UTAC__CFLOW_FUNC *cf ;
1995 void *tmp ;
1996 unsigned long __cil_tmp7 ;
1997 unsigned long __cil_tmp8 ;
1998 unsigned long __cil_tmp9 ;
1999 unsigned long __cil_tmp10 ;
2000 unsigned long __cil_tmp11 ;
2001 unsigned long __cil_tmp12 ;
2002 unsigned long __cil_tmp13 ;
2003 unsigned long __cil_tmp14 ;
2004 int (**mem_15)(int , int ) ;
2005 int *mem_16 ;
2006 struct __UTAC__CFLOW_FUNC **mem_17 ;
2007 struct __UTAC__CFLOW_FUNC **mem_18 ;
2008 struct __UTAC__CFLOW_FUNC **mem_19 ;
2009
2010 {
2011 {
2012#line 33
2013 excep = (struct __UTAC__EXCEPTION *)exception;
2014#line 34
2015 tmp = malloc(24UL);
2016#line 34
2017 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
2018#line 36
2019 mem_15 = (int (**)(int , int ))cf;
2020#line 36
2021 *mem_15 = cflow_func;
2022#line 37
2023 __cil_tmp7 = (unsigned long )cf;
2024#line 37
2025 __cil_tmp8 = __cil_tmp7 + 8;
2026#line 37
2027 mem_16 = (int *)__cil_tmp8;
2028#line 37
2029 *mem_16 = val;
2030#line 38
2031 __cil_tmp9 = (unsigned long )cf;
2032#line 38
2033 __cil_tmp10 = __cil_tmp9 + 16;
2034#line 38
2035 __cil_tmp11 = (unsigned long )excep;
2036#line 38
2037 __cil_tmp12 = __cil_tmp11 + 24;
2038#line 38
2039 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
2040#line 38
2041 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
2042#line 38
2043 *mem_17 = *mem_18;
2044#line 39
2045 __cil_tmp13 = (unsigned long )excep;
2046#line 39
2047 __cil_tmp14 = __cil_tmp13 + 24;
2048#line 39
2049 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2050#line 39
2051 *mem_19 = cf;
2052 }
2053#line 654 "libacc.c"
2054 return;
2055}
2056}
2057#line 44 "libacc.c"
2058void __utac__exception__cf_handler_free(void *exception )
2059{ struct __UTAC__EXCEPTION *excep ;
2060 struct __UTAC__CFLOW_FUNC *cf ;
2061 struct __UTAC__CFLOW_FUNC *tmp ;
2062 unsigned long __cil_tmp5 ;
2063 unsigned long __cil_tmp6 ;
2064 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2065 unsigned long __cil_tmp8 ;
2066 unsigned long __cil_tmp9 ;
2067 unsigned long __cil_tmp10 ;
2068 unsigned long __cil_tmp11 ;
2069 void *__cil_tmp12 ;
2070 unsigned long __cil_tmp13 ;
2071 unsigned long __cil_tmp14 ;
2072 struct __UTAC__CFLOW_FUNC **mem_15 ;
2073 struct __UTAC__CFLOW_FUNC **mem_16 ;
2074 struct __UTAC__CFLOW_FUNC **mem_17 ;
2075
2076 {
2077#line 45
2078 excep = (struct __UTAC__EXCEPTION *)exception;
2079#line 46
2080 __cil_tmp5 = (unsigned long )excep;
2081#line 46
2082 __cil_tmp6 = __cil_tmp5 + 24;
2083#line 46
2084 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2085#line 46
2086 cf = *mem_15;
2087 {
2088#line 49
2089 while (1) {
2090 while_0_continue: ;
2091 {
2092#line 49
2093 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2094#line 49
2095 __cil_tmp8 = (unsigned long )__cil_tmp7;
2096#line 49
2097 __cil_tmp9 = (unsigned long )cf;
2098#line 49
2099 if (__cil_tmp9 != __cil_tmp8) {
2100
2101 } else {
2102 goto while_0_break;
2103 }
2104 }
2105 {
2106#line 50
2107 tmp = cf;
2108#line 51
2109 __cil_tmp10 = (unsigned long )cf;
2110#line 51
2111 __cil_tmp11 = __cil_tmp10 + 16;
2112#line 51
2113 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
2114#line 51
2115 cf = *mem_16;
2116#line 52
2117 __cil_tmp12 = (void *)tmp;
2118#line 52
2119 free(__cil_tmp12);
2120 }
2121 }
2122 while_0_break: ;
2123 }
2124#line 55
2125 __cil_tmp13 = (unsigned long )excep;
2126#line 55
2127 __cil_tmp14 = __cil_tmp13 + 24;
2128#line 55
2129 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
2130#line 55
2131 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
2132#line 694 "libacc.c"
2133 return;
2134}
2135}
2136#line 59 "libacc.c"
2137void __utac__exception__cf_handler_reset(void *exception )
2138{ struct __UTAC__EXCEPTION *excep ;
2139 struct __UTAC__CFLOW_FUNC *cf ;
2140 unsigned long __cil_tmp5 ;
2141 unsigned long __cil_tmp6 ;
2142 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
2143 unsigned long __cil_tmp8 ;
2144 unsigned long __cil_tmp9 ;
2145 int (*__cil_tmp10)(int , int ) ;
2146 unsigned long __cil_tmp11 ;
2147 unsigned long __cil_tmp12 ;
2148 int __cil_tmp13 ;
2149 unsigned long __cil_tmp14 ;
2150 unsigned long __cil_tmp15 ;
2151 struct __UTAC__CFLOW_FUNC **mem_16 ;
2152 int (**mem_17)(int , int ) ;
2153 int *mem_18 ;
2154 struct __UTAC__CFLOW_FUNC **mem_19 ;
2155
2156 {
2157#line 60
2158 excep = (struct __UTAC__EXCEPTION *)exception;
2159#line 61
2160 __cil_tmp5 = (unsigned long )excep;
2161#line 61
2162 __cil_tmp6 = __cil_tmp5 + 24;
2163#line 61
2164 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
2165#line 61
2166 cf = *mem_16;
2167 {
2168#line 64
2169 while (1) {
2170 while_1_continue: ;
2171 {
2172#line 64
2173 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
2174#line 64
2175 __cil_tmp8 = (unsigned long )__cil_tmp7;
2176#line 64
2177 __cil_tmp9 = (unsigned long )cf;
2178#line 64
2179 if (__cil_tmp9 != __cil_tmp8) {
2180
2181 } else {
2182 goto while_1_break;
2183 }
2184 }
2185 {
2186#line 65
2187 mem_17 = (int (**)(int , int ))cf;
2188#line 65
2189 __cil_tmp10 = *mem_17;
2190#line 65
2191 __cil_tmp11 = (unsigned long )cf;
2192#line 65
2193 __cil_tmp12 = __cil_tmp11 + 8;
2194#line 65
2195 mem_18 = (int *)__cil_tmp12;
2196#line 65
2197 __cil_tmp13 = *mem_18;
2198#line 65
2199 (*__cil_tmp10)(4, __cil_tmp13);
2200#line 66
2201 __cil_tmp14 = (unsigned long )cf;
2202#line 66
2203 __cil_tmp15 = __cil_tmp14 + 16;
2204#line 66
2205 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
2206#line 66
2207 cf = *mem_19;
2208 }
2209 }
2210 while_1_break: ;
2211 }
2212 {
2213#line 69
2214 __utac__exception__cf_handler_free(exception);
2215 }
2216#line 732 "libacc.c"
2217 return;
2218}
2219}
2220#line 80 "libacc.c"
2221void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
2222#line 80 "libacc.c"
2223static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
2224#line 79 "libacc.c"
2225void *__utac__error_stack_mgt(void *env , int mode , int count )
2226{ void *retValue_acc ;
2227 struct __ACC__ERR *new ;
2228 void *tmp ;
2229 struct __ACC__ERR *temp ;
2230 struct __ACC__ERR *next ;
2231 void *excep ;
2232 unsigned long __cil_tmp10 ;
2233 unsigned long __cil_tmp11 ;
2234 unsigned long __cil_tmp12 ;
2235 unsigned long __cil_tmp13 ;
2236 void *__cil_tmp14 ;
2237 unsigned long __cil_tmp15 ;
2238 unsigned long __cil_tmp16 ;
2239 void *__cil_tmp17 ;
2240 void **mem_18 ;
2241 struct __ACC__ERR **mem_19 ;
2242 struct __ACC__ERR **mem_20 ;
2243 void **mem_21 ;
2244 struct __ACC__ERR **mem_22 ;
2245 void **mem_23 ;
2246 void **mem_24 ;
2247
2248 {
2249#line 82 "libacc.c"
2250 if (count == 0) {
2251#line 758 "libacc.c"
2252 return (retValue_acc);
2253 } else {
2254
2255 }
2256#line 86 "libacc.c"
2257 if (mode == 0) {
2258 {
2259#line 87
2260 tmp = malloc(16UL);
2261#line 87
2262 new = (struct __ACC__ERR *)tmp;
2263#line 88
2264 mem_18 = (void **)new;
2265#line 88
2266 *mem_18 = env;
2267#line 89
2268 __cil_tmp10 = (unsigned long )new;
2269#line 89
2270 __cil_tmp11 = __cil_tmp10 + 8;
2271#line 89
2272 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
2273#line 89
2274 *mem_19 = head;
2275#line 90
2276 head = new;
2277#line 776 "libacc.c"
2278 retValue_acc = (void *)new;
2279 }
2280#line 778
2281 return (retValue_acc);
2282 } else {
2283
2284 }
2285#line 94 "libacc.c"
2286 if (mode == 1) {
2287#line 95
2288 temp = head;
2289 {
2290#line 98
2291 while (1) {
2292 while_2_continue: ;
2293#line 98
2294 if (count > 1) {
2295
2296 } else {
2297 goto while_2_break;
2298 }
2299 {
2300#line 99
2301 __cil_tmp12 = (unsigned long )temp;
2302#line 99
2303 __cil_tmp13 = __cil_tmp12 + 8;
2304#line 99
2305 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
2306#line 99
2307 next = *mem_20;
2308#line 100
2309 mem_21 = (void **)temp;
2310#line 100
2311 excep = *mem_21;
2312#line 101
2313 __cil_tmp14 = (void *)temp;
2314#line 101
2315 free(__cil_tmp14);
2316#line 102
2317 __utac__exception__cf_handler_reset(excep);
2318#line 103
2319 temp = next;
2320#line 104
2321 count = count - 1;
2322 }
2323 }
2324 while_2_break: ;
2325 }
2326 {
2327#line 107
2328 __cil_tmp15 = (unsigned long )temp;
2329#line 107
2330 __cil_tmp16 = __cil_tmp15 + 8;
2331#line 107
2332 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
2333#line 107
2334 head = *mem_22;
2335#line 108
2336 mem_23 = (void **)temp;
2337#line 108
2338 excep = *mem_23;
2339#line 109
2340 __cil_tmp17 = (void *)temp;
2341#line 109
2342 free(__cil_tmp17);
2343#line 110
2344 __utac__exception__cf_handler_reset(excep);
2345#line 820 "libacc.c"
2346 retValue_acc = excep;
2347 }
2348#line 822
2349 return (retValue_acc);
2350 } else {
2351
2352 }
2353#line 114
2354 if (mode == 2) {
2355#line 118 "libacc.c"
2356 if (head) {
2357#line 831
2358 mem_24 = (void **)head;
2359#line 831
2360 retValue_acc = *mem_24;
2361#line 833
2362 return (retValue_acc);
2363 } else {
2364#line 837 "libacc.c"
2365 retValue_acc = (void *)0;
2366#line 839
2367 return (retValue_acc);
2368 }
2369 } else {
2370
2371 }
2372#line 846 "libacc.c"
2373 return (retValue_acc);
2374}
2375}
2376#line 122 "libacc.c"
2377void *__utac__get_this_arg(int i , struct JoinPoint *this )
2378{ void *retValue_acc ;
2379 unsigned long __cil_tmp4 ;
2380 unsigned long __cil_tmp5 ;
2381 int __cil_tmp6 ;
2382 int __cil_tmp7 ;
2383 unsigned long __cil_tmp8 ;
2384 unsigned long __cil_tmp9 ;
2385 void **__cil_tmp10 ;
2386 void **__cil_tmp11 ;
2387 int *mem_12 ;
2388 void ***mem_13 ;
2389
2390 {
2391#line 123
2392 if (i > 0) {
2393 {
2394#line 123
2395 __cil_tmp4 = (unsigned long )this;
2396#line 123
2397 __cil_tmp5 = __cil_tmp4 + 16;
2398#line 123
2399 mem_12 = (int *)__cil_tmp5;
2400#line 123
2401 __cil_tmp6 = *mem_12;
2402#line 123
2403 if (i <= __cil_tmp6) {
2404
2405 } else {
2406 {
2407#line 123
2408 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2409 123U, "__utac__get_this_arg");
2410 }
2411 }
2412 }
2413 } else {
2414 {
2415#line 123
2416 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2417 123U, "__utac__get_this_arg");
2418 }
2419 }
2420#line 870 "libacc.c"
2421 __cil_tmp7 = i - 1;
2422#line 870
2423 __cil_tmp8 = (unsigned long )this;
2424#line 870
2425 __cil_tmp9 = __cil_tmp8 + 8;
2426#line 870
2427 mem_13 = (void ***)__cil_tmp9;
2428#line 870
2429 __cil_tmp10 = *mem_13;
2430#line 870
2431 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2432#line 870
2433 retValue_acc = *__cil_tmp11;
2434#line 872
2435 return (retValue_acc);
2436#line 879
2437 return (retValue_acc);
2438}
2439}
2440#line 129 "libacc.c"
2441char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
2442{ char const *retValue_acc ;
2443 unsigned long __cil_tmp4 ;
2444 unsigned long __cil_tmp5 ;
2445 int __cil_tmp6 ;
2446 int __cil_tmp7 ;
2447 unsigned long __cil_tmp8 ;
2448 unsigned long __cil_tmp9 ;
2449 char const **__cil_tmp10 ;
2450 char const **__cil_tmp11 ;
2451 int *mem_12 ;
2452 char const ***mem_13 ;
2453
2454 {
2455#line 131
2456 if (i > 0) {
2457 {
2458#line 131
2459 __cil_tmp4 = (unsigned long )this;
2460#line 131
2461 __cil_tmp5 = __cil_tmp4 + 16;
2462#line 131
2463 mem_12 = (int *)__cil_tmp5;
2464#line 131
2465 __cil_tmp6 = *mem_12;
2466#line 131
2467 if (i <= __cil_tmp6) {
2468
2469 } else {
2470 {
2471#line 131
2472 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2473 131U, "__utac__get_this_argtype");
2474 }
2475 }
2476 }
2477 } else {
2478 {
2479#line 131
2480 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
2481 131U, "__utac__get_this_argtype");
2482 }
2483 }
2484#line 903 "libacc.c"
2485 __cil_tmp7 = i - 1;
2486#line 903
2487 __cil_tmp8 = (unsigned long )this;
2488#line 903
2489 __cil_tmp9 = __cil_tmp8 + 24;
2490#line 903
2491 mem_13 = (char const ***)__cil_tmp9;
2492#line 903
2493 __cil_tmp10 = *mem_13;
2494#line 903
2495 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
2496#line 903
2497 retValue_acc = *__cil_tmp11;
2498#line 905
2499 return (retValue_acc);
2500#line 912
2501 return (retValue_acc);
2502}
2503}
2504#line 1 "wsllib_check.o"
2505#pragma merger(0,"wsllib_check.i","")
2506#line 3 "wsllib_check.c"
2507void __automaton_fail(void)
2508{
2509
2510 {
2511 goto ERROR;
2512 ERROR: ;
2513#line 53 "wsllib_check.c"
2514 return;
2515}
2516}
2517#line 1 "featureselect.o"
2518#pragma merger(0,"featureselect.i","")
2519#line 41 "featureselect.h"
2520int select_one(void) ;
2521#line 43
2522void select_features(void) ;
2523#line 45
2524void select_helpers(void) ;
2525#line 47
2526int valid_product(void) ;
2527#line 8 "featureselect.c"
2528int select_one(void)
2529{ int retValue_acc ;
2530 int choice = __VERIFIER_nondet_int();
2531
2532 {
2533#line 84 "featureselect.c"
2534 retValue_acc = choice;
2535#line 86
2536 return (retValue_acc);
2537#line 93
2538 return (retValue_acc);
2539}
2540}
2541#line 14 "featureselect.c"
2542void select_features(void)
2543{
2544
2545 {
2546#line 115 "featureselect.c"
2547 return;
2548}
2549}
2550#line 20 "featureselect.c"
2551void select_helpers(void)
2552{
2553
2554 {
2555#line 133 "featureselect.c"
2556 return;
2557}
2558}
2559#line 25 "featureselect.c"
2560int valid_product(void)
2561{ int retValue_acc ;
2562
2563 {
2564#line 151 "featureselect.c"
2565 retValue_acc = 1;
2566#line 153
2567 return (retValue_acc);
2568#line 160
2569 return (retValue_acc);
2570}
2571}
2572#line 1 "EmailLib.o"
2573#pragma merger(0,"EmailLib.i","")
2574#line 4 "EmailLib.h"
2575int initEmail(void) ;
2576#line 8
2577void setEmailId(int handle , int value ) ;
2578#line 18
2579char *getEmailSubject(int handle ) ;
2580#line 20
2581void setEmailSubject(int handle , char *value ) ;
2582#line 22
2583char *getEmailBody(int handle ) ;
2584#line 24
2585void setEmailBody(int handle , char *value ) ;
2586#line 28
2587void setEmailIsEncrypted(int handle , int value ) ;
2588#line 32
2589void setEmailEncryptionKey(int handle , int value ) ;
2590#line 36
2591void setEmailIsSigned(int handle , int value ) ;
2592#line 40
2593void setEmailSignKey(int handle , int value ) ;
2594#line 44
2595void setEmailIsSignatureVerified(int handle , int value ) ;
2596#line 5 "EmailLib.c"
2597int __ste_Email_counter = 0;
2598#line 7 "EmailLib.c"
2599int initEmail(void)
2600{ int retValue_acc ;
2601
2602 {
2603#line 12 "EmailLib.c"
2604 if (__ste_Email_counter < 2) {
2605#line 670
2606 __ste_Email_counter = __ste_Email_counter + 1;
2607#line 670
2608 retValue_acc = __ste_Email_counter;
2609#line 672
2610 return (retValue_acc);
2611 } else {
2612#line 678 "EmailLib.c"
2613 retValue_acc = -1;
2614#line 680
2615 return (retValue_acc);
2616 }
2617#line 687 "EmailLib.c"
2618 return (retValue_acc);
2619}
2620}
2621#line 15 "EmailLib.c"
2622int __ste_email_id0 = 0;
2623#line 17 "EmailLib.c"
2624int __ste_email_id1 = 0;
2625#line 19 "EmailLib.c"
2626int getEmailId(int handle )
2627{ int retValue_acc ;
2628
2629 {
2630#line 26 "EmailLib.c"
2631 if (handle == 1) {
2632#line 716
2633 retValue_acc = __ste_email_id0;
2634#line 718
2635 return (retValue_acc);
2636 } else {
2637#line 720
2638 if (handle == 2) {
2639#line 725
2640 retValue_acc = __ste_email_id1;
2641#line 727
2642 return (retValue_acc);
2643 } else {
2644#line 733 "EmailLib.c"
2645 retValue_acc = 0;
2646#line 735
2647 return (retValue_acc);
2648 }
2649 }
2650#line 742 "EmailLib.c"
2651 return (retValue_acc);
2652}
2653}
2654#line 29 "EmailLib.c"
2655void setEmailId(int handle , int value )
2656{
2657
2658 {
2659#line 35
2660 if (handle == 1) {
2661#line 31
2662 __ste_email_id0 = value;
2663 } else {
2664#line 32
2665 if (handle == 2) {
2666#line 33
2667 __ste_email_id1 = value;
2668 } else {
2669
2670 }
2671 }
2672#line 773 "EmailLib.c"
2673 return;
2674}
2675}
2676#line 37 "EmailLib.c"
2677int __ste_email_from0 = 0;
2678#line 39 "EmailLib.c"
2679int __ste_email_from1 = 0;
2680#line 41 "EmailLib.c"
2681int getEmailFrom(int handle )
2682{ int retValue_acc ;
2683
2684 {
2685#line 48 "EmailLib.c"
2686 if (handle == 1) {
2687#line 798
2688 retValue_acc = __ste_email_from0;
2689#line 800
2690 return (retValue_acc);
2691 } else {
2692#line 802
2693 if (handle == 2) {
2694#line 807
2695 retValue_acc = __ste_email_from1;
2696#line 809
2697 return (retValue_acc);
2698 } else {
2699#line 815 "EmailLib.c"
2700 retValue_acc = 0;
2701#line 817
2702 return (retValue_acc);
2703 }
2704 }
2705#line 824 "EmailLib.c"
2706 return (retValue_acc);
2707}
2708}
2709#line 51 "EmailLib.c"
2710void setEmailFrom(int handle , int value )
2711{
2712
2713 {
2714#line 57
2715 if (handle == 1) {
2716#line 53
2717 __ste_email_from0 = value;
2718 } else {
2719#line 54
2720 if (handle == 2) {
2721#line 55
2722 __ste_email_from1 = value;
2723 } else {
2724
2725 }
2726 }
2727#line 855 "EmailLib.c"
2728 return;
2729}
2730}
2731#line 59 "EmailLib.c"
2732int __ste_email_to0 = 0;
2733#line 61 "EmailLib.c"
2734int __ste_email_to1 = 0;
2735#line 63 "EmailLib.c"
2736int getEmailTo(int handle )
2737{ int retValue_acc ;
2738
2739 {
2740#line 70 "EmailLib.c"
2741 if (handle == 1) {
2742#line 880
2743 retValue_acc = __ste_email_to0;
2744#line 882
2745 return (retValue_acc);
2746 } else {
2747#line 884
2748 if (handle == 2) {
2749#line 889
2750 retValue_acc = __ste_email_to1;
2751#line 891
2752 return (retValue_acc);
2753 } else {
2754#line 897 "EmailLib.c"
2755 retValue_acc = 0;
2756#line 899
2757 return (retValue_acc);
2758 }
2759 }
2760#line 906 "EmailLib.c"
2761 return (retValue_acc);
2762}
2763}
2764#line 73 "EmailLib.c"
2765void setEmailTo(int handle , int value )
2766{
2767
2768 {
2769#line 79
2770 if (handle == 1) {
2771#line 75
2772 __ste_email_to0 = value;
2773 } else {
2774#line 76
2775 if (handle == 2) {
2776#line 77
2777 __ste_email_to1 = value;
2778 } else {
2779
2780 }
2781 }
2782#line 937 "EmailLib.c"
2783 return;
2784}
2785}
2786#line 81 "EmailLib.c"
2787char *__ste_email_subject0 ;
2788#line 83 "EmailLib.c"
2789char *__ste_email_subject1 ;
2790#line 85 "EmailLib.c"
2791char *getEmailSubject(int handle )
2792{ char *retValue_acc ;
2793 void *__cil_tmp3 ;
2794
2795 {
2796#line 92 "EmailLib.c"
2797 if (handle == 1) {
2798#line 962
2799 retValue_acc = __ste_email_subject0;
2800#line 964
2801 return (retValue_acc);
2802 } else {
2803#line 966
2804 if (handle == 2) {
2805#line 971
2806 retValue_acc = __ste_email_subject1;
2807#line 973
2808 return (retValue_acc);
2809 } else {
2810#line 979 "EmailLib.c"
2811 __cil_tmp3 = (void *)0;
2812#line 979
2813 retValue_acc = (char *)__cil_tmp3;
2814#line 981
2815 return (retValue_acc);
2816 }
2817 }
2818#line 988 "EmailLib.c"
2819 return (retValue_acc);
2820}
2821}
2822#line 95 "EmailLib.c"
2823void setEmailSubject(int handle , char *value )
2824{
2825
2826 {
2827#line 101
2828 if (handle == 1) {
2829#line 97
2830 __ste_email_subject0 = value;
2831 } else {
2832#line 98
2833 if (handle == 2) {
2834#line 99
2835 __ste_email_subject1 = value;
2836 } else {
2837
2838 }
2839 }
2840#line 1019 "EmailLib.c"
2841 return;
2842}
2843}
2844#line 103 "EmailLib.c"
2845char *__ste_email_body0 = (char *)0;
2846#line 105 "EmailLib.c"
2847char *__ste_email_body1 = (char *)0;
2848#line 107 "EmailLib.c"
2849char *getEmailBody(int handle )
2850{ char *retValue_acc ;
2851 void *__cil_tmp3 ;
2852
2853 {
2854#line 114 "EmailLib.c"
2855 if (handle == 1) {
2856#line 1044
2857 retValue_acc = __ste_email_body0;
2858#line 1046
2859 return (retValue_acc);
2860 } else {
2861#line 1048
2862 if (handle == 2) {
2863#line 1053
2864 retValue_acc = __ste_email_body1;
2865#line 1055
2866 return (retValue_acc);
2867 } else {
2868#line 1061 "EmailLib.c"
2869 __cil_tmp3 = (void *)0;
2870#line 1061
2871 retValue_acc = (char *)__cil_tmp3;
2872#line 1063
2873 return (retValue_acc);
2874 }
2875 }
2876#line 1070 "EmailLib.c"
2877 return (retValue_acc);
2878}
2879}
2880#line 117 "EmailLib.c"
2881void setEmailBody(int handle , char *value )
2882{
2883
2884 {
2885#line 123
2886 if (handle == 1) {
2887#line 119
2888 __ste_email_body0 = value;
2889 } else {
2890#line 120
2891 if (handle == 2) {
2892#line 121
2893 __ste_email_body1 = value;
2894 } else {
2895
2896 }
2897 }
2898#line 1101 "EmailLib.c"
2899 return;
2900}
2901}
2902#line 125 "EmailLib.c"
2903int __ste_email_isEncrypted0 = 0;
2904#line 127 "EmailLib.c"
2905int __ste_email_isEncrypted1 = 0;
2906#line 129 "EmailLib.c"
2907int isEncrypted(int handle )
2908{ int retValue_acc ;
2909
2910 {
2911#line 136 "EmailLib.c"
2912 if (handle == 1) {
2913#line 1126
2914 retValue_acc = __ste_email_isEncrypted0;
2915#line 1128
2916 return (retValue_acc);
2917 } else {
2918#line 1130
2919 if (handle == 2) {
2920#line 1135
2921 retValue_acc = __ste_email_isEncrypted1;
2922#line 1137
2923 return (retValue_acc);
2924 } else {
2925#line 1143 "EmailLib.c"
2926 retValue_acc = 0;
2927#line 1145
2928 return (retValue_acc);
2929 }
2930 }
2931#line 1152 "EmailLib.c"
2932 return (retValue_acc);
2933}
2934}
2935#line 139 "EmailLib.c"
2936void setEmailIsEncrypted(int handle , int value )
2937{
2938
2939 {
2940#line 145
2941 if (handle == 1) {
2942#line 141
2943 __ste_email_isEncrypted0 = value;
2944 } else {
2945#line 142
2946 if (handle == 2) {
2947#line 143
2948 __ste_email_isEncrypted1 = value;
2949 } else {
2950
2951 }
2952 }
2953#line 1183 "EmailLib.c"
2954 return;
2955}
2956}
2957#line 147 "EmailLib.c"
2958int __ste_email_encryptionKey0 = 0;
2959#line 149 "EmailLib.c"
2960int __ste_email_encryptionKey1 = 0;
2961#line 151 "EmailLib.c"
2962int getEmailEncryptionKey(int handle )
2963{ int retValue_acc ;
2964
2965 {
2966#line 158 "EmailLib.c"
2967 if (handle == 1) {
2968#line 1208
2969 retValue_acc = __ste_email_encryptionKey0;
2970#line 1210
2971 return (retValue_acc);
2972 } else {
2973#line 1212
2974 if (handle == 2) {
2975#line 1217
2976 retValue_acc = __ste_email_encryptionKey1;
2977#line 1219
2978 return (retValue_acc);
2979 } else {
2980#line 1225 "EmailLib.c"
2981 retValue_acc = 0;
2982#line 1227
2983 return (retValue_acc);
2984 }
2985 }
2986#line 1234 "EmailLib.c"
2987 return (retValue_acc);
2988}
2989}
2990#line 161 "EmailLib.c"
2991void setEmailEncryptionKey(int handle , int value )
2992{
2993
2994 {
2995#line 167
2996 if (handle == 1) {
2997#line 163
2998 __ste_email_encryptionKey0 = value;
2999 } else {
3000#line 164
3001 if (handle == 2) {
3002#line 165
3003 __ste_email_encryptionKey1 = value;
3004 } else {
3005
3006 }
3007 }
3008#line 1265 "EmailLib.c"
3009 return;
3010}
3011}
3012#line 169 "EmailLib.c"
3013int __ste_email_isSigned0 = 0;
3014#line 171 "EmailLib.c"
3015int __ste_email_isSigned1 = 0;
3016#line 173 "EmailLib.c"
3017int isSigned(int handle )
3018{ int retValue_acc ;
3019
3020 {
3021#line 180 "EmailLib.c"
3022 if (handle == 1) {
3023#line 1290
3024 retValue_acc = __ste_email_isSigned0;
3025#line 1292
3026 return (retValue_acc);
3027 } else {
3028#line 1294
3029 if (handle == 2) {
3030#line 1299
3031 retValue_acc = __ste_email_isSigned1;
3032#line 1301
3033 return (retValue_acc);
3034 } else {
3035#line 1307 "EmailLib.c"
3036 retValue_acc = 0;
3037#line 1309
3038 return (retValue_acc);
3039 }
3040 }
3041#line 1316 "EmailLib.c"
3042 return (retValue_acc);
3043}
3044}
3045#line 183 "EmailLib.c"
3046void setEmailIsSigned(int handle , int value )
3047{
3048
3049 {
3050#line 189
3051 if (handle == 1) {
3052#line 185
3053 __ste_email_isSigned0 = value;
3054 } else {
3055#line 186
3056 if (handle == 2) {
3057#line 187
3058 __ste_email_isSigned1 = value;
3059 } else {
3060
3061 }
3062 }
3063#line 1347 "EmailLib.c"
3064 return;
3065}
3066}
3067#line 191 "EmailLib.c"
3068int __ste_email_signKey0 = 0;
3069#line 193 "EmailLib.c"
3070int __ste_email_signKey1 = 0;
3071#line 195 "EmailLib.c"
3072int getEmailSignKey(int handle )
3073{ int retValue_acc ;
3074
3075 {
3076#line 202 "EmailLib.c"
3077 if (handle == 1) {
3078#line 1372
3079 retValue_acc = __ste_email_signKey0;
3080#line 1374
3081 return (retValue_acc);
3082 } else {
3083#line 1376
3084 if (handle == 2) {
3085#line 1381
3086 retValue_acc = __ste_email_signKey1;
3087#line 1383
3088 return (retValue_acc);
3089 } else {
3090#line 1389 "EmailLib.c"
3091 retValue_acc = 0;
3092#line 1391
3093 return (retValue_acc);
3094 }
3095 }
3096#line 1398 "EmailLib.c"
3097 return (retValue_acc);
3098}
3099}
3100#line 205 "EmailLib.c"
3101void setEmailSignKey(int handle , int value )
3102{
3103
3104 {
3105#line 211
3106 if (handle == 1) {
3107#line 207
3108 __ste_email_signKey0 = value;
3109 } else {
3110#line 208
3111 if (handle == 2) {
3112#line 209
3113 __ste_email_signKey1 = value;
3114 } else {
3115
3116 }
3117 }
3118#line 1429 "EmailLib.c"
3119 return;
3120}
3121}
3122#line 213 "EmailLib.c"
3123int __ste_email_isSignatureVerified0 ;
3124#line 215 "EmailLib.c"
3125int __ste_email_isSignatureVerified1 ;
3126#line 217 "EmailLib.c"
3127int isVerified(int handle )
3128{ int retValue_acc ;
3129
3130 {
3131#line 224 "EmailLib.c"
3132 if (handle == 1) {
3133#line 1454
3134 retValue_acc = __ste_email_isSignatureVerified0;
3135#line 1456
3136 return (retValue_acc);
3137 } else {
3138#line 1458
3139 if (handle == 2) {
3140#line 1463
3141 retValue_acc = __ste_email_isSignatureVerified1;
3142#line 1465
3143 return (retValue_acc);
3144 } else {
3145#line 1471 "EmailLib.c"
3146 retValue_acc = 0;
3147#line 1473
3148 return (retValue_acc);
3149 }
3150 }
3151#line 1480 "EmailLib.c"
3152 return (retValue_acc);
3153}
3154}
3155#line 227 "EmailLib.c"
3156void setEmailIsSignatureVerified(int handle , int value )
3157{
3158
3159 {
3160#line 233
3161 if (handle == 1) {
3162#line 229
3163 __ste_email_isSignatureVerified0 = value;
3164 } else {
3165#line 230
3166 if (handle == 2) {
3167#line 231
3168 __ste_email_isSignatureVerified1 = value;
3169 } else {
3170
3171 }
3172 }
3173#line 1511 "EmailLib.c"
3174 return;
3175}
3176}
3177#line 1 "Client.o"
3178#pragma merger(0,"Client.i","")
3179#line 688 "/usr/include/stdio.h"
3180extern int puts(char const *__s ) ;
3181#line 14 "Client.h"
3182void queue(int client , int msg ) ;
3183#line 17
3184int is_queue_empty(void) ;
3185#line 19
3186int get_queued_client(void) ;
3187#line 21
3188int get_queued_email(void) ;
3189#line 24
3190void mail(int client , int msg ) ;
3191#line 26
3192void outgoing(int client , int msg ) ;
3193#line 28
3194void deliver(int client , int msg ) ;
3195#line 30
3196void incoming(int client , int msg ) ;
3197#line 32
3198int createClient(char *name ) ;
3199#line 35
3200void sendEmail(int sender , int receiver ) ;
3201#line 40
3202int isKeyPairValid(int publicKey , int privateKey ) ;
3203#line 44
3204void generateKeyPair(int client , int seed ) ;
3205#line 45
3206void autoRespond(int client , int msg ) ;
3207#line 46
3208void sendToAddressBook(int client , int msg ) ;
3209#line 48
3210void sign(int client , int msg ) ;
3211#line 50
3212void forward(int client , int msg ) ;
3213#line 52
3214void verify(int client , int msg ) ;
3215#line 6 "Client.c"
3216int queue_empty = 1;
3217#line 9 "Client.c"
3218int queued_message ;
3219#line 12 "Client.c"
3220int queued_client ;
3221#line 18 "Client.c"
3222void mail(int client , int msg )
3223{ int tmp ;
3224
3225 {
3226 {
3227#line 19
3228 puts("mail sent");
3229#line 20
3230 tmp = getEmailTo(msg);
3231#line 20
3232 incoming(tmp, msg);
3233 }
3234#line 739 "Client.c"
3235 return;
3236}
3237}
3238#line 27 "Client.c"
3239void outgoing__wrappee__Keys(int client , int msg )
3240{ int tmp ;
3241
3242 {
3243 {
3244#line 28
3245 tmp = getClientId(client);
3246#line 28
3247 setEmailFrom(msg, tmp);
3248#line 29
3249 mail(client, msg);
3250 }
3251#line 761 "Client.c"
3252 return;
3253}
3254}
3255#line 33 "Client.c"
3256void outgoing__wrappee__AutoResponder(int client , int msg )
3257{ int receiver ;
3258 int tmp ;
3259 int pubkey ;
3260 int tmp___0 ;
3261
3262 {
3263 {
3264#line 36
3265 tmp = getEmailTo(msg);
3266#line 36
3267 receiver = tmp;
3268#line 37
3269 tmp___0 = findPublicKey(client, receiver);
3270#line 37
3271 pubkey = tmp___0;
3272 }
3273#line 38
3274 if (pubkey) {
3275 {
3276#line 39
3277 setEmailEncryptionKey(msg, pubkey);
3278#line 40
3279 setEmailIsEncrypted(msg, 1);
3280 }
3281 } else {
3282
3283 }
3284 {
3285#line 45
3286 outgoing__wrappee__Keys(client, msg);
3287 }
3288#line 796 "Client.c"
3289 return;
3290}
3291}
3292#line 52 "Client.c"
3293void outgoing__wrappee__AddressBook(int client , int msg )
3294{ int size ;
3295 int tmp ;
3296 int receiver ;
3297 int tmp___0 ;
3298 int second ;
3299 int tmp___1 ;
3300 int tmp___2 ;
3301
3302 {
3303 {
3304#line 54
3305 tmp = getClientAddressBookSize(client);
3306#line 54
3307 size = tmp;
3308 }
3309#line 56
3310 if (size) {
3311 {
3312#line 57
3313 sendToAddressBook(client, msg);
3314#line 58
3315 puts("sending to alias in address book\n");
3316#line 59
3317 tmp___0 = getEmailTo(msg);
3318#line 59
3319 receiver = tmp___0;
3320#line 61
3321 puts("sending to second receipient\n");
3322#line 62
3323 tmp___1 = getClientAddressBookAddress(client, 1);
3324#line 62
3325 second = tmp___1;
3326#line 63
3327 setEmailTo(msg, second);
3328#line 64
3329 outgoing__wrappee__AutoResponder(client, msg);
3330#line 67
3331 tmp___2 = getClientAddressBookAddress(client, 0);
3332#line 67
3333 setEmailTo(msg, tmp___2);
3334#line 68
3335 outgoing__wrappee__AutoResponder(client, msg);
3336 }
3337 } else {
3338 {
3339#line 70
3340 outgoing__wrappee__AutoResponder(client, msg);
3341 }
3342 }
3343#line 846 "Client.c"
3344 return;
3345}
3346}
3347#line 78 "Client.c"
3348void outgoing(int client , int msg )
3349{
3350
3351 {
3352 {
3353#line 79
3354 sign(client, msg);
3355#line 80
3356 outgoing__wrappee__AddressBook(client, msg);
3357 }
3358#line 868 "Client.c"
3359 return;
3360}
3361}
3362#line 870
3363void __utac_acc__VerifyForward_spec__1(int client , int msg ) ;
3364#line 87 "Client.c"
3365void deliver(int client , int msg )
3366{ int __utac__ad__arg1 ;
3367 int __utac__ad__arg2 ;
3368
3369 {
3370 {
3371#line 881 "Client.c"
3372 __utac__ad__arg1 = client;
3373#line 882
3374 __utac__ad__arg2 = msg;
3375#line 883
3376 __utac_acc__VerifyForward_spec__1(__utac__ad__arg1, __utac__ad__arg2);
3377#line 88 "Client.c"
3378 puts("mail delivered\n");
3379 }
3380#line 898 "Client.c"
3381 return;
3382}
3383}
3384#line 95 "Client.c"
3385void incoming__wrappee__Encrypt(int client , int msg )
3386{
3387
3388 {
3389 {
3390#line 96
3391 deliver(client, msg);
3392 }
3393#line 918 "Client.c"
3394 return;
3395}
3396}
3397#line 102 "Client.c"
3398void incoming__wrappee__Sign(int client , int msg )
3399{ int tmp ;
3400
3401 {
3402 {
3403#line 103
3404 incoming__wrappee__Encrypt(client, msg);
3405#line 104
3406 tmp = getClientAutoResponse(client);
3407 }
3408#line 104
3409 if (tmp) {
3410 {
3411#line 105
3412 autoRespond(client, msg);
3413 }
3414 } else {
3415
3416 }
3417#line 943 "Client.c"
3418 return;
3419}
3420}
3421#line 112 "Client.c"
3422void incoming__wrappee__Forward(int client , int msg )
3423{ int fwreceiver ;
3424 int tmp ;
3425
3426 {
3427 {
3428#line 113
3429 incoming__wrappee__Sign(client, msg);
3430#line 114
3431 tmp = getClientForwardReceiver(client);
3432#line 114
3433 fwreceiver = tmp;
3434 }
3435#line 115
3436 if (fwreceiver) {
3437 {
3438#line 117
3439 setEmailTo(msg, fwreceiver);
3440#line 118
3441 forward(client, msg);
3442 }
3443 } else {
3444
3445 }
3446#line 974 "Client.c"
3447 return;
3448}
3449}
3450#line 126 "Client.c"
3451void incoming__wrappee__Verify(int client , int msg )
3452{
3453
3454 {
3455 {
3456#line 127
3457 verify(client, msg);
3458#line 128
3459 incoming__wrappee__Forward(client, msg);
3460 }
3461#line 996 "Client.c"
3462 return;
3463}
3464}
3465#line 133 "Client.c"
3466void incoming(int client , int msg )
3467{ int privkey ;
3468 int tmp ;
3469 int tmp___0 ;
3470 int tmp___1 ;
3471 int tmp___2 ;
3472
3473 {
3474 {
3475#line 136
3476 tmp = getClientPrivateKey(client);
3477#line 136
3478 privkey = tmp;
3479 }
3480#line 137
3481 if (privkey) {
3482 {
3483#line 145
3484 tmp___0 = isEncrypted(msg);
3485 }
3486#line 145
3487 if (tmp___0) {
3488 {
3489#line 145
3490 tmp___1 = getEmailEncryptionKey(msg);
3491#line 145
3492 tmp___2 = isKeyPairValid(tmp___1, privkey);
3493 }
3494#line 145
3495 if (tmp___2) {
3496 {
3497#line 142
3498 setEmailIsEncrypted(msg, 0);
3499#line 143
3500 setEmailEncryptionKey(msg, 0);
3501 }
3502 } else {
3503
3504 }
3505 } else {
3506
3507 }
3508 } else {
3509
3510 }
3511 {
3512#line 148
3513 incoming__wrappee__Verify(client, msg);
3514 }
3515#line 1030 "Client.c"
3516 return;
3517}
3518}
3519#line 152 "Client.c"
3520int createClient(char *name )
3521{ int retValue_acc ;
3522 int client ;
3523 int tmp ;
3524
3525 {
3526 {
3527#line 153
3528 tmp = initClient();
3529#line 153
3530 client = tmp;
3531#line 1052 "Client.c"
3532 retValue_acc = client;
3533 }
3534#line 1054
3535 return (retValue_acc);
3536#line 1061
3537 return (retValue_acc);
3538}
3539}
3540#line 160 "Client.c"
3541void sendEmail(int sender , int receiver )
3542{ int email ;
3543 int tmp ;
3544
3545 {
3546 {
3547#line 161
3548 tmp = createEmail(0, receiver);
3549#line 161
3550 email = tmp;
3551#line 162
3552 outgoing(sender, email);
3553 }
3554#line 1089 "Client.c"
3555 return;
3556}
3557}
3558#line 170 "Client.c"
3559void queue(int client , int msg )
3560{
3561
3562 {
3563#line 171
3564 queue_empty = 0;
3565#line 172
3566 queued_message = msg;
3567#line 173
3568 queued_client = client;
3569#line 1113 "Client.c"
3570 return;
3571}
3572}
3573#line 179 "Client.c"
3574int is_queue_empty(void)
3575{ int retValue_acc ;
3576
3577 {
3578#line 1131 "Client.c"
3579 retValue_acc = queue_empty;
3580#line 1133
3581 return (retValue_acc);
3582#line 1140
3583 return (retValue_acc);
3584}
3585}
3586#line 186 "Client.c"
3587int get_queued_client(void)
3588{ int retValue_acc ;
3589
3590 {
3591#line 1162 "Client.c"
3592 retValue_acc = queued_client;
3593#line 1164
3594 return (retValue_acc);
3595#line 1171
3596 return (retValue_acc);
3597}
3598}
3599#line 193 "Client.c"
3600int get_queued_email(void)
3601{ int retValue_acc ;
3602
3603 {
3604#line 1193 "Client.c"
3605 retValue_acc = queued_message;
3606#line 1195
3607 return (retValue_acc);
3608#line 1202
3609 return (retValue_acc);
3610}
3611}
3612#line 199 "Client.c"
3613int isKeyPairValid(int publicKey , int privateKey )
3614{ int retValue_acc ;
3615 char const * __restrict __cil_tmp4 ;
3616
3617 {
3618 {
3619#line 200
3620 __cil_tmp4 = (char const * __restrict )"keypair valid %d %d";
3621#line 200
3622 printf(__cil_tmp4, publicKey, privateKey);
3623 }
3624#line 201 "Client.c"
3625 if (! publicKey) {
3626#line 1227 "Client.c"
3627 retValue_acc = 0;
3628#line 1229
3629 return (retValue_acc);
3630 } else {
3631#line 201 "Client.c"
3632 if (! privateKey) {
3633#line 1227 "Client.c"
3634 retValue_acc = 0;
3635#line 1229
3636 return (retValue_acc);
3637 } else {
3638
3639 }
3640 }
3641#line 1234 "Client.c"
3642 retValue_acc = privateKey == publicKey;
3643#line 1236
3644 return (retValue_acc);
3645#line 1243
3646 return (retValue_acc);
3647}
3648}
3649#line 209 "Client.c"
3650void generateKeyPair(int client , int seed )
3651{
3652
3653 {
3654 {
3655#line 210
3656 setClientPrivateKey(client, seed);
3657 }
3658#line 1267 "Client.c"
3659 return;
3660}
3661}
3662#line 216 "Client.c"
3663void autoRespond(int client , int msg )
3664{ int sender ;
3665 int tmp ;
3666
3667 {
3668 {
3669#line 217
3670 puts("sending autoresponse\n");
3671#line 218
3672 tmp = getEmailFrom(msg);
3673#line 218
3674 sender = tmp;
3675#line 219
3676 setEmailTo(msg, sender);
3677#line 220
3678 queue(client, msg);
3679 }
3680#line 1409 "Client.c"
3681 return;
3682}
3683}
3684#line 225 "Client.c"
3685void sendToAddressBook(int client , int msg )
3686{
3687
3688 {
3689#line 1427 "Client.c"
3690 return;
3691}
3692}
3693#line 231 "Client.c"
3694void sign(int client , int msg )
3695{ int privkey ;
3696 int tmp ;
3697
3698 {
3699 {
3700#line 232
3701 tmp = getClientPrivateKey(client);
3702#line 232
3703 privkey = tmp;
3704 }
3705#line 233
3706 if (! privkey) {
3707#line 234
3708 return;
3709 } else {
3710
3711 }
3712 {
3713#line 235
3714 setEmailIsSigned(msg, 1);
3715#line 236
3716 setEmailSignKey(msg, privkey);
3717 }
3718#line 1457 "Client.c"
3719 return;
3720}
3721}
3722#line 241 "Client.c"
3723void forward(int client , int msg )
3724{
3725
3726 {
3727 {
3728#line 242
3729 puts("Forwarding message.\n");
3730#line 243
3731 printMail(msg);
3732#line 244
3733 queue(client, msg);
3734 }
3735#line 1481 "Client.c"
3736 return;
3737}
3738}
3739#line 250 "Client.c"
3740void verify(int client , int msg )
3741{ int tmp ;
3742 int tmp___0 ;
3743 int pubkey ;
3744 int tmp___1 ;
3745 int tmp___2 ;
3746 int tmp___3 ;
3747 int tmp___4 ;
3748
3749 {
3750 {
3751#line 255
3752 tmp = isReadable(msg);
3753 }
3754#line 255
3755 if (tmp) {
3756 {
3757#line 255
3758 tmp___0 = isSigned(msg);
3759 }
3760#line 255
3761 if (tmp___0) {
3762
3763 } else {
3764#line 256
3765 return;
3766 }
3767 } else {
3768#line 256
3769 return;
3770 }
3771 {
3772#line 255
3773 tmp___1 = getEmailFrom(msg);
3774#line 255
3775 tmp___2 = findPublicKey(client, tmp___1);
3776#line 255
3777 pubkey = tmp___2;
3778 }
3779#line 256
3780 if (pubkey) {
3781 {
3782#line 256
3783 tmp___3 = getEmailSignKey(msg);
3784#line 256
3785 tmp___4 = isKeyPairValid(tmp___3, pubkey);
3786 }
3787#line 256
3788 if (tmp___4) {
3789 {
3790#line 257
3791 setEmailIsSignatureVerified(msg, 1);
3792 }
3793 } else {
3794
3795 }
3796 } else {
3797
3798 }
3799#line 1512 "Client.c"
3800 return;
3801}
3802}
3803#line 1 "VerifyForward_spec.o"
3804#pragma merger(0,"VerifyForward_spec.i","")
3805#line 12 "VerifyForward_spec.c"
3806void __utac_acc__VerifyForward_spec__1(int client , int msg )
3807{ int pubkey ;
3808 int tmp ;
3809 int tmp___0 ;
3810 int tmp___1 ;
3811
3812 {
3813 {
3814#line 15
3815 puts("before deliver\n");
3816#line 17
3817 tmp___1 = isVerified(msg);
3818 }
3819#line 17
3820 if (tmp___1) {
3821 {
3822#line 18
3823 tmp = getEmailFrom(msg);
3824#line 18
3825 tmp___0 = findPublicKey(client, tmp);
3826#line 18
3827 pubkey = tmp___0;
3828 }
3829#line 19
3830 if (pubkey == 0) {
3831 {
3832#line 20
3833 __automaton_fail();
3834 }
3835 } else {
3836
3837 }
3838 } else {
3839
3840 }
3841#line 20
3842 return;
3843}
3844}
3845#line 1 "Test.o"
3846#pragma merger(0,"Test.i","")
3847#line 2 "Test.h"
3848int bob ;
3849#line 5 "Test.h"
3850int rjh ;
3851#line 8 "Test.h"
3852int chuck ;
3853#line 11
3854void setup_bob(int bob___0 ) ;
3855#line 14
3856void setup_rjh(int rjh___0 ) ;
3857#line 17
3858void setup_chuck(int chuck___0 ) ;
3859#line 23
3860void bobToRjh(void) ;
3861#line 26
3862void rjhToBob(void) ;
3863#line 29
3864void test(void) ;
3865#line 32
3866void setup(void) ;
3867#line 35
3868int main(void) ;
3869#line 36
3870void bobKeyAdd(void) ;
3871#line 39
3872void bobKeyAddChuck(void) ;
3873#line 42
3874void rjhKeyAdd(void) ;
3875#line 45
3876void rjhKeyAddChuck(void) ;
3877#line 48
3878void chuckKeyAdd(void) ;
3879#line 51
3880void bobKeyChange(void) ;
3881#line 54
3882void rjhKeyChange(void) ;
3883#line 57
3884void rjhDeletePrivateKey(void) ;
3885#line 60
3886void chuckKeyAddRjh(void) ;
3887#line 61
3888void rjhSetAutoRespond(void) ;
3889#line 63
3890void bobSetAddressBook(void) ;
3891#line 64
3892void rjhEnableForwarding(void) ;
3893#line 18 "Test.c"
3894void setup_bob__wrappee__Base(int bob___0 )
3895{
3896
3897 {
3898 {
3899#line 19
3900 setClientId(bob___0, bob___0);
3901 }
3902#line 1338 "Test.c"
3903 return;
3904}
3905}
3906#line 23 "Test.c"
3907void setup_bob(int bob___0 )
3908{
3909
3910 {
3911 {
3912#line 24
3913 setup_bob__wrappee__Base(bob___0);
3914#line 25
3915 setClientPrivateKey(bob___0, 123);
3916 }
3917#line 1360 "Test.c"
3918 return;
3919}
3920}
3921#line 33 "Test.c"
3922void setup_rjh__wrappee__Base(int rjh___0 )
3923{
3924
3925 {
3926 {
3927#line 34
3928 setClientId(rjh___0, rjh___0);
3929 }
3930#line 1380 "Test.c"
3931 return;
3932}
3933}
3934#line 40 "Test.c"
3935void setup_rjh(int rjh___0 )
3936{
3937
3938 {
3939 {
3940#line 42
3941 setup_rjh__wrappee__Base(rjh___0);
3942#line 43
3943 setClientPrivateKey(rjh___0, 456);
3944 }
3945#line 1402 "Test.c"
3946 return;
3947}
3948}
3949#line 50 "Test.c"
3950void setup_chuck__wrappee__Base(int chuck___0 )
3951{
3952
3953 {
3954 {
3955#line 51
3956 setClientId(chuck___0, chuck___0);
3957 }
3958#line 1422 "Test.c"
3959 return;
3960}
3961}
3962#line 57 "Test.c"
3963void setup_chuck(int chuck___0 )
3964{
3965
3966 {
3967 {
3968#line 58
3969 setup_chuck__wrappee__Base(chuck___0);
3970#line 59
3971 setClientPrivateKey(chuck___0, 789);
3972 }
3973#line 1444 "Test.c"
3974 return;
3975}
3976}
3977#line 69 "Test.c"
3978void bobToRjh(void)
3979{ int tmp ;
3980 int tmp___0 ;
3981 int tmp___1 ;
3982
3983 {
3984 {
3985#line 71
3986 puts("Please enter a subject and a message body.\n");
3987#line 72
3988 sendEmail(bob, rjh);
3989#line 73
3990 tmp___1 = is_queue_empty();
3991 }
3992#line 73
3993 if (tmp___1) {
3994
3995 } else {
3996 {
3997#line 74
3998 tmp = get_queued_email();
3999#line 74
4000 tmp___0 = get_queued_client();
4001#line 74
4002 outgoing(tmp___0, tmp);
4003 }
4004 }
4005#line 1471 "Test.c"
4006 return;
4007}
4008}
4009#line 81 "Test.c"
4010void rjhToBob(void)
4011{
4012
4013 {
4014 {
4015#line 83
4016 puts("Please enter a subject and a message body.\n");
4017#line 84
4018 sendEmail(rjh, bob);
4019 }
4020#line 1493 "Test.c"
4021 return;
4022}
4023}
4024#line 88 "Test.c"
4025#line 95 "Test.c"
4026void setup(void)
4027{ char const * __restrict __cil_tmp1 ;
4028 char const * __restrict __cil_tmp2 ;
4029 char const * __restrict __cil_tmp3 ;
4030
4031 {
4032 {
4033#line 96
4034 bob = 1;
4035#line 97
4036 setup_bob(bob);
4037#line 98
4038 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
4039#line 98
4040 printf(__cil_tmp1, bob);
4041#line 100
4042 rjh = 2;
4043#line 101
4044 setup_rjh(rjh);
4045#line 102
4046 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
4047#line 102
4048 printf(__cil_tmp2, rjh);
4049#line 104
4050 chuck = 3;
4051#line 105
4052 setup_chuck(chuck);
4053#line 106
4054 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
4055#line 106
4056 printf(__cil_tmp3, chuck);
4057 }
4058#line 1564 "Test.c"
4059 return;
4060}
4061}
4062#line 112 "Test.c"
4063int main(void)
4064{ int retValue_acc ;
4065 int tmp ;
4066
4067 {
4068 {
4069#line 113
4070 select_helpers();
4071#line 114
4072 select_features();
4073#line 115
4074 tmp = valid_product();
4075 }
4076#line 115
4077 if (tmp) {
4078 {
4079#line 116
4080 setup();
4081#line 117
4082 test();
4083 }
4084 } else {
4085
4086 }
4087#line 1595 "Test.c"
4088 return (retValue_acc);
4089}
4090}
4091#line 125 "Test.c"
4092void bobKeyAdd(void)
4093{ int tmp ;
4094 int tmp___0 ;
4095 char const * __restrict __cil_tmp3 ;
4096 char const * __restrict __cil_tmp4 ;
4097
4098 {
4099 {
4100#line 126
4101 createClientKeyringEntry(bob);
4102#line 127
4103 setClientKeyringUser(bob, 0, 2);
4104#line 128
4105 setClientKeyringPublicKey(bob, 0, 456);
4106#line 129
4107 puts("bob added rjhs key");
4108#line 130
4109 tmp = getClientKeyringUser(bob, 0);
4110#line 130
4111 __cil_tmp3 = (char const * __restrict )"%d\n";
4112#line 130
4113 printf(__cil_tmp3, tmp);
4114#line 131
4115 tmp___0 = getClientKeyringPublicKey(bob, 0);
4116#line 131
4117 __cil_tmp4 = (char const * __restrict )"%d\n";
4118#line 131
4119 printf(__cil_tmp4, tmp___0);
4120 }
4121#line 1629 "Test.c"
4122 return;
4123}
4124}
4125#line 137 "Test.c"
4126void rjhKeyAdd(void)
4127{
4128
4129 {
4130 {
4131#line 138
4132 createClientKeyringEntry(rjh);
4133#line 139
4134 setClientKeyringUser(rjh, 0, 1);
4135#line 140
4136 setClientKeyringPublicKey(rjh, 0, 123);
4137 }
4138#line 1653 "Test.c"
4139 return;
4140}
4141}
4142#line 146 "Test.c"
4143void rjhKeyAddChuck(void)
4144{
4145
4146 {
4147 {
4148#line 147
4149 createClientKeyringEntry(rjh);
4150#line 148
4151 setClientKeyringUser(rjh, 0, 3);
4152#line 149
4153 setClientKeyringPublicKey(rjh, 0, 789);
4154 }
4155#line 1677 "Test.c"
4156 return;
4157}
4158}
4159#line 156 "Test.c"
4160void bobKeyAddChuck(void)
4161{
4162
4163 {
4164 {
4165#line 157
4166 createClientKeyringEntry(bob);
4167#line 158
4168 setClientKeyringUser(bob, 1, 3);
4169#line 159
4170 setClientKeyringPublicKey(bob, 1, 789);
4171 }
4172#line 1701 "Test.c"
4173 return;
4174}
4175}
4176#line 165 "Test.c"
4177void chuckKeyAdd(void)
4178{
4179
4180 {
4181 {
4182#line 166
4183 createClientKeyringEntry(chuck);
4184#line 167
4185 setClientKeyringUser(chuck, 0, 1);
4186#line 168
4187 setClientKeyringPublicKey(chuck, 0, 123);
4188 }
4189#line 1725 "Test.c"
4190 return;
4191}
4192}
4193#line 174 "Test.c"
4194void chuckKeyAddRjh(void)
4195{
4196
4197 {
4198 {
4199#line 175
4200 createClientKeyringEntry(chuck);
4201#line 176
4202 setClientKeyringUser(chuck, 0, 2);
4203#line 177
4204 setClientKeyringPublicKey(chuck, 0, 456);
4205 }
4206#line 1749 "Test.c"
4207 return;
4208}
4209}
4210#line 183 "Test.c"
4211void rjhDeletePrivateKey(void)
4212{
4213
4214 {
4215 {
4216#line 184
4217 setClientPrivateKey(rjh, 0);
4218 }
4219#line 1769 "Test.c"
4220 return;
4221}
4222}
4223#line 190 "Test.c"
4224void bobKeyChange(void)
4225{
4226
4227 {
4228 {
4229#line 191
4230 generateKeyPair(bob, 777);
4231 }
4232#line 1789 "Test.c"
4233 return;
4234}
4235}
4236#line 197 "Test.c"
4237void rjhKeyChange(void)
4238{
4239
4240 {
4241 {
4242#line 198
4243 generateKeyPair(rjh, 666);
4244 }
4245#line 1809 "Test.c"
4246 return;
4247}
4248}
4249#line 204 "Test.c"
4250void rjhSetAutoRespond(void)
4251{
4252
4253 {
4254 {
4255#line 205
4256 setClientAutoResponse(rjh, 1);
4257 }
4258#line 1829 "Test.c"
4259 return;
4260}
4261}
4262#line 210 "Test.c"
4263void bobSetAddressBook(void)
4264{
4265
4266 {
4267 {
4268#line 211
4269 setClientAddressBookSize(bob, 1);
4270#line 212
4271 setClientAddressBookAlias(bob, 0, rjh);
4272#line 213
4273 setClientAddressBookAddress(bob, 0, rjh);
4274#line 214
4275 setClientAddressBookAddress(bob, 1, chuck);
4276 }
4277#line 1855 "Test.c"
4278 return;
4279}
4280}
4281#line 220 "Test.c"
4282void rjhEnableForwarding(void)
4283{
4284
4285 {
4286 {
4287#line 221
4288 setClientForwardReceiver(rjh, chuck);
4289 }
4290#line 1875 "Test.c"
4291 return;
4292}
4293}
4294#line 1 "scenario.o"
4295#pragma merger(0,"scenario.i","")
4296#line 1 "scenario.c"
4297void test(void)
4298{ int op1 ;
4299 int op2 ;
4300 int op3 ;
4301 int op4 ;
4302 int op5 ;
4303 int op6 ;
4304 int op7 ;
4305 int op8 ;
4306 int op9 ;
4307 int op10 ;
4308 int op11 ;
4309 int splverifierCounter ;
4310 int tmp ;
4311 int tmp___0 ;
4312 int tmp___1 ;
4313 int tmp___2 ;
4314 int tmp___3 ;
4315 int tmp___4 ;
4316 int tmp___5 ;
4317 int tmp___6 ;
4318 int tmp___7 ;
4319 int tmp___8 ;
4320 int tmp___9 ;
4321
4322 {
4323#line 2
4324 op1 = 0;
4325#line 3
4326 op2 = 0;
4327#line 4
4328 op3 = 0;
4329#line 5
4330 op4 = 0;
4331#line 6
4332 op5 = 0;
4333#line 7
4334 op6 = 0;
4335#line 8
4336 op7 = 0;
4337#line 9
4338 op8 = 0;
4339#line 10
4340 op9 = 0;
4341#line 11
4342 op10 = 0;
4343#line 12
4344 op11 = 0;
4345#line 13
4346 splverifierCounter = 0;
4347 {
4348#line 14
4349 while (1) {
4350 while_3_continue: ;
4351#line 14
4352 if (splverifierCounter < 4) {
4353
4354 } else {
4355 goto while_3_break;
4356 }
4357#line 15
4358 splverifierCounter = splverifierCounter + 1;
4359#line 16
4360 if (! op1) {
4361 {
4362#line 16
4363 tmp___9 = __VERIFIER_nondet_int();
4364 }
4365#line 16
4366 if (tmp___9) {
4367 {
4368#line 17
4369 bobKeyAdd();
4370#line 18
4371 op1 = 1;
4372 }
4373 } else {
4374 goto _L___8;
4375 }
4376 } else {
4377 _L___8:
4378#line 19
4379 if (! op2) {
4380 {
4381#line 19
4382 tmp___8 = __VERIFIER_nondet_int();
4383 }
4384#line 19
4385 if (tmp___8) {
4386 {
4387#line 21
4388 rjhSetAutoRespond();
4389#line 22
4390 op2 = 1;
4391 }
4392 } else {
4393 goto _L___7;
4394 }
4395 } else {
4396 _L___7:
4397#line 23
4398 if (! op3) {
4399 {
4400#line 23
4401 tmp___7 = __VERIFIER_nondet_int();
4402 }
4403#line 23
4404 if (tmp___7) {
4405 {
4406#line 25
4407 rjhDeletePrivateKey();
4408#line 26
4409 op3 = 1;
4410 }
4411 } else {
4412 goto _L___6;
4413 }
4414 } else {
4415 _L___6:
4416#line 27
4417 if (! op4) {
4418 {
4419#line 27
4420 tmp___6 = __VERIFIER_nondet_int();
4421 }
4422#line 27
4423 if (tmp___6) {
4424 {
4425#line 29
4426 rjhKeyAdd();
4427#line 30
4428 op4 = 1;
4429 }
4430 } else {
4431 goto _L___5;
4432 }
4433 } else {
4434 _L___5:
4435#line 31
4436 if (! op5) {
4437 {
4438#line 31
4439 tmp___5 = __VERIFIER_nondet_int();
4440 }
4441#line 31
4442 if (tmp___5) {
4443 {
4444#line 33
4445 chuckKeyAddRjh();
4446#line 34
4447 op5 = 1;
4448 }
4449 } else {
4450 goto _L___4;
4451 }
4452 } else {
4453 _L___4:
4454#line 35
4455 if (! op6) {
4456 {
4457#line 35
4458 tmp___4 = __VERIFIER_nondet_int();
4459 }
4460#line 35
4461 if (tmp___4) {
4462 {
4463#line 37
4464 rjhEnableForwarding();
4465#line 38
4466 op6 = 1;
4467 }
4468 } else {
4469 goto _L___3;
4470 }
4471 } else {
4472 _L___3:
4473#line 39
4474 if (! op7) {
4475 {
4476#line 39
4477 tmp___3 = __VERIFIER_nondet_int();
4478 }
4479#line 39
4480 if (tmp___3) {
4481 {
4482#line 41
4483 rjhKeyChange();
4484#line 42
4485 op7 = 1;
4486 }
4487 } else {
4488 goto _L___2;
4489 }
4490 } else {
4491 _L___2:
4492#line 43
4493 if (! op8) {
4494 {
4495#line 43
4496 tmp___2 = __VERIFIER_nondet_int();
4497 }
4498#line 43
4499 if (tmp___2) {
4500 {
4501#line 45
4502 bobSetAddressBook();
4503#line 46
4504 op8 = 1;
4505 }
4506 } else {
4507 goto _L___1;
4508 }
4509 } else {
4510 _L___1:
4511#line 47
4512 if (! op9) {
4513 {
4514#line 47
4515 tmp___1 = __VERIFIER_nondet_int();
4516 }
4517#line 47
4518 if (tmp___1) {
4519 {
4520#line 49
4521 chuckKeyAdd();
4522#line 50
4523 op9 = 1;
4524 }
4525 } else {
4526 goto _L___0;
4527 }
4528 } else {
4529 _L___0:
4530#line 51
4531 if (! op10) {
4532 {
4533#line 51
4534 tmp___0 = __VERIFIER_nondet_int();
4535 }
4536#line 51
4537 if (tmp___0) {
4538 {
4539#line 53
4540 bobKeyChange();
4541#line 54
4542 op10 = 1;
4543 }
4544 } else {
4545 goto _L;
4546 }
4547 } else {
4548 _L:
4549#line 55
4550 if (! op11) {
4551 {
4552#line 55
4553 tmp = __VERIFIER_nondet_int();
4554 }
4555#line 55
4556 if (tmp) {
4557 {
4558#line 57
4559 chuckKeyAdd();
4560#line 58
4561 op11 = 1;
4562 }
4563 } else {
4564 goto while_3_break;
4565 }
4566 } else {
4567 goto while_3_break;
4568 }
4569 }
4570 }
4571 }
4572 }
4573 }
4574 }
4575 }
4576 }
4577 }
4578 }
4579 }
4580 while_3_break: ;
4581 }
4582 {
4583#line 62
4584 bobToRjh();
4585 }
4586#line 171 "scenario.c"
4587 return;
4588}
4589}