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