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