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