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