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