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