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