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