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