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