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