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