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