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