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