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