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