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