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