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