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