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