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