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