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