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