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