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